projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f01ff9c) | patch
Fix incorrect proof from ITE in circuit propagator (#7446)
authorGereon Kremer <nafur42@gmail.com>
Thu, 21 Oct 2021 16:33:23 +0000 (09:33 -0700)
committerGitHub <noreply@github.com>
Thu, 21 Oct 2021 16:33:23 +0000 (16:33 +0000)
commit8f4eacebff0ea1d9ed7a3d00e3cee03c1877a016
tree6cc6788b5209706d21a52a0e636acdadb0bfbc2ftree
parentf01ff9cf9d966a758ab60e186c0811bf59e57b72commit | diff
Fix incorrect proof from ITE in circuit propagator (#7446)

This PR fixes an incorrect proof in the circuit propagator related to back-propagation of an ite term.
Fixes cvc5/cvc5-projects#305.
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.smt2 [new file with mode: 0644] blob