diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 0d820ad8b..d370ceed3 100644
--- 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
index 6a6b43650..d25df5b06 100644
--- 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) {