re-enable delayed literal propagation

Z3Prover · Nov 29, 2023 · 2f01b5b · 2f01b5b
1 parent 4289cfa
commit 2f01b5b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
@@ -83,7 +83,7 @@ namespace euf {
     void egraph::reinsert_equality(enode* p) {
         SASSERT(p->is_equality());
         if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) 
-            add_literal(p, nullptr);
+            queue_literal(p, nullptr);
     }
 
     void egraph::queue_literal(enode* p, enode* ante) {

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -1059,6 +1059,7 @@ namespace euf {
         };
         r->m_egraph.copy_from(m_egraph, copy_justification);        
         r->set_solver(s);
+        r->m_egraph.copy_from(m_egraph, copy_justification);        
         for (euf::enode* n : r->m_egraph.nodes()) {
             auto b = n->bool_var();
             if (b != sat::null_bool_var) {