diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-09 16:18:43 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-09 16:18:43 -0500 |
commit | df3fa17542b8bc3f455cb80ede4936b25a44fe5a (patch) | |
tree | f77f5337e84c234fa5650af003099a810baf23cc /test | |
parent | c74e9c8ba946387616345b70d63028896a0022c2 (diff) |
Fix type issue in arith rewrite equality (#3972)
Fixes #3952 and fixes #3940 and fixes #3941 and fixes #3968.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/arith/issue3952-rew-eq.smt2 | 53 |
2 files changed, 54 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d96360ad6..0edbd094d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1173,6 +1173,7 @@ set(regress_1_tests regress1/arith/div.06.smt2 regress1/arith/div.08.smt2 regress1/arith/div.09.smt2 + regress1/arith/issue3952-rew-eq.smt2 regress1/arith/miplib3.cvc regress1/arith/mod.02.smt2 regress1/arith/mod.03.smt2 diff --git a/test/regress/regress1/arith/issue3952-rew-eq.smt2 b/test/regress/regress1/arith/issue3952-rew-eq.smt2 new file mode 100644 index 000000000..9a14251a0 --- /dev/null +++ b/test/regress/regress1/arith/issue3952-rew-eq.smt2 @@ -0,0 +1,53 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: unsat +(set-logic QF_UFNIA) +(set-option :check-models true) +(set-option :produce-models true) +(set-option :arith-rewrite-equalities true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const v4 Bool) +(declare-const v5 Bool) +(declare-const i3 Int) +(declare-const i4 Int) +(declare-const i5 Int) +(declare-const i7 Int) +(declare-const i8 Int) +(declare-const i10 Int) +(declare-const i11 Int) +(declare-const i13 Int) +(declare-const i15 Int) +(declare-const i16 Int) +(declare-const i17 Int) +(push 1) +(assert (< i15 i8)) +(declare-const v6 Bool) +(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2)) +(push 1) +(declare-const v7 Bool) +(declare-const i18 Int) +(push 1) +(declare-const v8 Bool) +(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2)) +(declare-const v9 Bool) +(declare-const i19 Int) +(assert (xor (<= (- i4 i3 i10 i7) 65) (not v5) (and (<= i18 i11) v6 (distinct v6 (or v1 v2 v0 v5) (< i15 i8) v3 v2 v1 (< i15 i8) v6 v3 v3) (or v1 v2 v0 v5)) v7 (not v5) (= 128 i11))) +(push 1) +(declare-const v10 Bool) +(assert (=> v9 v1)) +(assert (not v5)) +(declare-const v11 Bool) +(declare-const i20 Int) +(declare-const i21 Int) +(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2)) +(push 1) +(assert (= v10 (=> (<= i18 i11) (distinct 67 i18)) v1 v6 (<= (- i4 i3 i10 i7) 65) (xor (<= (- i4 i3 i10 i7) 65) (not v5) (and (<= i18 i11) v6 (distinct v6 (or v1 v2 v0 v5) (< i15 i8) v3 v2 v1 (< i15 i8) v6 v3 v3) (or v1 v2 v0 v5)) v7 (not v5) (= 128 i11)) v8)) +(push 1) +(check-sat) +(push 1) +(push 1) +(pop 1) +(check-sat) |