projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bcaebfa) | patch
Fix issue with reset-assertions. (#3988)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 10 Mar 2020 21:51:32 +0000 (14:51 -0700)
committerGitHub <noreply@github.com>
Tue, 10 Mar 2020 21:51:32 +0000 (14:51 -0700)
commite9f4cec2cad02e270747759223090c16b9d2d44c
treeff902073b926d48cb0ae23848bee4b90e96000c7tree
parentbcaebfa163bb27e1cf14c0f763afb47b185a5f99commit | diff
Fix issue with reset-assertions. (#3988)

Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
14 files changed:
src/decision/justification_heuristic.cpp diff | blob | history
src/decision/justification_heuristic.h diff | blob | history
src/preprocessing/preprocessing_pass_context.h diff | blob | history
src/prop/minisat/minisat.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/sat_solver.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/util/statistics_registry.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/reset-assertions.smt2 [deleted file] blob | history
test/regress/regress0/smtlib/reset-assertions-global.smt2 [new file with mode: 0644] blob
test/regress/regress0/smtlib/reset-assertions1.smt2 [new file with mode: 0644] blob
test/regress/regress0/smtlib/reset-assertions2.smt2 [new file with mode: 0644] blob