diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-22 14:37:54 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-22 21:37:54 +0000 |
| commit | f1db161860d0283cb5537ad8847e0b52d1485e28 (patch) | |
| tree | a001059ece760bea3f1180e17819209bcb84f33c /test | |
| parent | c4ebca0e668e83f330cbb777a90c6b02b1c47eb9 (diff) | |
Fix another double negation proof issue (#7468)
This PR fixes another subtle proof issue in the circuit propagator concerning negated ites.
Fixes cvc5/cvc5-projects#309.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1c81316c3..ab449dc13 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -839,6 +839,7 @@ set(regress_0_tests regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 + regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 regress0/print_define_fun_internal.smt2 regress0/print_lambda.cvc.smt2 regress0/print_model.cvc.smt2 diff --git a/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 b/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 new file mode 100644 index 000000000..09626896d --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-fun a () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (not a)) +(assert (not (ite a d (not c)))) +(check-sat) |