diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 781a94c85..a6e58c6d1 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -214,6 +214,14 @@ 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);
     }