From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 29 Sep 2020 03:56:20 +0000 (-0500)
Subject: Reset assertions on resetAssertions (#5153)
X-Git-Tag: cvc5-1.0.0~2793
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a20cee891d1fb820ed04f08c1fd0999b619ea8b;p=cvc5.git

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 caf098cb8..3caf03946 100644
--- 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 257a70c80..7d29db744 100644
--- 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
index 000000000..b55177a6a
--- /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)