projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0dfbf4b) | patch
[proof] Fixing CHAIN_RESOLUTION checker (#7465)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 22 Oct 2021 22:08:27 +0000 (19:08 -0300)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 22:08:27 +0000 (22:08 +0000)
commitd442be84a2e47ccc6b3b91dbcf5ae2c1b891049b
tree6ace93ab05d78dd1d10eef9af193e40f05110a6dtree
parent0dfbf4b80f25bc9edd1c843ba9a9bb37bace79a9commit | diff
[proof] Fixing CHAIN_RESOLUTION checker (#7465)

Previously the checker was doing things in a smart way that could lead to issues when a clause coincided with a singleton clause as a literal of another clause within the chain.

Fixes cvc5/cvc5-projects#310
src/smt/proof_post_processor.cpp diff | blob | history
src/theory/booleans/proof_checker.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 [new file with mode: 0644] blob