From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 3 May 2018 23:36:48 +0000 (-0700)
Subject: Fix redundant internalPush calls. (#1865)
X-Git-Tag: cvc5-1.0.0~5094
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2cc0e2c6a691fb6d30ed8879832b49bc1f277d77;p=cvc5.git

Fix redundant internalPush calls. (#1865)

The SMT2 parser by default passes a true expression to the CheckSatCommand,
which results in checkSatisfiability (in SmtEngine) to always do an internal
push. As a consequence, the work of each check-sat was reset even though no
user level push/pop happened.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 74f8e71d3..5afb2c316 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -454,7 +454,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
               "permitted while operating in strict compliance mode.");
         }
       }
-    | { expr = MK_CONST(bool(true)); }
+    | { expr = Expr(); }
     )
     { cmd->reset(new CheckSatCommand(expr)); }
   | /* check-sat-assuming */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0cff9c8fa..c1e8596cf 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4530,6 +4530,12 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       d_assumptions = assumptions;
     }
 
+    if (!d_assumptions.empty())
+    {
+      internalPush();
+      didInternalPush = true;
+    }
+
     Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
     for (Expr e : d_assumptions)
     {
@@ -4540,8 +4546,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       ensureBoolean(e);
 
       /* Add assumption  */
-      internalPush();
-      didInternalPush = true;
       if (d_assertionList != NULL)
       {
         d_assertionList->push_back(e);