diff options
Diffstat (limited to 'test/regress/regress0/auflia/fuzz02.smtv1.smt2')
| -rw-r--r-- | test/regress/regress0/auflia/fuzz02.smtv1.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/auflia/fuzz02.smtv1.smt2 b/test/regress/regress0/auflia/fuzz02.smtv1.smt2 new file mode 100644 index 000000000..593002fc4 --- /dev/null +++ b/test/regress/regress0/auflia/fuzz02.smtv1.smt2 @@ -0,0 +1,12 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_AUFLIA) +(declare-fun f0 (Int) Int) +(declare-fun f1 ((Array Int Int)) (Array Int Int)) +(declare-fun p0 (Int Int Int) Bool) +(declare-fun p1 ((Array Int Int) (Array Int Int) (Array Int Int)) Bool) +(declare-fun v0 () Int) +(declare-fun v1 () Int) +(declare-fun v2 () (Array Int Int)) +(declare-fun v3 () (Array Int Int)) +(check-sat-assuming ( (let ((_let_0 (f0 v0))) (let ((_let_1 (ite (p0 _let_0 v1 (+ v0 v0)) 1 0))) (let ((_let_2 (select v3 (+ v0 v0)))) (let ((_let_3 (f1 (f1 v3)))) (let ((_let_4 (p1 v3 v3 v3))) (let ((_let_5 (p1 (f1 v3) (f1 v3) (f1 _let_3)))) (let ((_let_6 (ite (> v0 _let_0) (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3) v3))) (let ((_let_7 (ite (< (+ v0 v0) _let_2) (f1 _let_3) _let_3))) (let ((_let_8 (ite (< (+ v0 v0) _let_2) (f1 v2) (ite (p1 v2 v3 (f1 v3)) v2 _let_6)))) (let ((_let_9 (ite (p1 (f1 v2) (f1 _let_3) _let_3) (f1 v3) _let_8))) (let ((_let_10 (ite (p0 v1 (select v3 _let_0) v0) (f1 _let_3) (f1 v3)))) (let ((_let_11 (ite (p0 (* v0 1) v1 _let_1) (* v0 1) v1))) (let ((_let_12 (ite _let_5 v1 (* v0 1)))) (let ((_let_13 (ite (p0 v1 (select v3 _let_0) v0) (ite (> v0 _let_0) v0 _let_1) _let_1))) (let ((_let_14 (ite (> v0 _let_0) (select v3 _let_0) (* v0 1)))) (let ((_let_15 (ite (p0 v1 (select v3 _let_0) v0) _let_1 _let_0))) (let ((_let_16 (ite (< (+ v0 v0) _let_2) (+ v0 v0) (* v0 1)))) (let ((_let_17 (ite (p1 v2 v3 (f1 v3)) (ite (> v0 _let_0) v0 _let_1) (* v0 1)))) (let ((_let_18 (select (f1 _let_3) _let_12))) (let ((_let_19 (select (ite (p1 v2 v3 (f1 v3)) v2 _let_6) _let_13))) (let ((_let_20 (f1 _let_7))) (let ((_let_21 (f1 (f1 v2)))) (let ((_let_22 (f1 (ite _let_4 (f1 v3) (ite (p1 v2 v3 (f1 v3)) v2 _let_6))))) (let ((_let_23 (f1 _let_9))) (let ((_let_24 (f1 _let_10))) (let ((_let_25 (f1 _let_21))) (let ((_let_26 (f1 (f1 _let_6)))) (let ((_let_27 (f0 (ite (p1 (f1 v2) (f1 _let_3) _let_3) _let_0 _let_1)))) (let ((_let_28 (+ v0 (ite (p1 (f1 v2) (f1 _let_3) _let_3) _let_0 _let_1)))) (let ((_let_29 (f0 (ite (> v0 _let_0) v0 _let_1)))) (let ((_let_30 (f0 _let_0))) (let ((_let_31 (- _let_12 _let_29))) (let ((_let_32 (- _let_14 _let_13))) (let ((_let_33 (* _let_16 1))) (let ((_let_34 (ite (p0 _let_32 _let_1 (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1))) 1 0))) (let ((_let_35 (- _let_2))) (let ((_let_36 (- _let_13 _let_13))) (let ((_let_37 (f0 (- (ite _let_4 _let_2 _let_13))))) (let ((_let_38 (+ _let_37 (- _let_17 _let_27)))) (let ((_let_39 (- (* v0 1) (* v0 1)))) (let ((_let_40 (and (<= (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1)) _let_11) (p0 (- v1 _let_12) (f0 _let_28) (- v1 _let_12))))) (let ((_let_41 (=> (= (and (and (and (>= _let_1 _let_30) (xor (= _let_38 (ite _let_4 _let_2 _let_13)) (= (p0 (ite (p1 (f1 v2) (f1 _let_3) _let_3) _let_0 _let_1) _let_11 _let_11) (=> (p1 v2 (f1 (f1 _let_3)) _let_10) (ite (>= (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1)) (ite _let_4 _let_2 _let_13)) (distinct (- _let_2 (+ v0 v0)) _let_33) (p1 _let_25 v2 _let_10)))))) (and (not (ite (=> (ite (p1 (f1 _let_3) (f1 _let_6) (f1 v2)) (p1 _let_22 _let_3 _let_9) (p0 (ite (p0 _let_27 (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1)) _let_31) 1 0) _let_2 (- (ite _let_4 _let_2 _let_13)))) (< _let_37 _let_12)) (not (> (ite (p0 (+ v0 v0) _let_27 (- (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1)) (ite _let_4 _let_2 _let_13))) 1 0) _let_37)) (= (and (or _let_5 (> (- _let_17 _let_27) (ite (> v0 _let_0) v0 _let_1))) (<= _let_18 _let_1)) (p1 (f1 _let_6) _let_3 _let_22)))) (not (ite (=> (ite (p1 (f1 _let_3) (f1 _let_6) (f1 v2)) (p1 _let_22 _let_3 _let_9) (p0 (ite (p0 _let_27 (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1)) _let_31) 1 0) _let_2 (- (ite _let_4 _let_2 _let_13)))) (< _let_37 _let_12)) (not (> (ite (p0 (+ v0 v0) _let_27 (- (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1)) (ite _let_4 _let_2 _let_13))) 1 0) _let_37)) (= (and (or _let_5 (> (- _let_17 _let_27) (ite (> v0 _let_0) v0 _let_1))) (<= _let_18 _let_1)) (p1 (f1 _let_6) _let_3 _let_22)))))) (ite (<= (- _let_17) (- _let_2 (+ v0 v0))) (and (=> (distinct _let_34 _let_28) (p1 (f1 v2) _let_8 (f1 v2))) (p0 (select v3 _let_0) _let_14 _let_34)) (<= (- _let_17) (- _let_2 (+ v0 v0))))) (and (xor (p0 _let_35 _let_39 _let_37) (< _let_31 _let_36)) (ite (p1 _let_25 _let_7 _let_25) (and (p1 (f1 v3) _let_3 (f1 _let_3)) (p0 (* v0 1) v1 _let_1)) (and (distinct _let_19 _let_34) (< (f0 _let_28) (ite _let_4 _let_2 _let_13)))))) (= (= (and (p1 (f1 _let_3) (f1 v2) (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3)) (p1 (f1 _let_3) (f1 v2) (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3))) (p1 _let_23 _let_3 _let_26)) (and (and (or (= _let_33 _let_30) (= (and (p0 v1 (select v3 _let_0) v0) (>= (- _let_19) (* v0 1))) (p1 (f1 (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3)) _let_21 (f1 v2)))) (and (p1 v2 (f1 (ite _let_5 (f1 _let_3) (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3))) (f1 _let_3)) (ite (xor (=> (= (- _let_11) _let_29) (p1 (f1 (ite (p1 v2 v3 (f1 v3)) v2 _let_6)) _let_23 _let_26)) (>= _let_32 _let_2)) (not (p0 v1 _let_33 (+ v0 v0))) (p0 (* 1 _let_15) _let_38 _let_28)))) (> v0 _let_0)))))) (or (ite (not (xor _let_40 _let_40)) (not (= (xor (or (= (p1 _let_26 (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3) _let_24) (< (- (ite (p0 (* v0 1) v1 _let_1) (ite (> v0 _let_0) v0 _let_1) (ite (> v0 _let_0) v0 _let_1)) (ite _let_4 _let_2 _let_13)) v0)) (< _let_13 _let_35)) (not (>= (* _let_2 (- 1)) _let_15))) (p1 (ite _let_5 (f1 _let_3) (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3)) _let_3 (f1 (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3))))) (not (and (p1 v2 v3 (f1 v3)) (or (p1 _let_23 _let_3 _let_9) (= (p1 (ite _let_4 (f1 v3) (ite (p1 v2 v3 (f1 v3)) v2 _let_6)) _let_3 _let_20) (=> (> (+ (select v3 _let_0) _let_30) (- _let_17 _let_27)) (p1 (f1 _let_8) (ite _let_5 (f1 _let_3) (ite (p0 (* v0 1) v1 _let_1) _let_3 _let_3)) (f1 _let_3)))))))) (ite _let_41 _let_41 (or (xor (xor (and (ite (xor (>= _let_15 (ite (p0 _let_37 (select v3 _let_0) _let_32) 1 0)) (p1 v3 (f1 v3) _let_9)) (or (= _let_27 _let_16) _let_4) (p1 (f1 v2) (f1 _let_3) _let_3)) (< (+ v0 v0) _let_2)) (p1 (ite (p1 v2 v3 (f1 v3)) v2 _let_6) (f1 _let_3) _let_9)) (= (p1 _let_6 _let_24 (f1 v2)) (= (=> (p1 (f1 v2) _let_21 _let_20) (distinct _let_35 _let_2)) (<= _let_39 (+ _let_18 _let_11))))) (or (xor (p0 _let_16 v1 (ite (p1 (f1 v2) (f1 _let_3) _let_3) _let_0 _let_1)) (> _let_14 _let_2)) (not (= (not (and (= (>= _let_39 (+ v0 v0)) (or (> (ite (> v0 _let_0) v0 _let_1) _let_11) (= (or (p1 _let_9 _let_8 _let_3) (p1 _let_26 _let_25 _let_9)) (>= _let_36 (ite (p1 (f1 v2) (f1 _let_3) _let_3) _let_0 _let_1))))) (distinct _let_38 _let_0))) (p0 _let_17 _let_27 v0))))))))))))))))))))))))))))))))))))))))))))))))) )) |