From d777306bb6e4c89ebd9ccbc0a314c2071587a741 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Jan 2022 10:43:15 -0800 Subject: [PATCH] #5778 --- src/sat/sat_solver.cpp | 2 +- src/sat/smt/euf_internalize.cpp | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index c6d3ad3ae..90e31b97a 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3531,7 +3531,7 @@ namespace sat { for (unsigned i = old_num_vars; i < sz; ++i) { bool_var v = m_active_vars[i]; - if (is_visited(v) || is_active(v)) { + if (is_external(v) || is_visited(v) || is_active(v)) { m_vars_to_reinit.push_back(v); m_active_vars[j++] = v; m_var_scope[v] = new_lvl; diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index f6684c17a..6cc72eba5 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -182,11 +182,10 @@ namespace euf { } m_bool_var2expr[v] = e; - m_var_trail.push_back(v); + m_var_trail.push_back(v); enode* n = m_egraph.find(e); - if (!n) { + if (!n) n = mk_enode(e, 0, nullptr); - } SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v); m_egraph.set_bool_var(n, v); if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))