From 622b8431b3b52469db474b6de7f7062a60ebb3c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Mar 2023 08:26:42 +0100 Subject: [PATCH] use v1, v2 instead of r1, r2 (roots) to get narrower equality conflicts Signed-off-by: Nikolaj Bjorner --- src/sat/smt/bv_polysat.cpp | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index 0c8535e15..f0be25c82 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -218,10 +218,10 @@ namespace bv { if (!use_polysat()) return false; force_push(); - pdd p = var2pdd(r1); - pdd q = var2pdd(r2); + pdd p = var2pdd(v1); + pdd q = var2pdd(v2); auto sc = m_polysat.eq(p, q); - m_var_eqs.setx(m_var_eqs_head, std::make_pair(r1, r2), std::make_pair(r1, r2)); + m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); ctx.push(value_trail(m_var_eqs_head)); m_polysat.assign_eh(sc, polysat::dependency(2 * m_var_eqs_head)); m_var_eqs_head++; @@ -274,9 +274,12 @@ namespace bv { eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2))); } } - for (auto lit : core) { - VERIFY(s().value(lit) == l_true); - } + DEBUG_CODE( + for (auto lit : core) + VERIFY(s().value(lit) == l_true); + for (auto const& [a, b] : eqs) + VERIFY(var2enode(v1)->get_root() == var2enode(v2)->get_root()); + ); auto ex = mk_bv2ext_justification(core, eqs); ctx.set_conflict(ex); }