diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 51f342fe1..f6684c17a 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -167,12 +167,20 @@ namespace euf {
             lit = lit2;
         }
 
+        TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
         m_bool_var2expr.reserve(v + 1, nullptr);
         if (m_bool_var2expr[v] && m_egraph.find(e)) {
+            if (m_egraph.find(e)->bool_var() != v) {
+                IF_VERBOSE(0, verbose_stream()
+                 << "var " << v << "\n"
+                 << "found var " << m_egraph.find(e)->bool_var() << "\n"
+                 << mk_pp(m_bool_var2expr[v], m) << "\n"
+                 << mk_pp(e, m) << "\n");
+            }
             SASSERT(m_egraph.find(e)->bool_var() == v);
             return lit;
         }
-        TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
+
         m_bool_var2expr[v] = e;
         m_var_trail.push_back(v);
         enode* n = m_egraph.find(e);