From 3021da87cf72b446bebc3d281545ac786f11f79c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Sep 2021 21:10:26 -0700
Subject: [PATCH] #5532

---
 src/sat/smt/arith_solver.cpp    | 11 +++++++++++
 src/sat/smt/euf_internalize.cpp | 30 ++++++++++++++++++++++++++----
 src/sat/smt/euf_solver.h        |  3 ++-
 3 files changed, 39 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 2f9c44cc880..7c8eb3e776b 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -581,6 +581,17 @@ namespace arith {
                 value = ~value;
             if (!found_bad && value == get_phase(n->bool_var()))
                 continue;
+
+            TRACE("arith",
+                ptr_vector<expr> nodes;
+                nodes.push_back(n->get_expr());
+                for (unsigned i = 0; i < nodes.size(); ++i) {
+                    expr* r = nodes[i];
+                    if (is_app(r))
+                        for (expr* arg : *to_app(r))
+                            nodes.push_back(arg);
+                    tout << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << " := " << mdl(r) << "\n";
+                });
             TRACE("arith",
                 tout << eval << " " << value << " " << ctx.bpp(n) << "\n";
                 tout << mdl << "\n";
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index f6240993cbf..11756e9f8fd 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -85,7 +85,7 @@ namespace euf {
         if (auto* s = expr2solver(e))
             s->internalize(e, m_is_redundant);            
         else 
-            attach_node(m_egraph.mk(e, m_generation, 0, nullptr));        
+            attach_node(mk_enode(e, 0, nullptr));        
         return true;
     }
 
@@ -100,7 +100,7 @@ namespace euf {
         if (auto* s = expr2solver(e)) 
             s->internalize(e, m_is_redundant);        
         else 
-            attach_node(m_egraph.mk(e, m_generation, num, m_args.data()));        
+            attach_node(mk_enode(e, num, m_args.data()));        
         return true;
     }
 
@@ -159,7 +159,7 @@ namespace euf {
         m_var_trail.push_back(v);
         enode* n = m_egraph.find(e);
         if (!n) {
-            n = m_egraph.mk(e, m_generation, 0, nullptr);
+            n = mk_enode(e, 0, nullptr);
         }
         SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
         m_egraph.set_bool_var(n, v);
@@ -263,7 +263,7 @@ namespace euf {
             for (unsigned i = 0; i < sz; ++i) {
                 expr_ref fapp(m.mk_app(f, e->get_arg(i)), m);
                 expr_ref fresh(m.mk_fresh_const("dist-value", u), m);
-                enode* n = m_egraph.mk(fresh, m_generation, 0, nullptr);
+                enode* n = mk_enode(fresh, 0, nullptr);
                 n->mark_interpreted();
                 expr_ref eq = mk_eq(fapp, fresh);
                 sat::literal lit = mk_literal(eq);
@@ -429,4 +429,26 @@ namespace euf {
         return n;
     }
 
+    euf::enode* solver::mk_enode(expr* e, unsigned n, enode* const* args) { 
+        euf::enode* r = m_egraph.mk(e, m_generation, n, args); 
+        for (unsigned i = 0; i < n; ++i)
+            ensure_merged_tf(args[i]);
+        return r;
+    }
+
+    void solver::ensure_merged_tf(euf::enode* n) {
+        switch (n->value()) {
+        case l_undef:
+            break;
+        case l_true:
+            if (n->get_root() != mk_true())
+                m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
+            break;
+        case l_false:
+            if (n->get_root() != mk_false())
+                m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var())));
+            break;
+        }
+    }
+
 }
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 218c605e6cd..6d08ba51222 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -127,6 +127,7 @@ namespace euf {
         void add_not_distinct_axiom(app* e, euf::enode* const* args);
         void axiomatize_basic(enode* n);
         bool internalize_root(app* e, bool sign, ptr_vector<enode> const& args);
+        void ensure_merged_tf(euf::enode* n);
         euf::enode* mk_true();
         euf::enode* mk_false();
 
@@ -349,7 +350,7 @@ namespace euf {
         expr_ref mk_eq(expr* e1, expr* e2);
         expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); }
         euf::enode* e_internalize(expr* e);
-        euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, m_generation, n, args); }
+        euf::enode* mk_enode(expr* e, unsigned n, enode* const* args);
         expr* bool_var2expr(sat::bool_var v) const { return m_bool_var2expr.get(v, nullptr); }
         expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return (e && lit.sign()) ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
         unsigned generation() const { return m_generation; }