1 files changed, 145 insertions, 0 deletions
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)