test/regress/regress0/bv/fuzz22.smtv1.smt2


1
2
3
4
5
6
7
8
9

(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 4))
(declare-fun v1 () (_ BitVec 4))
(declare-fun v2 () (_ BitVec 4))
(declare-fun v3 () (_ BitVec 4))
(declare-fun v4 () (_ BitVec 4))
(check-sat-assuming ( (let ((_let_0 (bvnot ((_ rotate_left 1) v0)))) (let ((_let_1 (bvnot v2))) (let ((_let_2 (bvashr v1 _let_1))) (let ((_let_3 ((_ repeat 1) _let_0))) (let ((_let_4 ((_ zero_extend 0) (_ bv12 4)))) (let ((_let_5 (ite (bvsge (ite (= (_ bv1 1) ((_ extract 2 2) v0)) v1 v2) _let_4) (_ bv1 1) (_ bv0 1)))) (let ((_let_6 (bvlshr _let_2 _let_0))) (let ((_let_7 (bvxor v4 ((_ rotate_left 1) v0)))) (let ((_let_8 (bvneg _let_6))) (let ((_let_9 (ite (bvsgt ((_ rotate_left 1) v0) _let_1) (_ bv1 1) (_ bv0 1)))) (let ((_let_10 (ite (bvslt (bvneg _let_1) v4) (_ bv1 1) (_ bv0 1)))) (let ((_let_11 (ite (= (_ bv1 1) ((_ extract 0 0) _let_9)) ((_ zero_extend 3) _let_5) _let_1))) (let ((_let_12 (bvshl (_ bv12 4) _let_4))) (let ((_let_13 ((_ rotate_left 0) _let_1))) (let ((_let_14 (ite (bvult v1 _let_0) (_ bv1 1) (_ bv0 1)))) (let ((_let_15 (bvmul _let_3 ((_ zero_extend 3) _let_9)))) (let ((_let_16 ((_ sign_extend 0) _let_6))) (let ((_let_17 ((_ rotate_right 3) (bvxnor _let_13 ((_ zero_extend 3) (bvcomp v0 (_ bv12 4))))))) (let ((_let_18 (ite (bvult _let_4 ((_ sign_extend 3) (bvnot _let_14))) (_ bv1 1) (_ bv0 1)))) (let ((_let_19 (bvxor _let_16 (_ bv12 4)))) (let ((_let_20 (bvlshr _let_6 v3))) (let ((_let_21 (distinct _let_10 _let_5))) (let ((_let_22 (= (ite (= (_ bv1 1) ((_ extract 2 2) v0)) v1 v2) (bvxnor _let_13 ((_ zero_extend 3) (bvcomp v0 (_ bv12 4))))))) (let ((_let_23 ((_ sign_extend 3) _let_18))) (let ((_let_24 ((_ sign_extend 3) _let_9))) (let ((_let_25 (= (bvxnor _let_13 ((_ zero_extend 3) (bvcomp v0 (_ bv12 4)))) v4))) (let ((_let_26 ((_ sign_extend 3) (ite (bvule (_ bv12 4) _let_8) (_ bv1 1) (_ bv0 1))))) (let ((_let_27 (bvugt v0 _let_3))) (let ((_let_28 (bvult v3 (bvor _let_1 _let_0)))) (let ((_let_29 (bvule (bvnor _let_4 (_ bv12 4)) _let_3))) (let ((_let_30 (= _let_11 _let_2))) (let ((_let_31 (bvsge _let_11 ((_ rotate_left 1) v0)))) (let ((_let_32 (bvsle _let_0 _let_1))) (let ((_let_33 (bvslt _let_20 _let_8))) (let ((_let_34 (bvuge _let_12 _let_0))) (let ((_let_35 (bvsgt (ite (= (_ bv1 1) ((_ extract 2 2) v0)) v1 v2) ((_ sign_extend 3) _let_14)))) (let ((_let_36 (bvult v3 _let_4))) (let ((_let_37 (distinct ((_ rotate_left 1) v0) _let_17))) (let ((_let_38 (bvslt _let_1 _let_0))) (let ((_let_39 (bvsge _let_19 _let_24))) (let ((_let_40 (bvsge _let_20 (_ bv12 4)))) (let ((_let_41 (distinct (bvxnor _let_13 ((_ zero_extend 3) (bvcomp v0 (_ bv12 4)))) v2))) (let ((_let_42 (bvule ((_ sign_extend 3) _let_14) _let_6))) (let ((_let_43 (= (bvnor _let_4 (_ bv12 4)) _let_8))) (let ((_let_44 (not _let_43))) (let ((_let_45 (not _let_30))) (let ((_let_46 (not (bvult ((_ rotate_left 1) v0) ((_ zero_extend 3) _let_18))))) (let ((_let_47 (not (bvsgt _let_0 v1)))) (let ((_let_48 (not (bvuge _let_13 _let_24)))) (let ((_let_49 (not (bvsgt ((_ rotate_left 1) v0) ((_ zero_extend 3) _let_9))))) (let ((_let_50 (not (bvsge _let_15 _let_23)))) (let ((_let_51 (not (= _let_7 (bvashr _let_6 _let_3))))) (let ((_let_52 (not _let_37))) (let ((_let_53 (not (= v1 _let_15)))) (let ((_let_54 (not (bvslt _let_20 ((_ zero_extend 3) _let_9))))) (let ((_let_55 (not (= v3 _let_17)))) (and (or _let_44 _let_22 _let_43) (or _let_22 _let_41 (not (bvsge _let_6 _let_11))) (or (not (bvult v3 (bvnor _let_4 (_ bv12 4)))) (not (bvsle _let_12 _let_20)) (not _let_32)) (or (not (bvult _let_4 (_ bv12 4))) (not _let_25) _let_45) (or _let_40 (not (bvuge ((_ sign_extend 3) (ite (bvult _let_13 _let_7) (_ bv1 1) (_ bv0 1))) (bvneg _let_1))) (bvugt _let_1 (bvxnor _let_13 ((_ zero_extend 3) (bvcomp v0 (_ bv12 4)))))) (or (bvslt v3 (ite (= (_ bv1 1) ((_ extract 2 2) v0)) v1 v2)) _let_39 _let_46) (or _let_32 (not (bvsle _let_26 _let_17)) _let_47) (or (bvsle v0 _let_23) _let_48 (not (bvsgt (bvnot (ite (= (_ bv1 1) ((_ extract 2 2) v0)) v1 v2)) _let_7))) (or (not _let_34) (not _let_39) _let_49) (or _let_50 (not _let_41) _let_25) (or (not (bvugt _let_16 _let_7)) (not (bvslt _let_2 ((_ sign_extend 3) (bvcomp v0 (_ bv12 4))))) _let_49) (or _let_33 (not _let_21) _let_22) (or (not (bvult ((_ rotate_left 1) v0) _let_24)) (not (bvsge (_ bv12 4) _let_23)) _let_51) (or (not _let_22) (not (bvslt v2 _let_26)) _let_35) (or _let_21 (not _let_31) _let_35) (or _let_52 _let_53 (bvule ((_ zero_extend 3) (bvnot _let_14)) _let_6)) (or (not _let_40) _let_34 _let_38) (or (not _let_27) _let_36 (bvslt _let_7 ((_ zero_extend 0) (bvnor _let_4 (_ bv12 4))))) (or _let_21 (bvslt _let_19 _let_0) _let_40) (or _let_47 (not (bvuge _let_4 v1)) _let_45) (or _let_50 _let_41 _let_54) (or (not (bvuge (_ bv12 4) v2)) _let_52 _let_25) (or _let_28 (not _let_42) (not _let_35)) (or _let_30 _let_31 _let_28) (or _let_42 (bvsle _let_11 _let_4) _let_36) (or _let_46 _let_33 _let_45) (or _let_38 _let_42 (bvule _let_1 v1)) (or _let_44 (bvsgt _let_12 _let_12) _let_47) (or _let_54 _let_51 (bvslt ((_ sign_extend 3) _let_10) _let_17)) (or (bvugt _let_13 v2) _let_55 (not (bvslt _let_15 ((_ rotate_left 1) v0)))) (or (bvuge _let_4 (bvxor v2 (_ bv12 4))) _let_21 _let_53) (or _let_29 (= (_ bv12 4) _let_2) _let_37) (or _let_55 _let_41 _let_48) (or (not _let_36) (not (bvsge _let_3 _let_26)) _let_27) (or _let_29 (not _let_38) _let_41)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))