projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8f4eace) | patch
Add regression (#7447)
authorGereon Kremer <nafur42@gmail.com>
Thu, 21 Oct 2021 16:48:47 +0000 (09:48 -0700)
committerGitHub <noreply@github.com>
Thu, 21 Oct 2021 16:48:47 +0000 (16:48 +0000)
commit109f17375661cc29f8125d289c4a776514c23e33
tree8e7518359b64475d64930e314985e902c65a15bdtree
parent8f4eacebff0ea1d9ed7a3d00e3cee03c1877a016commit | diff
Add regression (#7447)

This PR fixes a proof for an xor term that failed to eliminate a double negation.

Fixes cvc5/cvc5-projects#304
src/theory/booleans/proof_circuit_propagator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 [new file with mode: 0644] blob