Only push/pop around check-sat if it is associated with an assertion (#1525)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b2d43ac510c5f87058d53861b6f447e86e23830e..3c8d5e04a0c65d700cbb2ae97f66a420c1f6dd2a 100644 (file)
--- 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;