From 59f69bbe0dc81e6aef2a9fa9aa9b0cfffd1ce2b9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Aug 2019 11:56:03 -0700
Subject: [PATCH] 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       | 10 ++++------
 src/smt/smt_model_checker.cpp | 16 ++++++++++++++--
 src/smt/smt_model_checker.h   |  1 +
 3 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/smt/smt_checker.cpp b/src/smt/smt_checker.cpp
index 1b6a5d37009..b124f3118bb 100644
--- a/src/smt/smt_checker.cpp
+++ b/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;
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 58158ec0613..b9e93cac9ff 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/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)) {
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index 57edf303400..7c83eb4fd0b 100644
--- a/src/smt/smt_model_checker.h
+++ b/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);