diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-10-26 17:59:31 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-26 20:59:31 +0000 |
| commit | 38b59f152974347c132f3ca665948f4a7780abc4 (patch) | |
| tree | dd4bfe185bb4f92f2dbf10a532361c726767712f /test/regress | |
| parent | 1d2c50986cb53207e0f99a950b939736db226634 (diff) | |
[proofs] Fix singleton check in MACRO_RES post-processing (#7498)
Previously the check for whether the original conclusion of the MACRO_RESOULTION step was a singleton was incomplete. Now the test is made the proper way.
Depends on #7497.
Fixes cvc5/cvc5-projects#318
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2a96818eb..1379c7066 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -861,6 +861,7 @@ set(regress_0_tests regress0/proofs/qgu-fuzz-1-bool-sat.smt2 regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 + regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 regress0/proofs/scope.smt2 regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 diff --git a/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 b/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 new file mode 100644 index 000000000..8eef0674b --- /dev/null +++ b/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (and (or d (ite c false true)) (not (= d (or b c))) (= d (ite c d (not d))))) +(check-sat) |