diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index fd93ce943..691c42981 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -818,9 +818,13 @@ namespace euf {
                 args.push_back(old_expr2new_enode[n1->get_arg(j)->get_expr_id()]);
             expr*  e2 = tr(e1);
             enode* n2 = mk(e2, n1->generation(), args.size(), args.data());
+            
             old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
-            n2->set_value(n2->value());
+            n2->set_value(n1->value());
             n2->m_bool_var = n1->m_bool_var;
+            n2->m_commutative = n1->m_commutative;
+            n2->m_merge_enabled = n1->m_merge_enabled;
+            n2->m_is_equality = n1->m_is_equality;            
         }
         for (unsigned i = 0; i < src.m_nodes.size(); ++i) {             
             enode* n1 = src.m_nodes[i];
diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index 73405b77e..8498c9790 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -55,17 +55,17 @@ namespace euf {
         unsigned      m_table_id = UINT_MAX;       
         unsigned      m_generation = 0;         // Tracks how many quantifier instantiation rounds were needed to generate this enode.
         enode_vector  m_parents;
-        enode* m_next   = nullptr;
-        enode* m_root   = nullptr;
-        enode* m_target = nullptr;
-        enode* m_cg     = nullptr;
+        enode*        m_next   = nullptr;
+        enode*        m_root   = nullptr;
+        enode*        m_target = nullptr;
+        enode*        m_cg     = nullptr;
         th_var_list   m_th_vars;
         justification m_justification;
         unsigned      m_num_args = 0;
-        signed char         m_lbl_hash = -1;  // It is different from -1, if enode is used in a pattern
-        approx_set          m_lbls;
-        approx_set          m_plbls;
-        enode* m_args[0];
+        signed char   m_lbl_hash = -1;  // It is different from -1, if enode is used in a pattern
+        approx_set    m_lbls;
+        approx_set    m_plbls;
+        enode*        m_args[0];
 
         friend class enode_args;
         friend class enode_parents;
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index e10225c9c..53fda2a2f 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -316,6 +316,7 @@ namespace euf {
         }
         if (n->is_equality()) {
             SASSERT(!m.is_iff(e));
+            SASSERT(m.is_eq(e));
             if (sign)
                 m_egraph.new_diseq(n);
             else                 
@@ -867,9 +868,9 @@ namespace euf {
         for (euf::enode* n : r->m_egraph.nodes()) {
             auto b = n->bool_var();
             if (b != sat::null_bool_var) {
-                m_bool_var2expr.setx(b, n->get_expr(), nullptr);
+                r->m_bool_var2expr.setx(b, n->get_expr(), nullptr);
                 SASSERT(r->m.is_bool(n->get_sort()));
-                IF_VERBOSE(11, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
+                IF_VERBOSE(11, verbose_stream() << "set bool_var " << b << " " << r->bpp(n) << " " << mk_bounded_pp(n->get_expr(), m) << "\n");
             }
         }
         for (auto* s_orig : m_id2solver) {