projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a158366) | patch
Fix issues with double negation in circuit propagator (#6669)
authorGereon Kremer <nafur42@gmail.com>
Wed, 2 Jun 2021 11:55:40 +0000 (13:55 +0200)
committerGitHub <noreply@github.com>
Wed, 2 Jun 2021 11:55:40 +0000 (11:55 +0000)
commit61b2694ac72d41aeff9c67e3631278e5a3bea5cb
tree1188888a726c908963fa55ffd332fe234b6eb8fdtree
parenta158366e1e7fdc76e00926393b9d091870e30badcommit | diff
Fix issues with double negation in circuit propagator (#6669)

This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.
src/theory/booleans/proof_circuit_propagator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/issue277-circuit-propagator.smt2 [new file with mode: 0644] blob