mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

m_var2pdd entries may need to change pdd manager

Browse source
This commit is contained in:
Jakob Rath 2023-05-29 15:46:01 +02:00
parent 129039dc52
commit 52c4716636
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/bv_polysat.cpp
View file

@ -323,14 +323,15 @@ namespace bv {
} }
void solver::polysat_set(euf::theory_var v, pdd const& p) { 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.reserve(get_num_vars(), p);
m_var2pdd_valid.reserve(get_num_vars(), false); m_var2pdd_valid.reserve(get_num_vars(), false);
ctx.push(set_bitvector_trail(m_var2pdd_valid, v)); ctx.push(set_bitvector_trail(m_var2pdd_valid, v));
m_var2pdd[v].reset(p.manager());
m_var2pdd[v] = p; 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) { void solver::polysat_pop(unsigned n) {