diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index ea13ba398..d6926566a 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -141,8 +141,7 @@ namespace euf { } m_bool_var2expr.reserve(v + 1, nullptr); - if (m_bool_var2expr[v]) { - SASSERT(m_egraph.find(e)); + if (m_bool_var2expr[v] && m_egraph.find(e)) { SASSERT(m_egraph.find(e)->bool_var() == v); return lit; }