projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b830fb6) | patch
Reset assertions on resetAssertions (#5153)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 29 Sep 2020 03:56:20 +0000 (22:56 -0500)
committerGitHub <noreply@github.com>
Tue, 29 Sep 2020 03:56:20 +0000 (22:56 -0500)
commit8a20cee891d1fb820ed04f08c1fd0999b619ea8b
treeeec2abe9f2d8014c4800abf8f4b821d2296689betree
parentb830fb6747b5a5304100217e91481d9cc6c4f1c5commit | diff
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 diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/issue5144-resetAssertions.smt2 [new file with mode: 0644] blob