diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-05-03 16:36:48 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-03 16:36:48 -0700 |
| commit | 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 (patch) | |
| tree | 8c461783100ffd00fb3e8ad0a049482e64507d2a /src/parser/smt2/Smt2.g | |
| parent | 475a7de39316ee13bd279a090c30c52bc61978ce (diff) | |
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.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
1 files changed, 1 insertions, 1 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<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 */ |