; 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)