From e4ef1717e3a7b30fc87a4959dd80195a519721a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Sep 2022 23:26:31 -0700 Subject: [PATCH] fix variable tracking bug in explanations with literals --- src/sat/smt/euf_internalize.cpp | 2 +- src/sat/smt/euf_proof.cpp | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 8b8c7da74..96167b39f 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -167,7 +167,7 @@ namespace euf { lit = lit2; } - TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";); + TRACE("euf", tout << "attach v" << 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) { diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 6c90b3c66..bcbc9439b 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -83,10 +83,11 @@ namespace euf { expr_ref_vector eqs(m); unsigned nv = s().num_vars(); auto add_lit = [&](enode_pair const& eq) { + unsigned v = nv; ++nv; eqs.push_back(m.mk_eq(eq.first->get_expr(), eq.second->get_expr())); - set_tmp_bool_var(nv, eqs.back()); - return literal(nv, false); + set_tmp_bool_var(v, eqs.back()); + return literal(v, false); }; for (auto lit : euf::th_explain::lits(jst))