Reset assertions on resetAssertions (#5153)

The assertions object is currently not cleared on resetAssertions, only the prop engine is reset. This means that if a user added assertion, did not use them in a check-sat, and then called reset-assertions, they would not be removed from the assertions pipeline (storing the pending assertions before they are sent to the prop engine).

This fixes #5144.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index caf098cb85888bfd01113f93b5b025ea8509f345..3caf03946b130a13b6094de7f3a73d58a07b1afc 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2028,6 +2028,7 @@ void SmtEngine::resetAssertions()
         getOutputManager().getDumpOut());
   }
 
+  d_asserts->clearCurrent();
   d_state->notifyResetAssertions();
   d_dumpm->resetAssertions();
   // push the state to maintain global context around everything

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 257a70c80282a54dde113434d0e6fcffbcd80970..7d29db744b09860e0abab3f7d5c1ef71da5227e7 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -576,6 +576,7 @@ set(regress_0_tests
   regress0/issue2832-qualId.smt2
   regress0/issue4010-sort-inf-var.smt2
   regress0/issue4469-unc-no-reuse-var.smt2
+  regress0/issue5144-resetAssertions.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
   regress0/ite3.smt2

diff --git a/test/regress/regress0/issue5144-resetAssertions.smt2 b/test/regress/regress0/issue5144-resetAssertions.smt2
new file mode 100644 (file)
index 0000000..b55177a
--- /dev/null
+++ b/test/regress/regress0/issue5144-resetAssertions.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(set-info :status sat)
+(assert (= 0 1))
+(reset-assertions)
+(check-sat)