From be9484dc7f7db5e4301142ccfe493871d9f7eac8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 21 Jan 2018 20:06:58 -0600
Subject: [PATCH] Only push/pop around check-sat if it is associated with an
 assertion (#1525)

---
 src/smt/smt_engine.cpp | 13 +++++++++----
 1 file 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;
-- 
2.30.2