projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c54fe84) | patch
Fix unsat core proofs (#6655)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Jun 2021 15:28:36 +0000 (10:28 -0500)
committerGitHub <noreply@github.com>
Wed, 2 Jun 2021 15:28:36 +0000 (15:28 +0000)
commitec6fe33ab778a7bb5d2d016b799b1918b90fc338
treea870fea033a8cbf0761d7574c773b18e05f32a2etree
parentc54fe84863ce4257bd466a95ec42d7a6100d3c19commit | diff
Fix unsat core proofs (#6655)

Fixes cases of satisfiable unsat cores when proofs are enabled.

Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
src/smt/proof_manager.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/core/bitvec1.smtv1.smt2 diff | blob | history
test/regress/regress0/bv/core/bitvec3.smtv1.smt2 diff | blob | history
test/regress/regress0/bv/core/constant_core.smt2 diff | blob | history
test/regress/regress1/datatypes/dt-param-card4-unsat.smt2 diff | blob | history
test/regress/regress1/hole6.cvc diff | blob | history
test/regress/regress1/proofs/issue6625-unsat-core-proofs.smt2 [new file with mode: 0644] blob
test/regress/regress1/proofs/unsat-cores-proofs.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/sets-disequal.smt2 diff | blob | history