From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Jan 2018 02:06:58 +0000 (-0600)
Subject: Only push/pop around check-sat if it is associated with an assertion (#1525)
X-Git-Tag: cvc5-1.0.0~5352
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be9484dc7f7db5e4301142ccfe493871d9f7eac8;p=cvc5.git

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 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;