diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-21 09:33:23 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-21 16:33:23 +0000 |
| commit | 8f4eacebff0ea1d9ed7a3d00e3cee03c1877a016 (patch) | |
| tree | 6cc6788b5209706d21a52a0e636acdadb0bfbc2f /test/regress/regress0/preprocess | |
| parent | f01ff9cf9d966a758ab60e186c0811bf59e57b72 (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.
Diffstat (limited to 'test/regress/regress0/preprocess')
| -rw-r--r-- | test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 new file mode 100644 index 000000000..6760bdf4d --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-const x Bool) +(declare-const y Bool) +(declare-const z Bool) +(assert y) +(assert (not z)) +(assert (ite x y z)) +(check-sat)
\ No newline at end of file |