diff options
Diffstat (limited to 'test/regress/regress0/arrays/incorrect3.smtv1.smt2')
| -rw-r--r-- | test/regress/regress0/arrays/incorrect3.smtv1.smt2 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/arrays/incorrect3.smtv1.smt2 b/test/regress/regress0/arrays/incorrect3.smtv1.smt2 new file mode 100644 index 000000000..932ea92f5 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect3.smtv1.smt2 @@ -0,0 +1,13 @@ +(set-option :incremental false) +(set-info :status unsat) +(set-logic QF_AUF) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun v0 () (Array Index Element)) +(declare-fun v1 () Index) +(declare-fun v2 () Element) +(declare-fun v3 () Element) +(declare-fun v4 () Element) +(declare-fun v5 () Element) +(declare-fun v6 () Element) +(check-sat-assuming ( (let ((_let_0 (select (store v0 v1 v2) v1))) (let ((_let_1 (distinct v0 v0))) (let ((_let_2 (= (store v0 v1 v2) v0))) (let ((_let_3 (distinct v1 v1))) (let ((_let_4 (distinct v4 _let_0))) (let ((_let_5 (distinct v2 v6))) (let ((_let_6 (= _let_0 _let_0))) (let ((_let_7 (= v6 v5))) (let ((_let_8 (= v3 v3))) (let ((_let_9 (distinct v3 v4))) (let ((_let_10 (distinct v4 v5))) (let ((_let_11 (= _let_0 v3))) (let ((_let_12 (ite _let_9 v0 v0))) (let ((_let_13 (ite _let_4 _let_12 v0))) (let ((_let_14 (ite _let_4 (store v0 v1 v2) (store v0 v1 v2)))) (let ((_let_15 (ite _let_7 _let_14 _let_14))) (let ((_let_16 (ite (distinct v2 v5) _let_13 _let_13))) (let ((_let_17 (ite _let_8 _let_14 _let_15))) (let ((_let_18 (ite _let_2 _let_13 _let_14))) (let ((_let_19 (ite _let_6 _let_14 _let_16))) (let ((_let_20 (ite _let_5 (ite _let_9 _let_15 _let_12) _let_19))) (let ((_let_21 (ite _let_7 (store v0 v1 v2) _let_13))) (let ((_let_22 (ite _let_10 _let_17 v0))) (let ((_let_23 (ite _let_3 _let_12 _let_14))) (let ((_let_24 (ite _let_1 v0 (store v0 v1 v2)))) (let ((_let_25 (ite (distinct v2 v5) _let_23 _let_24))) (let ((_let_26 (ite _let_11 _let_18 _let_17))) (let ((_let_27 (ite (= v3 _let_0) (ite (distinct v2 v2) (store v0 v1 v2) v0) _let_13))) (let ((_let_28 (ite (distinct v2 v2) v1 v1))) (let ((_let_29 (ite (distinct v2 v5) v1 _let_28))) (let ((_let_30 (ite (= v2 v2) (ite _let_3 _let_29 v1) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))))) (let ((_let_31 (ite _let_2 v1 v1))) (let ((_let_32 (ite _let_5 (ite _let_3 _let_29 v1) _let_31))) (let ((_let_33 (ite (distinct v2 v2) v1 _let_30))) (let ((_let_34 (ite _let_6 _let_29 _let_30))) (let ((_let_35 (ite _let_1 (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28) _let_29))) (let ((_let_36 (ite _let_10 (ite _let_10 _let_32 (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))) _let_35))) (let ((_let_37 (ite _let_4 (ite _let_3 _let_29 v1) _let_32))) (let ((_let_38 (ite _let_9 (ite _let_5 _let_28 _let_29) _let_36))) (let ((_let_39 (ite _let_11 _let_29 (ite _let_5 _let_28 _let_29)))) (let ((_let_40 (ite _let_5 (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))) (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))))))) (let ((_let_41 (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) _let_39))) (let ((_let_42 (ite _let_8 (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))) _let_41))) (let ((_let_43 (ite _let_4 (ite _let_5 _let_28 _let_29) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))))) (let ((_let_44 (ite (distinct v2 v5) v6 v5))) (let ((_let_45 (ite _let_3 v4 v3))) (let ((_let_46 (ite (= v3 _let_0) v6 v3))) (let ((_let_47 (ite _let_7 v5 v6))) (let ((_let_48 (ite (distinct v2 v2) _let_0 v2))) (let ((_let_49 (ite _let_10 v3 v5))) (let ((_let_50 (ite _let_10 v5 _let_46))) (let ((_let_51 (ite (= v2 v2) v5 v5))) (let ((_let_52 (ite (distinct v2 v2) _let_48 (ite _let_9 v4 v5)))) (let ((_let_53 (ite _let_3 v5 _let_46))) (let ((_let_54 (ite _let_8 _let_47 (ite _let_3 v4 (ite _let_11 v5 _let_0))))) (let ((_let_55 (ite _let_7 _let_48 (ite _let_2 _let_47 v4)))) (let ((_let_56 (ite _let_1 (ite _let_7 _let_48 v4) (ite _let_11 v5 _let_0)))) (let ((_let_57 (ite _let_8 v2 _let_44))) (let ((_let_58 (ite (= v3 _let_0) v6 v5))) (let ((_let_59 (ite _let_5 _let_58 v3))) (let ((_let_60 (store (ite _let_2 _let_23 _let_24) _let_35 _let_45))) (let ((_let_61 (select _let_26 _let_32))) (let ((_let_62 (store _let_20 _let_39 _let_49))) (let ((_let_63 (select _let_18 _let_35))) (let ((_let_64 (distinct (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))) _let_40))) (let ((_let_65 (or (distinct _let_52 (ite _let_4 (ite _let_6 _let_45 _let_44) v2)) (distinct v5 _let_48)))) (let ((_let_66 (not (or (distinct _let_53 _let_50) (= _let_21 (ite (distinct v2 v2) (store v0 v1 v2) v0)))))) (let ((_let_67 (or (=> (and (= (= _let_36 _let_37) (or (distinct (ite _let_2 _let_47 v4) _let_0) (ite (distinct _let_0 _let_52) (xor (distinct (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28) _let_39) (not _let_64)) (xor (distinct (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28) _let_39) (not _let_64))))) (ite (distinct v2 v2) (= _let_27 _let_24) (distinct _let_53 _let_50))) (and (= v2 v6) (distinct _let_13 (ite _let_2 _let_23 _let_24)))) (not (distinct v6 _let_56))))) (let ((_let_68 (= (ite (and (=> (or (or (xor (distinct _let_0 v6) (distinct _let_0 _let_45)) (distinct v5 _let_63)) (=> (not (xor (= _let_42 (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))))) (and (ite (distinct _let_35 _let_33) (=> (distinct _let_16 _let_27) (distinct (ite (distinct v2 v2) (store v0 v1 v2) v0) _let_24)) (= _let_44 v5)) (= (= (ite _let_9 v4 v5) (ite _let_3 v4 (ite _let_11 v5 _let_0))) (= _let_26 _let_24))))) (=> _let_4 (distinct _let_30 _let_31)))) (=> (and (xor (= (= v3 _let_46) (distinct _let_49 (ite _let_7 _let_48 v4))) (distinct _let_22 (ite _let_9 _let_15 _let_12))) (= (ite _let_5 _let_28 _let_29) _let_36)) (ite _let_8 (= _let_33 (ite _let_3 _let_29 v1)) (=> (= (distinct _let_19 _let_16) (xor _let_9 (distinct (ite _let_1 (ite _let_2 _let_17 _let_15) (ite (distinct v2 v2) (store v0 v1 v2) v0)) _let_62))) (distinct _let_61 _let_52))))) (=> (and (or (=> (= _let_36 (ite _let_2 _let_30 _let_31)) (or (or (or (distinct _let_36 _let_43) _let_2) (distinct _let_36 _let_41)) (and (ite (= _let_47 _let_59) (distinct _let_63 _let_44) (distinct (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))) (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))))) (distinct (ite _let_7 _let_21 v0) _let_62)))) (= (not (distinct _let_34 _let_32)) (distinct _let_23 _let_13))) (distinct _let_28 _let_36)) (ite (or (= _let_17 _let_22) (distinct _let_50 _let_61)) (= _let_49 _let_50) (= _let_35 _let_30)))) (xor (xor (and (distinct v4 (ite _let_3 v4 (ite _let_11 v5 _let_0))) (= _let_52 _let_44)) (and (=> (not (= (distinct _let_25 _let_23) (=> (= _let_24 (ite _let_2 _let_17 _let_15)) (=> (=> (distinct (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))) _let_41) (distinct _let_26 _let_26)) (xor (not (= (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))) v1)) (= (xor (xor (distinct (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))) _let_39) (distinct _let_32 v1)) (= _let_33 _let_42)) (= (distinct _let_32 (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))))) (or (distinct _let_20 _let_62) (distinct (ite (distinct v2 v2) (store v0 v1 v2) v0) _let_27))))))))) (not (not (distinct v2 _let_51)))) (distinct _let_24 _let_17))) (not (= (distinct (ite _let_2 _let_17 _let_15) _let_20) (= v6 _let_49)))) (xor (or (or (=> (= (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) _let_30) (distinct _let_36 (ite _let_5 _let_28 _let_29))) (= _let_20 _let_17)) (= _let_44 v6)) (ite (xor (= _let_57 v5) (xor (and (= _let_22 _let_19) (= (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28) _let_32)) (xor (and (distinct _let_45 _let_0) (= _let_32 _let_34)) (xor (= (ite _let_4 (ite _let_6 _let_45 _let_44) v2) v2) (= _let_58 _let_54))))) (distinct _let_27 (ite _let_1 (ite _let_2 _let_17 _let_15) (ite (distinct v2 v2) (store v0 v1 v2) v0))) (= (xor (ite (distinct _let_17 (ite _let_1 (ite _let_2 _let_17 _let_15) (ite (distinct v2 v2) (store v0 v1 v2) v0))) (distinct _let_17 (ite _let_1 (ite _let_2 _let_17 _let_15) (ite (distinct v2 v2) (store v0 v1 v2) v0))) (distinct _let_16 _let_62)) (ite (ite _let_6 (ite (=> (= (ite _let_6 _let_45 _let_44) _let_0) (distinct (ite _let_3 v4 (ite _let_11 v5 _let_0)) _let_54)) (distinct _let_40 (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))))) (= _let_16 _let_13)) (and (= _let_21 _let_18) (distinct _let_57 v5))) (ite (not (not (distinct v2 _let_55))) (distinct _let_57 (ite _let_11 v5 _let_0)) (distinct _let_59 _let_61)) (ite _let_6 (ite (=> (= (ite _let_6 _let_45 _let_44) _let_0) (distinct (ite _let_3 v4 (ite _let_11 v5 _let_0)) _let_54)) (distinct _let_40 (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))))) (= _let_16 _let_13)) (and (= _let_21 _let_18) (distinct _let_57 v5))))) (distinct _let_26 _let_25))))) (=> (or (or (xor (= _let_43 _let_36) (and (= (ite _let_3 v3 _let_57) _let_48) (= _let_51 _let_54))) (ite _let_1 (distinct _let_15 _let_60) (= _let_19 _let_23))) (= v2 v2)) (and (and (= _let_57 _let_46) (xor (ite (=> (distinct _let_31 _let_34) (ite (distinct _let_33 (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28)) (= _let_17 _let_21) _let_3)) (distinct _let_39 _let_35) (not _let_5)) (=> (= _let_29 _let_40) (distinct _let_52 _let_55)))) (=> (distinct _let_45 _let_44) (= _let_60 _let_24))))))) (=> (and (not (distinct _let_12 _let_27)) (xor (and (xor _let_67 _let_67) (= (not (ite (xor (=> _let_66 _let_66) (= (or _let_7 (= (not (=> (= (ite (= v1 _let_30) (= (ite _let_3 v3 _let_57) _let_47) (= v3 _let_0)) (=> (= v4 _let_53) _let_11)) (or (=> (xor (= _let_57 (ite _let_6 _let_45 _let_44)) (= _let_46 v6)) (= (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))) _let_31)) (= (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28) _let_37)))) (=> (and (or (xor (= _let_42 _let_43) (distinct v0 (ite _let_1 (ite _let_2 _let_17 _let_15) (ite (distinct v2 v2) (store v0 v1 v2) v0)))) (ite (= _let_12 v0) _let_10 (distinct _let_38 _let_34))) (and (distinct (ite (= v2 v2) (store v0 v1 v2) (store v0 v1 v2)) (ite _let_2 _let_17 _let_15)) (distinct (ite _let_3 v4 (ite _let_11 v5 _let_0)) (ite _let_3 v3 _let_57)))) (or (not (or (= (ite (distinct v2 v2) (store v0 v1 v2) v0) _let_23) (= (ite _let_2 _let_17 _let_15) (ite (distinct v2 v2) (store v0 v1 v2) v0)))) (= _let_16 _let_27))))) (xor _let_64 (ite (and (not (or (ite (or (distinct _let_56 (ite (distinct v2 v5) _let_47 _let_46)) (xor (or (= v2 _let_56) (ite (distinct _let_25 _let_14) (= _let_44 _let_52) (distinct _let_34 _let_43))) (= (store v0 v1 v2) _let_22))) (= (ite _let_5 _let_28 _let_29) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))) (xor (= (= _let_31 _let_28) (= (ite _let_3 v4 (ite _let_11 v5 _let_0)) (ite _let_2 _let_47 v4))) _let_4)) (= _let_29 _let_29))) (and (not (distinct _let_42 (ite _let_2 _let_30 _let_31))) (distinct (ite _let_10 _let_32 (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1))) _let_32))) (= _let_63 (ite _let_2 _let_47 v4)) (not (=> (not (distinct (ite _let_3 v3 _let_57) _let_47)) (xor (distinct _let_53 (select _let_25 (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28))) (= _let_31 _let_34)))))))) (= (not (distinct _let_27 _let_22)) (= (ite _let_4 (ite _let_6 _let_45 _let_44) v2) _let_53)) (ite (distinct _let_28 _let_29) (and (distinct (ite _let_7 (ite _let_5 _let_28 _let_29) _let_28) _let_42) (distinct (ite (= v3 _let_0) (ite _let_3 _let_29 v1) (ite (= v2 v2) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)) (ite (distinct v2 v5) (ite _let_3 _let_29 v1) (ite _let_3 _let_29 v1)))) _let_42)) (not (and (= _let_49 _let_46) (distinct v2 v5)))))) (=> (and _let_65 _let_65) (=> (= _let_48 _let_0) (not (= (distinct (ite _let_1 (ite _let_2 _let_17 _let_15) (ite (distinct v2 v2) (store v0 v1 v2) v0)) _let_62) (ite (= _let_59 _let_48) (distinct _let_16 _let_26) (distinct v2 v5)))))))) (=> (xor (=> (xor (= _let_44 (ite _let_4 _let_0 _let_48)) (= _let_39 _let_43)) (distinct _let_54 (ite _let_3 v3 _let_57))) (or (= _let_35 v1) (= (= (ite _let_7 _let_48 v4) _let_56) (distinct _let_38 _let_31)))) (not (= (= _let_44 _let_48) (and (distinct _let_30 _let_42) (distinct _let_17 _let_25))))))) (xor _let_68 _let_68))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )) |