projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f83a753) | patch
Fix bv assert input reset assertions (#6820)
authorMathias Preiner <mathias.preiner@gmail.com>
Fri, 2 Jul 2021 22:13:17 +0000 (15:13 -0700)
committerGitHub <noreply@github.com>
Fri, 2 Jul 2021 22:13:17 +0000 (22:13 +0000)
commitde0401e53e4baab30a5e78d5bd51048348b1e1ce
tree0f1697a82a4c839b5fd7a365ce3c5777c741c70ftree
parentf83a753ad62a005085c47a7c0f4ba2e406d9acd7commit | diff
Fix bv assert input reset assertions (#6820)

If reset-assertions was called it will now reset the SAT solver and the
CNF stream if clauses were permanently added to the SAT solver via
option --bv-assert-input.
src/theory/bv/bv_solver_bitblast.cpp diff | blob | history
src/theory/bv/bv_solver_bitblast.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/reset-assertions-assert-input.smt2 [new file with mode: 0644] blob