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 | |
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')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 | 10 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3ea588e01..eda397da0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -834,6 +834,7 @@ set(regress_0_tests regress0/preprocess/preprocess_13.cvc.smt2 regress0/preprocess/preprocess_14.cvc.smt2 regress0/preprocess/preprocess_15.cvc.smt2 + regress0/preprocess/proj-issue305-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-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 |