diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-10-26 16:42:14 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-26 19:42:14 +0000 |
| commit | 77dfb2623f3cb8ce8e9795f319d6ae574012debf (patch) | |
| tree | a5cd324ee5719eae03d3ef8fa8fc6730c98b287c /test | |
| parent | 58e710b299aaf46d480085fb98c77cd3b60de04a (diff) | |
[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)
Fixes cvc5/cvc5-projects#319
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 299261284..34ef1a9f7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -859,6 +859,7 @@ set(regress_0_tests regress0/proofs/open-pf-rederivation.smt2 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/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-3-chainres-checking.smt2 b/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 new file mode 100644 index 000000000..27836734b --- /dev/null +++ b/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (and (= a (ite (or c d) d a)) (not (ite d a false)) (ite c a d))) +(check-sat)
\ No newline at end of file |