From 1ba86c8ce3598922de188d0c0dd232b534070875 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Mar 2023 08:38:10 +0100 Subject: [PATCH] fixup assertion Signed-off-by: Nikolaj Bjorner --- src/sat/smt/bv_polysat.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index f0be25c82..bda4362af 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -277,8 +277,8 @@ namespace bv { 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()); + for (auto const& [n1, n2] : eqs) + VERIFY(n1->get_root() == n2->get_root()); ); auto ex = mk_bv2ext_justification(core, eqs); ctx.set_conflict(ex);