(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 5))
(declare-fun v1 () (_ BitVec 2))
(declare-fun v2 () (_ BitVec 4))
(check-sat-assuming ( (let ((_let_0 (bvnot (_ bv2 2)))) (let ((_let_1 (bvadd (_ bv2 2) v1))) (let ((_let_2 (bvashr v0 ((_ sign_extend 3) _let_0)))) (let ((_let_3 (bvxor (_ bv2 2) ((_ sign_extend 1) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1)))))) (let ((_let_4 (ite (= ((_ sign_extend 3) (bvand _let_0 _let_1)) _let_2) (_ bv1 1) (_ bv0 1)))) (let ((_let_5 ((_ zero_extend 1) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))))) (let ((_let_6 (concat _let_4 v0))) (let ((_let_7 ((_ zero_extend 1) _let_4))) (let ((_let_8 (ite (bvsgt _let_2 ((_ zero_extend 3) (bvor _let_5 _let_0))) (_ bv1 1) (_ bv0 1)))) (let ((_let_9 ((_ repeat 1) (bvand _let_0 _let_1)))) (let ((_let_10 (ite (distinct _let_0 ((_ zero_extend 1) _let_8)) (_ bv1 1) (_ bv0 1)))) (let ((_let_11 (bvcomp _let_5 _let_1))) (let ((_let_12 (bvcomp _let_10 (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))))) (let ((_let_13 (bvnot _let_3))) (let ((_let_14 (bvsub ((_ sign_extend 4) (bvnot (bvand _let_7 _let_1))) _let_6))) (let ((_let_15 (bvneg _let_6))) (let ((_let_16 (ite (bvsge _let_9 _let_1) (_ bv1 1) (_ bv0 1)))) (let ((_let_17 (bvlshr (bvand _let_7 _let_1) ((_ sign_extend 1) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))))) (let ((_let_18 (bvcomp ((_ sign_extend 4) (bvand _let_7 _let_1)) _let_14))) (let ((_let_19 (bvcomp ((_ zero_extend 4) (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7))) _let_6))) (let ((_let_20 ((_ rotate_right 0) _let_11))) (let ((_let_21 ((_ rotate_left 0) _let_19))) (let ((_let_22 (bvsub (bvand _let_7 _let_1) ((_ sign_extend 1) _let_19)))) (let ((_let_23 (bvand ((_ sign_extend 1) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1))) _let_17))) (let ((_let_24 (bvxor ((_ zero_extend 3) _let_23) _let_2))) (let ((_let_25 (bvmul (_ bv2 2) _let_7))) (let ((_let_26 (ite (bvsgt ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 1) (_ bv2 2))) (_ bv1 1) (_ bv0 1)))) (let ((_let_27 (bvand _let_21 _let_20))) (let ((_let_28 (ite (= (_ bv1 1) ((_ extract 1 1) (bvor _let_5 _let_0))) (_ bv2 2) ((_ sign_extend 1) (ite (bvule (bvnot (bvand _let_7 _let_1)) _let_3) (_ bv1 1) (_ bv0 1)))))) (let ((_let_29 (concat _let_0 _let_21))) (let ((_let_30 (bvxnor ((_ zero_extend 1) _let_1) _let_29))) (let ((_let_31 (concat v1 _let_19))) (let ((_let_32 (bvlshr _let_13 _let_23))) (let ((_let_33 (ite (bvugt ((_ sign_extend 3) (bvnand (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) (_ bv2 2))) _let_24) (_ bv1 1) (_ bv0 1)))) (let ((_let_34 ((_ zero_extend 12) _let_0))) (let ((_let_35 (bvcomp ((_ sign_extend 3) (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0)) v0))) (let ((_let_36 (ite (distinct ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 2) _let_19)) (_ bv1 1) (_ bv0 1)))) (let ((_let_37 (bvor ((_ sign_extend 1) _let_8) (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7))))) (let ((_let_38 (ite (distinct (ite (bvsle (bvlshr (bvlshr (_ bv2 2) _let_7) _let_13) (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0)) (_ bv1 1) (_ bv0 1)) _let_21) (_ bv1 1) (_ bv0 1)))) (let ((_let_39 (bvnot (bvlshr (_ bv2 2) _let_7)))) (let ((_let_40 (ite (bvuge ((_ zero_extend 1) _let_16) (bvlshr (_ bv2 2) _let_7)) (_ bv1 1) (_ bv0 1)))) (let ((_let_41 (bvneg _let_8))) (let ((_let_42 ((_ rotate_right 0) _let_10))) (let ((_let_43 ((_ sign_extend 13) (bvand _let_7 _let_1)))) (let ((_let_44 (ite (= _let_38 (ite (bvsle (bvlshr (bvlshr (_ bv2 2) _let_7) _let_13) (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (let ((_let_45 ((_ sign_extend 1) _let_42))) (let ((_let_46 (bvor _let_45 _let_28))) (let ((_let_47 ((_ zero_extend 4) _let_41))) (let ((_let_48 (ite (bvugt ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 1) _let_9)) (_ bv1 1) (_ bv0 1)))) (let ((_let_49 (bvneg _let_46))) (let ((_let_50 (ite (bvslt _let_6 ((_ zero_extend 5) _let_20)) (_ bv1 1) (_ bv0 1)))) (let ((_let_51 ((_ repeat 4) (bvnot (bvand _let_7 _let_1))))) (let ((_let_52 ((_ repeat 3) (bvadd (bvor _let_5 _let_0) ((_ sign_extend 1) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))))))) (let ((_let_53 (ite (bvsle _let_14 _let_52) (_ bv1 1) (_ bv0 1)))) (let ((_let_54 ((_ rotate_right 1) _let_24))) (let ((_let_55 (bvashr _let_9 (_ bv2 2)))) (let ((_let_56 (bvashr _let_19 _let_19))) (let ((_let_57 (bvsub _let_54 ((_ sign_extend 2) _let_31)))) (let ((_let_58 (bvsub _let_3 ((_ zero_extend 1) (ite (bvsge (bvnot (bvand _let_7 _let_1)) (bvor _let_5 _let_0)) (_ bv1 1) (_ bv0 1)))))) (let ((_let_59 (ite (bvugt _let_31 ((_ zero_extend 1) _let_17)) (_ bv1 1) (_ bv0 1)))) (let ((_let_60 (bvmul ((_ zero_extend 3) (_ bv2 2)) v0))) (let ((_let_61 (concat (bvshl (_ bv2 2) (_ bv2 2)) _let_6))) (let ((_let_62 (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1)))) (let ((_let_63 ((_ sign_extend 1) _let_56))) (let ((_let_64 ((_ sign_extend 1) _let_48))) (let ((_let_65 ((_ zero_extend 1) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1))))) (let ((_let_66 ((_ zero_extend 1) _let_27))) (let ((_let_67 (xor (= _let_40 _let_40) (= (bvand _let_7 _let_1) (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)))))) (let ((_let_68 (not (= (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0) ((_ zero_extend 1) (ite (bvugt ((_ zero_extend 6) (bvneg _let_13)) _let_51) (_ bv1 1) (_ bv0 1))))))) (let ((_let_69 (ite (and (= ((_ zero_extend 2) _let_20) ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1)))) (= ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) _let_29)) (= (bvnot (bvand _let_7 _let_1)) ((_ zero_extend 1) _let_59)) (ite (= _let_22 (bvnand (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) (_ bv2 2))) (= _let_57 ((_ zero_extend 4) _let_48)) (= (_ bv2 2) ((_ sign_extend 1) (ite (bvsge (bvnot (bvand _let_7 _let_1)) (bvor _let_5 _let_0)) (_ bv1 1) (_ bv0 1)))))))) (let ((_let_70 (or (ite (= _let_33 (ite (bvsle (bvlshr (bvlshr (_ bv2 2) _let_7) _let_13) (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0)) (_ bv1 1) (_ bv0 1))) (not (= _let_0 (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)))) (= _let_33 (ite (bvsle (bvlshr (bvlshr (_ bv2 2) _let_7) _let_13) (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0)) (_ bv1 1) (_ bv0 1)))) (and (= (ite (distinct ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 2) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)) (ite (bvule (bvnot (bvand _let_7 _let_1)) _let_3) (_ bv1 1) (_ bv0 1))) (=> (= _let_24 ((_ zero_extend 3) (bvor _let_5 _let_0))) (= ((_ zero_extend 1) _let_16) _let_9)))))) (let ((_let_71 (not (xor (and (=> (= (= (ite (bvsge (bvnot (bvand _let_7 _let_1)) (bvor _let_5 _let_0)) (_ bv1 1) (_ bv0 1)) _let_19) (= _let_51 ((_ sign_extend 7) _let_4))) (not (= ((_ sign_extend 4) (ite (bvugt ((_ zero_extend 6) (bvneg _let_13)) _let_51) (_ bv1 1) (_ bv0 1))) v0))) (ite (= ((_ sign_extend 1) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1))) (bvand _let_7 _let_1)) (= _let_51 ((_ sign_extend 6) _let_25)) (= _let_39 _let_66))) (or (= (ite (bvsge (bvnot (bvand _let_7 _let_1)) (bvor _let_5 _let_0)) (_ bv1 1) (_ bv0 1)) _let_42) (xor (and (= _let_49 v1) (= (= ((_ zero_extend 4) _let_59) _let_47) (= ((_ zero_extend 2) _let_35) ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1)))))) (= (bvor _let_5 _let_0) (_ bv2 2)))))))) (or (or _let_71 _let_71) (=> (xor (= (xor (not (ite (= _let_14 ((_ sign_extend 3) ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))))) (not (= (_ bv2 2) ((_ sign_extend 1) _let_62))) (= (bvnand (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) (_ bv2 2)) (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7))))) (or (= (_ bv2 2) ((_ sign_extend 1) _let_11)) (= _let_8 (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1))))) (ite (= (or (= _let_7 (bvlshr (_ bv2 2) _let_7)) (= _let_39 _let_55)) (= (= _let_61 ((_ zero_extend 7) _let_53)) (= _let_23 (bvlshr (bvlshr (_ bv2 2) _let_7) _let_13)))) (and (= _let_29 ((_ zero_extend 2) (ite (bvugt ((_ zero_extend 6) (bvneg _let_13)) _let_51) (_ bv1 1) (_ bv0 1)))) (= _let_29 ((_ sign_extend 2) _let_62))) (ite (=> (= (= _let_37 ((_ sign_extend 1) (ite (bvsge (bvnot (bvand _let_7 _let_1)) (bvor _let_5 _let_0)) (_ bv1 1) (_ bv0 1)))) (= _let_51 ((_ sign_extend 6) (_ bv2 2)))) (= v2 ((_ sign_extend 2) _let_23))) (not (ite (= v1 _let_64) (= (ite (bvule (bvnot (bvand _let_7 _let_1)) _let_3) (_ bv1 1) (_ bv0 1)) _let_41) (not (=> (ite _let_67 (= ((_ zero_extend 13) _let_1) _let_43) _let_67) (= _let_49 _let_37))))) (= ((_ sign_extend 14) _let_32) ((_ zero_extend 15) (ite (distinct ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 2) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))))) (not (ite (xor (=> (= ((_ sign_extend 13) (ite (bvsle (bvlshr (bvlshr (_ bv2 2) _let_7) _let_13) (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0)) (_ bv1 1) (_ bv0 1))) _let_34) (= _let_63 (bvadd (bvor _let_5 _let_0) ((_ sign_extend 1) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1)))))) (or (and (= (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)) _let_40) (= (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1)) (ite (bvule (bvnot (bvand _let_7 _let_1)) _let_3) (_ bv1 1) (_ bv0 1)))) (or (=> (= _let_18 _let_27) (xor (= (_ bv2 2) ((_ zero_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0) ((_ sign_extend 1) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 1) _let_8) (bvnot (bvand _let_7 _let_1)))))) (= _let_53 _let_11) (ite (and (=> (= _let_65 _let_0) (xor (= _let_61 ((_ zero_extend 6) (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)))) (= ((_ zero_extend 5) _let_31) _let_51))) (= _let_52 ((_ zero_extend 4) _let_28))) (xor (= _let_43 ((_ zero_extend 14) _let_38)) (and (= (= v1 ((_ sign_extend 1) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) (= _let_13 _let_39)) (or (= ((_ zero_extend 4) _let_23) _let_15) (= (bvand _let_0 _let_1) (bvand _let_7 _let_1))))) (= _let_12 (ite (bvule (bvnot (bvand _let_7 _let_1)) _let_3) (_ bv1 1) (_ bv0 1))))))) (= (=> (and (ite (= (not (= (= _let_24 ((_ zero_extend 2) _let_29)) (not (= ((_ zero_extend 5) _let_44) _let_14)))) (=> (xor (ite (= _let_30 ((_ zero_extend 1) _let_13)) (=> (= _let_58 _let_0) (= ((_ sign_extend 4) _let_49) _let_52)) (and (or (xor (= ((_ zero_extend 5) _let_12) _let_52) (= (bvneg _let_13) _let_58)) (not (= _let_14 ((_ sign_extend 5) _let_11)))) (not (= _let_34 ((_ zero_extend 12) (bvand _let_7 _let_1)))))) (ite (= _let_61 ((_ zero_extend 3) _let_60)) (= (bvshl (_ bv2 2) (_ bv2 2)) (bvshl (_ bv2 2) (_ bv2 2))) (ite (or (= _let_2 ((_ zero_extend 3) _let_39)) (= _let_37 ((_ zero_extend 1) _let_56))) (not (= _let_6 ((_ zero_extend 4) _let_49))) (= ((_ sign_extend 1) _let_27) v1)))) (not (ite (or (= _let_13 ((_ zero_extend 1) _let_53)) (= ((_ zero_extend 13) _let_11) _let_34)) (= _let_58 ((_ sign_extend 1) _let_50)) (= ((_ sign_extend 2) _let_25) v2))))) (= (=> _let_68 _let_68) (ite (and (ite (=> (= ((_ rotate_right 0) (bvand _let_7 _let_1)) ((_ zero_extend 1) _let_11)) (= _let_16 _let_26)) (xor (= (_ bv2 2) ((_ sign_extend 1) _let_44)) (and (ite (= _let_17 _let_55) (= (bvand _let_7 _let_1) (bvnot (bvand _let_7 _let_1))) (= ((_ zero_extend 1) (ite (bvule (bvnot (bvand _let_7 _let_1)) _let_3) (_ bv1 1) (_ bv0 1))) _let_55)) (= _let_44 _let_4))) (or (= _let_28 ((_ sign_extend 1) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1)))) (or (= ((_ zero_extend 1) _let_26) _let_32) (and (ite (= _let_18 _let_44) (= _let_46 ((_ sign_extend 1) _let_59)) (= _let_41 (ite (distinct ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 2) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (or (xor (= _let_36 _let_20) (= (bvlshr (_ bv2 2) _let_7) (bvnot (bvand _let_7 _let_1)))) (= _let_17 (bvnand (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) (_ bv2 2)))))))) (and (not (= ((_ sign_extend 5) _let_40) _let_15)) (= (bvand _let_7 _let_1) ((_ sign_extend 1) _let_38)))) (xor (= ((_ zero_extend 1) _let_42) _let_37) (= ((_ zero_extend 7) _let_10) _let_51)) (= (and (ite _let_69 _let_69 (= _let_54 ((_ zero_extend 3) _let_9))) (ite (= _let_61 ((_ sign_extend 7) _let_20)) (or (= _let_45 _let_23) (= (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) (_ bv2 2))) (ite (= (= (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) ((_ sign_extend 1) _let_26)) (= _let_17 _let_66)) (= _let_6 ((_ zero_extend 5) _let_36)) (ite (=> (= _let_36 (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1))) (xor (and (= _let_65 _let_17) (= ((_ sign_extend 1) _let_21) _let_28)) (= ((_ sign_extend 3) _let_57) _let_61))) (or (= (= (bvnand (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) (_ bv2 2)) _let_39) (= _let_47 ((_ sign_extend 4) (ite (distinct ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 2) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))) (= ((_ sign_extend 6) _let_32) _let_61)) (= (= _let_28 ((_ zero_extend 1) (ite (distinct ((_ sign_extend 2) (ite (bvsle (_ bv2 2) _let_1) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 2) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (not (= ((_ zero_extend 3) (ite (bvsle ((_ sign_extend 1) ((_ extract 0 0) (bvshl (_ bv2 2) (_ bv2 2)))) _let_23) (_ bv1 1) (_ bv0 1))) v2))))))) (= ((_ zero_extend 1) (bvor _let_42 _let_10)) (bvnand (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7)) (_ bv2 2)))))) (and (= (not (or (= ((_ zero_extend 1) _let_20) (ite (= (_ bv1 1) ((_ extract 0 0) (ite (bvugt _let_11 _let_8) (_ bv1 1) (_ bv0 1)))) _let_1 _let_0)) (= _let_32 (bvshl ((_ sign_extend 1) _let_8) (bvlshr (_ bv2 2) _let_7))))) (not (=> (= v1 ((_ sign_extend 1) _let_36)) (or (= (bvand _let_0 _let_1) _let_3) (= _let_8 _let_8))))) (=> (or (= _let_64 _let_32) (= _let_30 ((_ sign_extend 2) _let_50))) (or (xor (= _let_0 (bvlshr (_ bv2 2) _let_7)) (= _let_22 _let_63)) (or (xor (or (= ((_ zero_extend 4) _let_35) _let_60) (xor (= _let_52 ((_ sign_extend 1) v0)) (= _let_32 ((_ sign_extend 1) _let_33)))) (= (ite (bvule (bvnot (bvand _let_7 _let_1)) _let_3) (_ bv1 1) (_ bv0 1)) _let_40)) (= _let_55 _let_46)))))) (or (not (= _let_16 _let_33)) (not (= (bvnot (bvand _let_7 _let_1)) ((_ sign_extend 1) _let_20))))) (not (= ((_ sign_extend 2) v2) _let_6))) (=> (xor (and (=> (= ((_ zero_extend 1) _let_48) _let_28) (or (= _let_61 ((_ sign_extend 6) _let_3)) (= (= (_ bv2 2) ((_ sign_extend 1) _let_53)) (= _let_54 _let_54)))) (= ((_ sign_extend 1) _let_13) (bvshl _let_31 ((_ zero_extend 1) (bvand _let_0 _let_1))))) (=> _let_70 _let_70)) (or (xor (xor (= _let_13 _let_23) (= _let_33 _let_16)) (= ((_ zero_extend 12) v1) _let_34)) (and (= _let_12 _let_62) (= (= _let_59 _let_27) (or (= v2 ((_ sign_extend 2) _let_17)) (= ((_ zero_extend 8) _let_6) _let_34))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))