mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

fix #2396

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-12 17:36:30 -04:00
parent 0bca2aabff
commit 26c1c744aa
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/nlsat/nlsat_solver.cpp
View file

@ -473,6 +473,7 @@ namespace nlsat {
}
void del(bool_var b) {
TRACE("nlsat", tout << "del " << b << "\n";);
SASSERT(m_bwatches[b].empty());
//SASSERT(m_bvalues[b] == l_undef);
m_num_bool_vars--;

7
src/qe/nlqsat.cpp
View file

@ -93,9 +93,9 @@ namespace qe {
check_cancel();
init_assumptions();
lbool res = m_solver.check(m_asms);
TRACE("qe", display(tout); );
switch (res) {
case l_true:
TRACE("qe", display(tout); );
save_model();
push();
break;
@ -306,6 +306,7 @@ namespace qe {
}
nlsat::literal l(v, false);
m_preds[k].push_back(l);
m_solver.inc_ref(v);
m_bvar2level.insert(v, level);
TRACE("qe", m_solver.display(tout, l); tout << ": " << level << "\n";);
}
@ -412,6 +413,7 @@ namespace qe {
nlsat::bool_var b = m_solver.mk_bool_var();
clause.push_back(nlsat::literal(b, true));
m_assumptions.push_back(nlsat::literal(b, false));
m_solver.inc_ref(b);
m_asm2fml.insert(b, fml);
m_trail.push_back(fml);
m_bvar2level.insert(b, max_level());
@ -562,6 +564,9 @@ namespace qe {
m_bound_rvars.reset();
m_bound_bvars.reset();
m_preds.reset();
for (auto const& kv : m_bvar2level) {
m_solver.dec_ref(kv.m_key);
}
m_rvar2level.reset();
m_bvar2level.reset();
m_t2x.reset();