From 52c471663658c3f7d9af6389be2b9137a9f63ddb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 29 May 2023 15:46:01 +0200 Subject: [PATCH] m_var2pdd entries may need to change pdd manager --- src/sat/smt/bv_polysat.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index 50161f046..e529d66ba 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -323,14 +323,15 @@ namespace bv { } void solver::polysat_set(euf::theory_var v, pdd const& p) { +#ifndef NDEBUG + expr* e = var2enode(v)->get_expr(); + verbose_stream() << "polysat_set: " << expr_ref(e, m) << " -> " << p << std::endl; +#endif m_var2pdd.reserve(get_num_vars(), p); m_var2pdd_valid.reserve(get_num_vars(), false); ctx.push(set_bitvector_trail(m_var2pdd_valid, v)); + m_var2pdd[v].reset(p.manager()); m_var2pdd[v] = p; -#ifndef NDEBUG - // expr* e = var2enode(v)->get_expr(); - // std::cerr << "polysat_set: " << mk_ismt2_pp(e, m) << " -> " << p << std::endl; -#endif } void solver::polysat_pop(unsigned n) {