mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fix #4829

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-28 11:25:36 -08:00
parent 17f04099a5
commit 05c5f72ca1
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/smt_consequences.cpp
View file

@ -282,18 +282,21 @@ namespace smt {
m_var2val.reset(); m_var2val.reset();
m_var2orig.reset(); m_var2orig.reset();
m_assumption2orig.reset(); m_assumption2orig.reset();
bool pushed = false;
struct scoped_level { struct scoped_level {
context& c; context& c;
unsigned lvl; unsigned lvl;
scoped_level(context& c): bool& pushed;
c(c), lvl(c.get_scope_level()) {} scoped_level(context& c, bool& pushed):
c(c), pushed(pushed), lvl(c.get_scope_level()) {}
~scoped_level() { ~scoped_level() {
if (c.get_scope_level() > lvl) if (c.get_scope_level() > lvl + pushed)
c.pop_scope(c.get_scope_level() - lvl); c.pop_scope(c.get_scope_level() - lvl - pushed);
if (pushed)
c.pop(1);
} }
}; };
scoped_level _lvl(*this); scoped_level _lvl(*this, pushed);
bool pushed = false;
for (expr* v : vars0) { for (expr* v : vars0) {
if (is_uninterp_const(v)) { if (is_uninterp_const(v)) {
@ -328,6 +331,7 @@ namespace smt {
} }
lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
if (is_sat != l_true) { if (is_sat != l_true) {
TRACE("context", tout << is_sat << "\n";); TRACE("context", tout << is_sat << "\n";);
return is_sat; return is_sat;