diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index bbb63540e..2a0159265 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -417,14 +417,7 @@ namespace euf {
             std::swap(r1, r2);
             std::swap(n1, n2);
         }
-        if (m.is_false(r2->get_expr()) && r1->value() == l_true) {
-            set_conflict(n1, n2, j);
-            return;
-        }
-        if (m.is_true(r2->get_expr()) && r1->value() == l_false) {
-            set_conflict(n1, n2, j);
-            return;
-        }
+
         if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
             add_literal(n1, false);
         if (n1->is_equality() && n1->value() == l_false)
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index a6e58c6d1..cbdc44743 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -214,14 +214,6 @@ namespace euf {
         TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";);
         DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
 
-#if 0
-        if (r.size() == 5 && r[0] == literal(401, true) && r[1] == literal(259, false) && r[2] == literal(250, false) &&
-            r[3] == literal(631, false) && r[4] == literal(639, false)) {
-            TRACE("euf", s().display(tout););
-            exit(0);
-        }
-#endif
-
         if (!probing)
             log_antecedents(l, r);
     }
@@ -311,19 +303,20 @@ namespace euf {
 	    if (n->value_conflict()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
+            return;
 	    }
-        else if (!sign && n->is_equality()) {
+        if (n->merge_tf()) {
+            euf::enode* nb = sign ? mk_false() : mk_true();
+            m_egraph.merge(n, nb, c);
+        }
+        if (!sign && n->is_equality()) {
             SASSERT(!m.is_iff(e));
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
             m_egraph.merge(na, nb, c);
         }
-        else if (n->merge_tf()) {
-            euf::enode* nb = sign ? mk_false() : mk_true();
-            m_egraph.merge(n, nb, c);
-        }
-        else if (sign && n->is_equality()) 
-            m_egraph.new_diseq(n);        
+        else if (sign && n->is_equality())
+            m_egraph.new_diseq(n);      
     }