From 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 3 May 2018 16:36:48 -0700 Subject: [PATCH] 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. --- src/parser/smt2/Smt2.g | 2 +- src/smt/smt_engine.cpp | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) 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* 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& 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& assumptions, ensureBoolean(e); /* Add assumption */ - internalPush(); - didInternalPush = true; if (d_assertionList != NULL) { d_assertionList->push_back(e); -- 2.30.2