diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b2d43ac51..3c8d5e04a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4702,17 +4702,19 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ d_needPostsolve = false; } - // Push the context - internalPush(); - // Note that a query has been made d_queryMade = true; // reset global negation d_globalNegation = false; + bool didInternalPush = false; // Add the formula if(!e.isNull()) { + // Push the context + internalPush(); + didInternalPush = true; + d_problemExtended = true; Expr ea = isQuery ? e.notExpr() : e; if(d_assertionList != NULL) { @@ -4763,7 +4765,10 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ } // Pop the context - internalPop(); + if (didInternalPush) + { + internalPop(); + } // Remember the status d_status = r; |