diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-01-21 20:06:58 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-21 20:06:58 -0600 |
commit | be9484dc7f7db5e4301142ccfe493871d9f7eac8 (patch) | |
tree | 62ac1cf68934dff8a6ed350dc11ba2fcc2ea9071 /src | |
parent | 248b977790b429ebfd22481462193e3e35c57ce2 (diff) |
Only push/pop around check-sat if it is associated with an assertion (#1525)
Diffstat (limited to 'src')
-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; |