From ed9341e3b017973555f18dca4a2d218f8501efec Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 17 Jun 2021 17:45:13 -0700
Subject: [PATCH] #5336

---
 src/ast/euf/euf_egraph.cpp        | 2 +-
 src/sat/smt/arith_diagnostics.cpp | 2 +-
 src/sat/smt/arith_solver.h        | 2 +-
 src/sat/smt/euf_internalize.cpp   | 1 +
 src/sat/smt/euf_solver.h          | 1 +
 src/sat/smt/q_mbi.cpp             | 1 +
 6 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 809cbe1f94a..2bc9b1cde72 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -745,7 +745,7 @@ namespace euf {
             out << "] ";
         }
         if (n->value() != l_undef) 
-            out << "[v" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
+            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
         if (n->has_th_vars()) {
             out << "[t";
             for (auto v : enode_th_vars(n))
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 770aeff981f..b639c183fef 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -50,7 +50,7 @@ namespace arith {
                     scoped_anum an(m_nla->am());
                     m_nla->am().display(out << " = ", nl_value(v, an));
                 }
-                else if (can_get_value(v))  
+                else if (can_get_value(v) && !m_solver->has_changed_columns())  
                     out << " = " << get_value(v);
                 if (is_int(v)) 
                     out << ", int";
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 19164dff665..b449e049e2f 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -384,7 +384,7 @@ namespace arith {
 
         obj_map<expr, expr*>      m_predicate2term;
         obj_map<expr, bound_info> m_term2bound_info;
-        bool                      m_model_is_initialized{ false };
+        bool                      m_model_is_initialized = false;
 
         unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; }
         bool propagate_eqs() const { return get_config().m_arith_propagate_eqs && m_num_conflicts < get_config().m_arith_propagation_threshold; }
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 1eb9d6aefe9..0a7aa717fb2 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -278,6 +278,7 @@ namespace euf {
             }
             else {
                 sat::bool_var v = si.to_bool_var(c);
+                s().set_external(v);
                 VERIFY(v != sat::null_bool_var);
                 VERIFY(s().is_external(v));
                 SASSERT(v != sat::null_bool_var);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index ac8c41d5916..73c44649c26 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -352,6 +352,7 @@ namespace euf {
         sat::literal attach_lit(sat::literal lit, expr* e);
         void unhandled_function(func_decl* f);
         th_rewriter& get_rewriter() { return m_rewriter; }
+        void rewrite(expr_ref& e) { m_rewriter(e); }
         bool is_shared(euf::enode* n) const;
 
         // relevancy
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index bf44b5dd27a..30c6c7e23bc 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -213,6 +213,7 @@ namespace q {
         sat::literal qlit = ctx.expr2literal(q);
         if (is_exists(q))
             qlit.neg();
+        ctx.rewrite(proj);
         TRACE("q", tout << "project: " << proj << "\n";);
         ++m_stats.m_num_instantiations;        
         unsigned generation = ctx.get_max_generation(proj);