#5454

src/ast/euf/euf_egraph.cpp

@@ -118,14 +118,14 @@ namespace euf {
             n->set_is_equality();
             update_children(n);
             reinsert_equality(n);
-            return n;
         }
-        enode_bool_pair p = insert_table(n);
-        enode* n2 = p.first;
-        if (n2 == n) 
-            update_children(n);        
-        else 
-            merge(n, n2, justification::congruence(p.second));        
+        else {
+            auto [n2, comm] = insert_table(n);
+            if (n2 == n) 
+                update_children(n);        
+            else 
+                merge(n, n2, justification::congruence(comm));
+        }
         return n;
     }
 
@@ -266,6 +266,11 @@ namespace euf {
         if (enable_merge != n->merge_enabled()) {
             toggle_merge_enabled(n);
             m_updates.push_back(update_record(n, update_record::toggle_merge()));
+            if (enable_merge && n->num_args() > 0) {
+                auto [n2, comm] = insert_table(n);
+                if (n2 != n) 
+                    merge(n, n2, justification::congruence(comm));                        
+            }
         }
     }
 
@@ -403,7 +408,7 @@ namespace euf {
         if (r1 == r2)
             return;
 
-        TRACE("euf", j.display(tout << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
+        TRACE("euf", j.display(tout << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n" << bpp(r1) << " " << bpp(r2) << "\n";);
         IF_VERBOSE(20, j.display(verbose_stream() << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
         force_push();
         SASSERT(m_num_scopes == 0);
@@ -457,12 +462,13 @@ namespace euf {
             if (!p->is_marked1())
                 continue;
             p->unmark1();
+            TRACE("euf", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->merge_enabled() << "\n";);
             if (p->merge_enabled()) {
-                auto rc = insert_table(p);
-                enode* p_other = rc.first;
+                auto [p_other, comm] = insert_table(p);
                 SASSERT(m_table.contains_ptr(p) == (p_other == p));
+                TRACE("euf", tout << "other " << bpp(p_other) << "\n";);
                 if (p_other != p) 
-                    m_to_merge.push_back(to_merge(p_other, p, rc.second));                
+                    m_to_merge.push_back(to_merge(p_other, p, comm));                
                 else
                     r2->m_parents.push_back(p);
                 if (p->is_equality())
@@ -752,7 +758,7 @@ namespace euf {
             out << "] ";
         }
         if (n->value() != l_undef) 
-            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
+            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] ";
         if (n->has_th_vars()) {
             out << "[t";
             for (auto v : enode_th_vars(n))