projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2da1033) | patch
Fix symmetric proof issue for ITE in circuit propagator (#7452)
authorGereon Kremer <nafur42@gmail.com>
Thu, 21 Oct 2021 19:10:26 +0000 (12:10 -0700)
committerGitHub <noreply@github.com>
Thu, 21 Oct 2021 19:10:26 +0000 (19:10 +0000)
commitf3bf9af12eb6af487e61c585fa9639f1d1485220
tree8cae4300799cb7a102fb51acfb273a00eec8fe45tree
parent2da1033d731495b4925087f06a082a81cadf97a9commit | diff
Fix symmetric proof issue for ITE in circuit propagator (#7452)

This PR goes back to #7446 and implements a proper fix that handles both symmetrical cases.
src/theory/booleans/proof_circuit_propagator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 [new file with mode: 0644] blob
test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 [new file with mode: 0644] blob
test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 [deleted file] blob | history