diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-04-08 14:38:09 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-08 16:38:09 -0500 |
commit | a48cafdd09c3ff8cb9984bad930343958c30ce56 (patch) | |
tree | 6394a01dc7dbd296b4d1cc7cf3bbdd9cddfd68f7 /test | |
parent | 24357fea07bf1eb6b1156a8e455c58faee96b604 (diff) |
Perform theory widening eagerly (#4044)
Fixes #3971 and fixes #3991. In incremental mode, the logic can change from one
(check-sat) call to another. In the reported issue, we start with QF_NIA
but then switch to QF_UFNIA because there is a div term (which has a UF in
its expanded form). Dealing with this issue is challenging in general. As a
result, we have decided not to allow theory widening in
Theory::expandDefinitions() anymore but instead to do it eagerly in
SmtEngine::setDefaults().
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/nl/issue3971.smt2 | 145 | ||||
-rw-r--r-- | test/regress/regress0/nl/issue3991.smt2 | 13 |
3 files changed, 160 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1f3d4f623..649178f91 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -582,6 +582,8 @@ set(regress_0_tests regress0/nl/issue3719.smt2 regress0/nl/issue3729-cm-solved-tf.smt2 regress0/nl/issue3959.smt2 + regress0/nl/issue3971.smt2 + regress0/nl/issue3991.smt2 regress0/nl/issue4007-rint-uf.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 diff --git a/test/regress/regress0/nl/issue3971.smt2 b/test/regress/regress0/nl/issue3971.smt2 new file mode 100644 index 000000000..93d370659 --- /dev/null +++ b/test/regress/regress0/nl/issue3971.smt2 @@ -0,0 +1,145 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic QF_NIA) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const i4 Int) +(declare-const i5 Int) +(declare-const i6 Int) +(declare-const i7 Int) +(declare-const i8 Int) +(declare-const i9 Int) +(declare-const i12 Int) +(declare-const i13 Int) +(declare-const i14 Int) +(declare-const v4 Bool) +(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6)))) +(declare-const v5 Bool) +(assert v1) +(declare-const i15 Int) +(declare-const v6 Bool) +(assert (distinct v5 (<= i8 i15))) +(declare-const i16 Int) +(assert v0) +(declare-const i17 Int) +(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) +(declare-const i18 Int) +(declare-const v7 Bool) +(assert (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6)) +(declare-const v8 Bool) +(declare-const v9 Bool) +(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) +(assert (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) +(assert (=> v4 (<= i13 i6))) +(declare-const v10 Bool) +(declare-const v11 Bool) +(assert v9) +(check-sat) +(assert (> (abs i7) i4)) +(assert v2) +(declare-const v12 Bool) +(assert (distinct v5 (<= i8 i15))) +(declare-const i19 Int) +(assert (xor (not (< (div i4 i8) 79)) (> (- 888) i15) (distinct i6 i12) (distinct i6 i12) (= (or v1 v3 v2) v1) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v10)) +(check-sat) +(declare-const v13 Bool) +(push 1) +(assert (< i9 i8)) +(assert (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8)) +(push 1) +(push 1) +(declare-const v14 Bool) +(assert v7) +(assert v10) +(declare-const v15 Bool) +(declare-const v16 Bool) +(declare-const i20 Int) +(assert (or v1 v3 v2)) +(declare-const i21 Int) +(declare-const v17 Bool) +(assert (=> (> i6 (abs 79)) (or (= (- i8) 36) v6 v1))) +(declare-const v18 Bool) +(assert (distinct i6 i12)) +(declare-const v19 Bool) +(assert (< i9 i8)) +(declare-const v20 Bool) +(assert (= v16 (>= i19 (abs i14)) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (<= i13 i6))) +(declare-const v21 Bool) +(declare-const v22 Bool) +(assert (> 79 34)) +(declare-const i22 Int) +(assert v9) +(declare-const i23 Int) +(declare-const v23 Bool) +(declare-const v24 Bool) +(declare-const i24 Int) +(pop 1) +(declare-const i25 Int) +(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6)))) +(declare-const v25 Bool) +(pop 1) +(declare-const v26 Bool) +(declare-const i26 Int) +(declare-const i27 Int) +(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1)) +(push 1) +(assert (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4))) +(declare-const v27 Bool) +(declare-const v28 Bool) +(declare-const v29 Bool) +(declare-const i28 Int) +(assert (distinct v5 (<= i8 i15))) +(assert (xor (> (- 888) i15) v3 (< i9 i8) (=> v4 (<= i13 i6)) (>= 162 43) (and (>= 162 43) (distinct 623 752) (= i15 960)) (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4)))) +(assert (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) +(declare-const v30 Bool) +(assert (or (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v6 (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (>= 162 43) v30 (< (div i4 i8) 79) v2 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6))) +(assert (= (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) v28 v28)) +(declare-const v31 Bool) +(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1)) +(declare-const v32 Bool) +(pop 1) +(declare-const i29 Int) +(assert (xor v2 v2 v3 v0 v0 v2 v3 v1 v2)) +(declare-const v33 Bool) +(assert v9) +(push 1) +(declare-const v34 Bool) +(assert (or (>= 162 43) (>= i14 i19) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79) (< i6 (div i4 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (or (not (< (div i4 i8) 79)) (> (abs i7) i4) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i9 i8) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v5)) +(declare-const i30 Int) +(declare-const v35 Bool) +(push 1) +(assert (and (>= 162 43) (distinct 623 752) (= i15 960))) +(declare-const v36 Bool) +(assert (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6)))) +(push 1) +(declare-const v37 Bool) +(declare-const v38 Bool) +(assert (distinct (= v3 v4 (<= i13 i6) v0 v10 v6) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (> 546 i8) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i6 (div i4 i8)) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79))) +(assert (and (= v3 v4 (<= i13 i6) v0 v10 v6) (>= (abs 969) (* i6 162 i4 i4)))) +(assert v0) +(assert (<= 12 i4)) +(check-sat) +(assert (distinct (>= (abs 969) (* i6 162 i4 i4)) (xor (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (< (div i4 i8) 79) v11 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v4 (> 546 i8) (> i6 (abs 79))))) +(assert (=> (or (= (- i8) 36) v6 v1) (distinct v5 (<= i8 i15)))) +(declare-const v39 Bool) +(push 1) +(declare-const v40 Bool) +(declare-const v41 Bool) +(declare-const v42 Bool) +(check-sat) +(assert (or (= (- i8) 36) v6 v1)) +(assert (=> (=> v4 (<= i13 i6)) (< i6 (div i4 i8)))) +(pop 1) +(declare-const v43 Bool) +(pop 1) +(assert (or v1 v3 v2)) +(push 1) +(assert (not (> (abs i7) i4))) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/issue3991.smt2 b/test/regress/regress0/nl/issue3991.smt2 new file mode 100644 index 000000000..c006b2885 --- /dev/null +++ b/test/regress/regress0/nl/issue3991.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --incremental --check-unsat-cores +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_NIA) +(declare-const i7 Int) +(check-sat) +(declare-const v18 Bool) +(assert (and (= i7 93) (or (> 19 i7) v18) v18)) +(check-sat) +(assert (> 19 i7)) +(assert (> (div i7 0) 0)) +(check-sat) |