From 05c5f72ca1dd6a2e8b31ebc38cfe8a6c9004955b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Nov 2020 11:25:36 -0800 Subject: [PATCH] fix #4829 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_consequences.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index d6d9fa3d6..477b8a8b3 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -282,18 +282,21 @@ namespace smt { m_var2val.reset(); m_var2orig.reset(); m_assumption2orig.reset(); + bool pushed = false; struct scoped_level { context& c; unsigned lvl; - scoped_level(context& c): - c(c), lvl(c.get_scope_level()) {} + bool& pushed; + scoped_level(context& c, bool& pushed): + c(c), pushed(pushed), lvl(c.get_scope_level()) {} ~scoped_level() { - if (c.get_scope_level() > lvl) - c.pop_scope(c.get_scope_level() - lvl); + if (c.get_scope_level() > lvl + pushed) + c.pop_scope(c.get_scope_level() - lvl - pushed); + if (pushed) + c.pop(1); } }; - scoped_level _lvl(*this); - bool pushed = false; + scoped_level _lvl(*this, pushed); for (expr* v : vars0) { if (is_uninterp_const(v)) { @@ -328,6 +331,7 @@ namespace smt { } lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); + if (is_sat != l_true) { TRACE("context", tout << is_sat << "\n";); return is_sat;