#5336

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))

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";

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; }

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);

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

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);