introduce fresh term when none is available in context or model to fix …

…#2456

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/smt_checker.cpp

@@ -23,18 +23,16 @@ Revision History:
 namespace smt {
 
     bool checker::all_args(app * a, bool is_true) {
-        unsigned num_args = a->get_num_args();
-        for (unsigned i = 0; i < num_args; i++) {
-            if (!check(a->get_arg(i), is_true))
+        for (expr* arg : *a) {
+            if (!check(arg, is_true))
                 return false;
         }
         return true;
     }
 
     bool checker::any_arg(app * a, bool is_true) {
-        unsigned num_args = a->get_num_args();
-        for (unsigned i = 0; i < num_args; i++) {
-            if (check(a->get_arg(i), is_true))
+        for (expr* arg : *a) {
+            if (check(arg, is_true))
                 return true;
         }
         return false;

src/smt/smt_model_checker.cpp

@@ -78,6 +78,19 @@ namespace smt {
         return t;
     }
 
+    expr * model_checker::get_type_compatible_term(expr * val) {
+        for (auto const& kv : m_value2expr) {
+            if (m.get_sort(kv.m_key) == m.get_sort(val) &&
+                !contains_model_value(kv.m_key)) {
+                return kv.m_key;
+            }
+        }
+        app* fresh_term = m.mk_fresh_const("sk", m.get_sort(val));
+        m_context->ensure_internalized(fresh_term);
+        m_value2expr.insert(val, fresh_term);
+        return fresh_term;
+    }
+
     void model_checker::init_value2expr() {
         if (m_value2expr.empty()) {
             // populate m_value2expr
@@ -207,8 +220,7 @@ namespace smt {
                 }
             }
             if (contains_model_value(sk_value)) {
-                TRACE("model_checker", tout << "value is private to model: " << sk_value << "\n";);
-                return false;
+                sk_value = get_type_compatible_term(sk_value);
             }
             func_decl * f = nullptr;
             if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f)) {

src/smt/smt_model_checker.h

@@ -60,6 +60,7 @@ namespace smt {
         void init_aux_context();
         void init_value2expr();
         expr * get_term_from_ctx(expr * val);
+        expr * get_type_compatible_term(expr * val);
         expr_ref replace_value_from_ctx(expr * e);
         void restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe);
         void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);