projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c4ebca0) | patch
Fix another double negation proof issue (#7468)
authorGereon Kremer <nafur42@gmail.com>
Fri, 22 Oct 2021 21:37:54 +0000 (14:37 -0700)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 21:37:54 +0000 (21:37 +0000)
commitf1db161860d0283cb5537ad8847e0b52d1485e28
treea001059ece760bea3f1180e17819209bcb84f33ctree
parentc4ebca0e668e83f330cbb777a90c6b02b1c47eb9commit | diff
Fix another double negation proof issue (#7468)

This PR fixes another subtle proof issue in the circuit propagator concerning negated ites.
Fixes cvc5/cvc5-projects#309.
src/theory/booleans/proof_circuit_propagator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 [new file with mode: 0644] blob