From c8e3ab75dcd416026d4cd80b1e39971ee78cc9f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Mar 2023 06:23:17 +0100 Subject: [PATCH] fix unsoundness bug related to tracking equality assumptions outside of polysat Signed-off-by: Nikolaj Bjorner --- src/sat/smt/bv_polysat.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index a5375f7dc..0c8535e15 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -221,7 +221,7 @@ namespace bv { pdd p = var2pdd(r1); pdd q = var2pdd(r2); auto sc = m_polysat.eq(p, q); - m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); + m_var_eqs.setx(m_var_eqs_head, std::make_pair(r1, r2), std::make_pair(r1, r2)); ctx.push(value_trail(m_var_eqs_head)); m_polysat.assign_eh(sc, polysat::dependency(2 * m_var_eqs_head)); m_var_eqs_head++;