diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-07-13 15:38:23 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-13 13:38:23 -0500 |
| commit | 912be5c60f194c3b0d52c1d06a1339fb6cb13a9c (patch) | |
| tree | d82fa967ecf45342133369c8641aac02ca633016 /test | |
| parent | 36d01a7fd74c6dff52bf9dcba490ff7ded29ad5d (diff) | |
[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)
Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index be0815668..39fa83311 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -828,6 +828,7 @@ set(regress_0_tests regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc regress0/proofs/issue277-circuit-propagator.smt2 + regress0/proofs/open-pf-if-unordered-iff.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/open-pf-if-unordered-iff.smt2 b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 new file mode 100644 index 000000000..b21c3f142 --- /dev/null +++ b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 @@ -0,0 +1,9 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-const __ (_ BitVec 3)) +(declare-const ___ (_ BitVec 3)) +(assert (= (_ bv0 64) (bvand (_ bv1 64) ((_ zero_extend 32) ((_ zero_extend 16) ((_ zero_extend 8) ((_ zero_extend 4) ((_ zero_extend 1) __)))))))) +(assert (bvule __ ___)) +(assert (= (_ bv0 64) (bvand (_ bv1 64) (bvadd (_ bv1 64) ((_ zero_extend 32) ((_ zero_extend 16) ((_ zero_extend 8) ((_ zero_extend 4) ((_ zero_extend 1) ___))))))))) +(assert (bvule ___ __)) +(check-sat) |