From 8a20cee891d1fb820ed04f08c1fd0999b619ea8b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 28 Sep 2020 22:56:20 -0500 Subject: [PATCH] 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. --- src/smt/smt_engine.cpp | 1 + test/regress/CMakeLists.txt | 1 + test/regress/regress0/issue5144-resetAssertions.smt2 | 5 +++++ 3 files changed, 7 insertions(+) create mode 100644 test/regress/regress0/issue5144-resetAssertions.smt2 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) -- 2.30.2