From dde5218b293075a2267b09fe33722da18691c721 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Jan 2023 22:47:34 -0500
Subject: [PATCH] fix mbqi value caching issue raised by Clemens and Martin

---
 src/smt/smt_model_checker.cpp   | 17 ++++++-------
 src/smt/smt_model_generator.cpp | 43 ++++++++++++++++++---------------
 2 files changed, 32 insertions(+), 28 deletions(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 61173907b11..e555088538c 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -82,22 +82,18 @@ namespace smt {
         app* fresh_term;
         if (is_app(val) && to_app(val)->get_num_args() > 0) {
             ptr_buffer<expr> args;
-            for (expr* arg : *to_app(val)) {
+            for (expr* arg : *to_app(val)) 
                 args.push_back(get_type_compatible_term(arg));
-            }
             fresh_term = m.mk_app(to_app(val)->get_decl(), args.size(), args.data());
         }
         else {
             expr * sk_term = get_term_from_ctx(val);
-            if (sk_term != nullptr) {
+            if (sk_term != nullptr) 
                 return sk_term;
-            }
 
-            for (expr* f : m_fresh_exprs) {
-                if (f->get_sort() == val->get_sort()) {
+            for (expr* f : m_fresh_exprs) 
+                if (f->get_sort() == val->get_sort()) 
                     return f;
-                }
-            }
             fresh_term = m.mk_fresh_const("sk", val->get_sort());
         }
         m_fresh_exprs.push_back(fresh_term);
@@ -106,13 +102,16 @@ namespace smt {
     }
 
     void model_checker::init_value2expr() {
+        
         if (m_value2expr.empty()) {
             // populate m_value2expr
             for (auto const& kv : *m_root2value) {
                 enode * n   = kv.m_key;
                 expr  * val = kv.m_value;
                 n = n->get_eq_enode_with_min_gen();
-                m_value2expr.insert(val, n->get_expr());
+                expr* e = n->get_expr();
+                if (!m.is_value(e))
+                    m_value2expr.insert(val, e);
             }
         }
     }
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 73d8cad9d51..6537e638d55 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -330,27 +330,32 @@ namespace smt {
                 enode * n = curr.get_enode();
                 SASSERT(n->get_root() == n);
                 TRACE("mg_top_sort", tout << curr << "\n";);
-                dependencies.reset();
-                dependency_values.reset();
-                model_value_proc * proc = root2proc[n];
-                SASSERT(proc);
-                proc->get_dependencies(dependencies);
-                for (model_value_dependency const& d : dependencies) {
-                    if (d.is_fresh_value()) {
-                        CTRACE("mg_top_sort", !d.get_value()->get_value(), 
-                               tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
-                        SASSERT(d.get_value()->get_value());
-                        dependency_values.push_back(d.get_value()->get_value());
-                    }
-                    else {
-                        enode * child = d.get_enode();
-                        TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): " 
-                              << mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
-                        child = child->get_root();
-                        dependency_values.push_back(m_root2value[child]);
+                app* val = nullptr;
+                if (m.is_value(n->get_expr()))
+                    val = to_app(n->get_expr());
+                else {
+                    dependencies.reset();
+                    dependency_values.reset();
+                    model_value_proc * proc = root2proc[n];
+                    SASSERT(proc);
+                    proc->get_dependencies(dependencies);
+                    for (model_value_dependency const& d : dependencies) {
+                        if (d.is_fresh_value()) {
+                            CTRACE("mg_top_sort", !d.get_value()->get_value(), 
+                                   tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
+                            SASSERT(d.get_value()->get_value());
+                            dependency_values.push_back(d.get_value()->get_value());
+                        }
+                        else {
+                            enode * child = d.get_enode();
+                            TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): " 
+                                  << mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
+                            child = child->get_root();
+                            dependency_values.push_back(m_root2value[child]);
+                        }
                     }
+                    val = proc->mk_value(*this, dependency_values);
                 }
-                app * val = proc->mk_value(*this, dependency_values); 
                 register_value(val);
                 m_asts.push_back(val);
                 m_root2value.insert(n, val);