Fix redundant internalPush calls. (#1865)
authorMathias Preiner <mathias.preiner@gmail.com>
Thu, 3 May 2018 23:36:48 +0000 (16:36 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Thu, 3 May 2018 23:36:48 +0000 (16:36 -0700)
commit2cc0e2c6a691fb6d30ed8879832b49bc1f277d77
tree8c461783100ffd00fb3e8ad0a049482e64507d2a
parent475a7de39316ee13bd279a090c30c52bc61978ce
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
src/smt/smt_engine.cpp