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 74f8e71d3270ffe89e9f8a9928196d3a9ee76106..5afb2c3169e4b79217d3257872a0963ee189cf18 100644 (file)
--- 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 0cff9c8fa8618af18d9aa54ae0da1583794d9e98..c1e8596cf958de441704ee347bff04759e06a6d9 100644 (file)
--- 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);