test/regress/regress0/aufbv/fuzz02.smtv1.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 14))
(declare-fun v1 () (_ BitVec 10))
(declare-fun v2 () (_ BitVec 10))
(declare-fun v3 () (_ BitVec 8))
(declare-fun v4 () (_ BitVec 11))
(declare-fun a5 () (Array (_ BitVec 5) (_ BitVec 13)))
(declare-fun a6 () (Array (_ BitVec 15) (_ BitVec 15)))
(declare-fun a7 () (Array (_ BitVec 3) (_ BitVec 1)))
(declare-fun a8 () (Array (_ BitVec 8) (_ BitVec 14)))
(declare-fun a9 () (Array (_ BitVec 6) (_ BitVec 16)))
(declare-fun a10 () (Array (_ BitVec 13) (_ BitVec 9)))
(declare-fun a11 () (Array (_ BitVec 3) (_ BitVec 14)))
(declare-fun a12 () (Array (_ BitVec 1) (_ BitVec 3)))
(check-sat-assuming ( (let ((_let_0 (ite (bvsle v4 ((_ sign_extend 6) (_ bv7 5))) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 (ite (bvsge v0 ((_ zero_extend 4) (_ bv37 10))) (_ bv1 1) (_ bv0 1)))) (let ((_let_2 (bvneg v3))) (let ((_let_3 (ite (bvsge v4 v4) (_ bv1 1) (_ bv0 1)))) (let ((_let_4 (ite (= ((_ zero_extend 4) (_ bv27 6)) (_ bv37 10)) (_ bv1 1) (_ bv0 1)))) (let ((_let_5 ((_ sign_extend 4) v2))) (let ((_let_6 (store a12 ((_ extract 5 5) (_ bv486 9)) ((_ extract 9 7) ((_ rotate_left 5) v1))))) (let ((_let_7 (ite (= (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1))) (_ bv1 1) (_ bv0 1)))) (let ((_let_8 (select a10 ((_ extract 13 1) v0)))) (let ((_let_9 (select a8 ((_ extract 13 6) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))))))) (let ((_let_10 (select a9 ((_ extract 9 4) v1)))) (let ((_let_11 ((_ zero_extend 1) (bvashr (_ bv60 7) ((_ zero_extend 6) _let_4))))) (let ((_let_12 (select (store a8 ((_ zero_extend 7) _let_4) _let_9) _let_11))) (let ((_let_13 (select a5 ((_ zero_extend 4) _let_7)))) (let ((_let_14 (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) _let_0))) (let ((_let_15 (bvnot (_ bv60 7)))) (let ((_let_16 (bvmul ((_ zero_extend 10) (select _let_6 ((_ extract 2 2) (_ bv7 5)))) (select (store a5 ((_ extract 5 1) (_ bv27 6)) ((_ zero_extend 12) _let_3)) ((_ extract 4 0) (_ bv60 7)))))) (let ((_let_17 (bvneg (select a8 _let_11)))) (let ((_let_18 (bvsub ((_ zero_extend 8) (_ bv7 5)) (select (store a5 ((_ extract 5 1) (_ bv27 6)) ((_ zero_extend 12) _let_3)) ((_ extract 4 0) (_ bv60 7)))))) (let ((_let_19 (ite (bvsgt _let_5 ((_ sign_extend 7) (bvashr (_ bv60 7) ((_ zero_extend 6) _let_4)))) (_ bv1 1) (_ bv0 1)))) (let ((_let_20 (bvcomp ((_ sign_extend 9) _let_7) (_ bv37 10)))) (let ((_let_21 ((_ rotate_left 3) _let_8))) (let ((_let_22 (bvadd (select (store a5 ((_ extract 5 1) (_ bv27 6)) ((_ zero_extend 12) _let_3)) ((_ extract 4 0) (_ bv60 7))) ((_ sign_extend 8) (_ bv7 5))))) (let ((_let_23 ((_ rotate_right 0) (select _let_6 ((_ extract 6 6) v2))))) (let ((_let_24 (ite (bvsgt ((_ zero_extend 6) (_ bv37 10)) ((_ repeat 2) v3)) (_ bv1 1) (_ bv0 1)))) (let ((_let_25 (ite (bvsle _let_10 ((_ zero_extend 6) v2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_26 (ite (bvuge ((_ zero_extend 15) _let_4) ((_ repeat 2) v3)) (_ bv1 1) (_ bv0 1)))) (let ((_let_27 (bvnand _let_0 _let_4))) (let ((_let_28 (bvashr _let_9 ((_ zero_extend 13) _let_20)))) (let ((_let_29 (bvxnor ((_ zero_extend 6) (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) ((_ extract 10 10) _let_9))) (bvneg (_ bv486 9))))) (let ((_let_30 (ite (bvugt _let_17 _let_5) (_ bv1 1) (_ bv0 1)))) (let ((_let_31 (bvashr ((_ zero_extend 2) _let_4) _let_23))) (let ((_let_32 (bvcomp ((_ sign_extend 3) v2) (bvlshr ((_ zero_extend 10) _let_14) _let_13)))) (let ((_let_33 (ite (bvugt _let_18 ((_ sign_extend 7) (_ bv27 6))) (_ bv1 1) (_ bv0 1)))) (let ((_let_34 (bvneg (bvshl ((_ zero_extend 13) _let_1) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))))))) (let ((_let_35 (ite (bvsgt ((_ sign_extend 5) _let_19) (_ bv27 6)) (_ bv1 1) (_ bv0 1)))) (let ((_let_36 ((_ repeat 3) _let_3))) (let ((_let_37 (bvcomp (bvlshr ((_ zero_extend 10) _let_14) _let_13) (bvlshr ((_ zero_extend 10) _let_14) _let_13)))) (let ((_let_38 ((_ zero_extend 4) _let_29))) (let ((_let_39 (ite (bvult _let_38 _let_13) (_ bv1 1) (_ bv0 1)))) (let ((_let_40 ((_ sign_extend 1) v1))) (let ((_let_41 (bvor ((_ sign_extend 2) _let_8) v4))) (let ((_let_42 (bvshl v0 (select a8 _let_11)))) (let ((_let_43 (ite (bvugt ((_ sign_extend 9) _let_24) v2) (_ bv1 1) (_ bv0 1)))) (let ((_let_44 (bvnot _let_12))) (let ((_let_45 ((_ zero_extend 2) _let_40))) (let ((_let_46 ((_ sign_extend 2) (bvneg (_ bv486 9))))) (let ((_let_47 ((_ zero_extend 11) (select _let_6 ((_ extract 6 6) v2))))) (let ((_let_48 ((_ zero_extend 12) _let_19))) (let ((_let_49 ((_ sign_extend 2) _let_7))) (let ((_let_50 ((_ zero_extend 2) _let_30))) (let ((_let_51 ((_ zero_extend 1) v3))) (let ((_let_52 ((_ zero_extend 5) (_ bv486 9)))) (let ((_let_53 ((_ sign_extend 12) _let_7))) (let ((_let_54 (ite (bvsle ((_ sign_extend 13) (select _let_6 ((_ extract 6 6) v2))) ((_ repeat 2) v3)) (and (bvult ((_ zero_extend 11) (select _let_6 ((_ extract 2 2) (_ bv7 5)))) _let_5) (bvsgt ((_ zero_extend 1) _let_22) _let_17)) (distinct (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))) ((_ sign_extend 13) _let_7))))) (let ((_let_55 (= (=> (bvsgt _let_45 _let_18) (bvugt (_ bv486 9) ((_ sign_extend 4) (_ bv7 5)))) (= (bvule _let_26 _let_1) (not (distinct ((_ zero_extend 13) _let_43) (select a8 _let_11))))))) (let ((_let_56 (ite (not (not (or (ite (bvsgt _let_44 ((_ zero_extend 4) (bvsub ((_ rotate_left 5) v1) ((_ zero_extend 3) (_ bv60 7))))) (bvuge (bvlshr ((_ zero_extend 10) _let_14) _let_13) ((_ zero_extend 6) _let_15)) (bvsle _let_17 ((_ zero_extend 13) (select (store a7 ((_ extract 2 0) _let_5) _let_0) ((_ extract 13 11) _let_12))))) (bvugt _let_41 ((_ sign_extend 10) _let_37))))) (=> (ite (bvslt _let_39 _let_1) (bvsge _let_18 ((_ sign_extend 3) (_ bv37 10))) (bvslt v1 ((_ sign_extend 9) _let_26))) (=> (and (and (and (bvsgt (bvlshr ((_ zero_extend 10) _let_14) _let_13) _let_53) (bvugt ((_ zero_extend 8) _let_1) _let_21)) (or (= (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1))) (bvslt _let_5 ((_ sign_extend 6) v3)))) (bvule ((_ sign_extend 4) (_ bv37 10)) _let_9)) (xor (distinct ((_ zero_extend 8) _let_32) (bvsub (_ bv486 9) _let_21)) (bvsgt v0 ((_ zero_extend 9) (_ bv7 5)))))) (=> (ite (bvslt _let_39 _let_1) (bvsge _let_18 ((_ sign_extend 3) (_ bv37 10))) (bvslt v1 ((_ sign_extend 9) _let_26))) (=> (and (and (and (bvsgt (bvlshr ((_ zero_extend 10) _let_14) _let_13) _let_53) (bvugt ((_ zero_extend 8) _let_1) _let_21)) (or (= (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1))) (bvslt _let_5 ((_ sign_extend 6) v3)))) (bvule ((_ sign_extend 4) (_ bv37 10)) _let_9)) (xor (distinct ((_ zero_extend 8) _let_32) (bvsub (_ bv486 9) _let_21)) (bvsgt v0 ((_ zero_extend 9) (_ bv7 5))))))))) (ite (=> (not (=> (ite (distinct _let_21 ((_ sign_extend 8) _let_24)) (or _let_55 _let_55) (bvsgt _let_36 ((_ sign_extend 2) _let_43))) (= (=> (not (or (xor (or (bvuge _let_44 ((_ sign_extend 13) (ite (bvsge ((_ zero_extend 8) _let_2) _let_10) (_ bv1 1) (_ bv0 1)))) (bvuge ((_ sign_extend 11) _let_31) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))))) (not (bvugt _let_9 _let_9))) (or (bvult _let_50 _let_36) (bvult _let_42 _let_47)))) (= (distinct ((_ zero_extend 2) _let_20) _let_14) (= (distinct _let_46 v4) (bvult (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) ((_ extract 10 10) _let_9)) ((_ zero_extend 2) _let_35))))) (xor (and (bvsgt _let_29 ((_ sign_extend 8) _let_19)) (or (and (bvule ((_ sign_extend 13) _let_43) (bvshl ((_ zero_extend 13) _let_1) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))))) (bvslt _let_10 ((_ zero_extend 15) _let_26))) (= _let_12 ((_ zero_extend 9) (_ bv7 5))))) (bvslt _let_9 v0))))) (not (xor (distinct _let_7 _let_35) (bvule _let_36 ((_ zero_extend 2) _let_1))))) (not (ite (=> (ite (distinct ((_ repeat 2) v3) ((_ sign_extend 10) (_ bv27 6))) (bvult (bvsub ((_ rotate_left 5) v1) ((_ zero_extend 3) (_ bv60 7))) ((_ sign_extend 9) _let_37)) (bvule _let_20 _let_32)) (ite (not (bvule ((_ zero_extend 15) _let_32) _let_10)) (bvsle ((_ zero_extend 13) _let_37) _let_34) (bvsge (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))) _let_47))) (not (bvsgt _let_42 ((_ zero_extend 13) _let_35))) (xor (or (and (bvsge (bvlshr ((_ zero_extend 10) _let_14) _let_13) _let_45) (distinct _let_50 (select _let_6 ((_ extract 2 2) (_ bv7 5))))) (distinct ((_ zero_extend 8) _let_25) (bvneg (_ bv486 9)))) (bvuge _let_21 ((_ sign_extend 2) (_ bv60 7)))))) (and (=> (or (ite (ite (xor (not (ite (bvuge v2 ((_ zero_extend 1) _let_29)) (= (bvuge _let_8 _let_21) (bvult _let_10 ((_ sign_extend 15) _let_43))) (=> (bvugt _let_34 (select a8 _let_11)) (distinct _let_41 ((_ sign_extend 10) _let_39))))) (=> (or (distinct ((_ zero_extend 6) (_ bv7 5)) _let_40) (xor (= (= (bvugt ((_ sign_extend 6) _let_43) _let_15) (bvslt ((_ zero_extend 3) _let_15) (_ bv37 10))) (distinct v1 ((_ zero_extend 7) _let_36))) (bvuge (bvlshr ((_ zero_extend 10) _let_14) _let_13) _let_22))) (or (= (bvule v0 ((_ zero_extend 5) (bvneg (_ bv486 9)))) (bvuge (select a8 _let_11) ((_ zero_extend 13) _let_26))) (bvult _let_44 _let_47)))) (=> (= (= (bvsle _let_33 _let_35) (bvuge ((_ sign_extend 13) _let_3) (select a8 _let_11))) (=> (= (= _let_25 (bvneg (select (store a7 ((_ extract 2 0) _let_5) _let_0) ((_ extract 13 11) _let_12)))) (and (bvsle (_ bv7 5) ((_ sign_extend 4) _let_43)) (or (not (bvule _let_3 _let_19)) (and (= _let_31 ((_ sign_extend 2) _let_25)) (xor (bvuge ((_ zero_extend 4) v2) _let_42) (bvsge (bvneg (_ bv486 9)) ((_ sign_extend 2) (bvashr (_ bv60 7) ((_ zero_extend 6) _let_4))))))))) (and (=> (ite (bvult ((_ zero_extend 9) _let_0) (_ bv37 10)) (and (bvsge ((_ zero_extend 3) _let_23) (_ bv27 6)) (bvsle ((_ zero_extend 10) (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) ((_ extract 10 10) _let_9))) _let_16)) (or (= ((_ sign_extend 5) _let_29) _let_17) (bvult _let_51 _let_8))) (xor (and (=> (bvuge _let_41 _let_46) (distinct ((_ sign_extend 6) _let_2) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))))) (bvule ((_ sign_extend 8) _let_23) _let_41)) (= (bvsle ((_ sign_extend 4) _let_14) (_ bv60 7)) (bvsge ((_ sign_extend 10) _let_23) (bvlshr ((_ zero_extend 10) _let_14) _let_13))))) (bvslt ((_ sign_extend 4) _let_21) _let_13)))) (bvugt _let_37 _let_7)) (xor (xor (and (bvsgt _let_42 ((_ sign_extend 1) _let_18)) (and (bvsle ((_ zero_extend 11) _let_14) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5))))) (bvslt _let_0 _let_33))) (=> (bvugt _let_8 ((_ zero_extend 6) (select _let_6 ((_ extract 2 2) (_ bv7 5))))) (xor (xor (ite (bvuge ((_ sign_extend 7) _let_15) (bvshl ((_ zero_extend 13) _let_1) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5)))))) (bvuge ((_ zero_extend 5) _let_4) (_ bv27 6)) (distinct _let_10 ((_ sign_extend 2) _let_12))) (or (bvugt (select a8 _let_11) ((_ zero_extend 4) v1)) (bvuge (bvshl ((_ zero_extend 13) _let_1) (select (store a11 ((_ extract 9 7) v0) ((_ sign_extend 4) v1)) (select _let_6 ((_ extract 2 2) (_ bv7 5))))) ((_ zero_extend 13) _let_3)))) (not (or (distinct ((_ rotate_left 5) v1) ((_ zero_extend 3) (_ bv60 7))) (bvsle ((_ sign_extend 9) _let_19) v2)))))) (=> (bvsgt _let_48 _let_22) (not (and (=> (ite (bvsgt v2 ((_ sign_extend 9) _let_7)) (bvsgt (bvneg (_ bv486 9)) _let_51) (= ((_ sign_extend 1) (select (store a5 ((_ extract 5 1) (_ bv27 6)) ((_ zero_extend 12) _let_3)) ((_ extract 4 0) (_ bv60 7)))) v0)) (bvsle (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) ((_ extract 10 10) _let_9)) (select _let_6 ((_ extract 6 6) v2)))) (bvule _let_23 ((_ sign_extend 2) _let_33))))))) _let_56 _let_56) (=> (or (bvsge ((_ sign_extend 7) _let_7) v3) (bvsge _let_7 _let_35)) (=> (xor (=> (or _let_54 _let_54) (xor (or (= ((_ zero_extend 4) (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) ((_ extract 10 10) _let_9))) (bvashr (_ bv60 7) ((_ zero_extend 6) _let_4))) (bvuge v0 ((_ sign_extend 5) _let_8))) (ite (bvuge v2 ((_ sign_extend 1) (bvneg (_ bv486 9)))) (bvsge _let_39 _let_7) (bvslt (bvneg (_ bv486 9)) ((_ zero_extend 4) (_ bv7 5)))))) (and (=> (not (bvule (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) ((_ extract 10 10) _let_9)) _let_49)) (distinct _let_16 _let_53)) (not (or (distinct _let_27 _let_32) (= (and (bvugt _let_15 ((_ zero_extend 2) (_ bv7 5))) (bvsge (bvashr (_ bv60 7) ((_ zero_extend 6) _let_4)) (bvashr (_ bv60 7) ((_ zero_extend 6) _let_4)))) (ite (bvuge _let_14 (select _let_6 ((_ extract 2 2) (_ bv7 5)))) (ite (bvsgt ((_ zero_extend 13) _let_30) _let_34) (bvsle ((_ sign_extend 11) (select _let_6 ((_ extract 6 6) v2))) (select a8 _let_11)) (bvsgt ((_ sign_extend 2) _let_28) ((_ repeat 2) v3))) (not (bvsle _let_28 ((_ zero_extend 5) _let_21))))))))) (=> (= (bvsgt v2 ((_ sign_extend 9) _let_1)) (bvsge ((_ zero_extend 8) _let_3) (bvneg (_ bv486 9)))) (= (bvsge _let_5 _let_12) (ite (=> (= _let_16 _let_48) (bvsgt ((_ zero_extend 11) _let_23) _let_9)) (xor (xor (bvuge (select a8 _let_11) ((_ zero_extend 1) (bvlshr ((_ zero_extend 10) _let_14) _let_13))) (bvugt _let_31 ((_ sign_extend 2) _let_0))) (= _let_52 _let_28)) (bvuge v0 ((_ sign_extend 1) (bvlshr ((_ zero_extend 10) _let_14) _let_13))))))))) (not (or (xor (bvsle ((_ sign_extend 2) _let_1) _let_14) (= (or (bvuge _let_13 _let_22) (bvsle ((_ zero_extend 10) _let_27) _let_41)) (xor (= ((_ sign_extend 6) _let_7) (bvashr (_ bv60 7) ((_ zero_extend 6) _let_4))) (bvsgt v4 ((_ sign_extend 10) _let_43))))) (xor (bvsge ((_ zero_extend 11) (select (store a12 ((_ extract 6 6) ((_ rotate_left 5) v1)) ((_ extract 13 11) v0)) ((_ extract 10 10) _let_9))) _let_44) (= (bvsgt _let_34 ((_ zero_extend 11) _let_36)) (bvsgt v4 ((_ zero_extend 10) _let_37))))))) (= (=> (= (=> (distinct ((_ sign_extend 15) _let_24) _let_10) (bvsle ((_ zero_extend 8) _let_39) (_ bv486 9))) (ite (= (or (=> (bvsgt _let_16 ((_ sign_extend 3) ((_ rotate_left 5) v1))) (bvult ((_ sign_extend 8) _let_37) _let_8)) (bvsge _let_8 ((_ zero_extend 8) _let_20))) (and (= ((_ rotate_left 5) v1) ((_ sign_extend 9) _let_43)) (bvugt ((_ sign_extend 5) v3) _let_13))) (xor (xor (=> (bvsle v3 ((_ zero_extend 7) _let_24)) (bvugt ((_ sign_extend 11) (_ bv7 5)) _let_10)) (bvslt _let_28 v0)) (xor (bvsgt ((_ zero_extend 13) _let_32) _let_42) (or (xor (= (bvsgt _let_13 ((_ zero_extend 12) _let_43)) (bvuge (select a8 _let_11) ((_ sign_extend 13) _let_25))) (bvule _let_44 _let_12)) (bvslt _let_22 _let_38)))) (=> (= (=> (ite (bvule _let_52 _let_17) (bvsge ((_ sign_extend 5) _let_26) (_ bv27 6)) (bvsge ((_ zero_extend 1) _let_18) _let_12)) (bvsle _let_18 ((_ zero_extend 10) _let_23))) (ite (bvule _let_36 ((_ zero_extend 2) _let_26)) (bvult ((_ zero_extend 8) _let_4) _let_29) (bvugt _let_17 ((_ sign_extend 8) (_ bv27 6))))) (bvult _let_0 _let_32)))) (bvuge _let_14 _let_49)) (= _let_15 ((_ sign_extend 6) _let_0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))