blob: 0e80fb969a996ab7516b66897709c8e7b9b6a9ef (
plain)
1
2
3
4
5
6
7
8
|
(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))
(check-sat-assuming ( (let ((_let_0 (ite (bvslt (_ bv11 4) (_ bv9 4)) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 (ite (bvslt v0 (_ bv11 4)) (_ bv1 1) (_ bv0 1)))) (let ((_let_2 ((_ zero_extend 0) v3))) (let ((_let_3 (bvxnor ((_ sign_extend 3) _let_0) (_ bv11 4)))) (let ((_let_4 (bvnot v3))) (let ((_let_5 (ite (bvugt _let_3 v3) (_ bv1 1) (_ bv0 1)))) (let ((_let_6 (bvcomp (bvxnor (bvor ((_ sign_extend 3) _let_0) (_ bv8 4)) (_ bv9 4)) _let_3))) (let ((_let_7 (bvxnor v3 (_ bv11 4)))) (let ((_let_8 ((_ rotate_right 0) _let_1))) (let ((_let_9 (bvadd v1 (bvor ((_ zero_extend 3) _let_0) (bvxnor (bvor ((_ sign_extend 3) _let_0) (_ bv8 4)) (_ bv9 4)))))) (let ((_let_10 (ite (bvule _let_2 (_ bv8 4)) (_ bv1 1) (_ bv0 1)))) (let ((_let_11 (ite (bvsle (_ bv8 4) ((_ sign_extend 3) _let_1)) (_ bv1 1) (_ bv0 1)))) (let ((_let_12 (ite (bvuge _let_9 v3) (_ bv1 1) (_ bv0 1)))) (let ((_let_13 (ite (bvsgt _let_2 ((_ sign_extend 3) _let_0)) (_ bv1 1) (_ bv0 1)))) (let ((_let_14 (ite (= (_ bv1 1) ((_ extract 0 0) _let_13)) ((_ sign_extend 3) (bvashr _let_8 (bvxnor _let_1 _let_6))) (_ bv11 4)))) (let ((_let_15 (ite (bvugt v1 _let_7) (_ bv1 1) (_ bv0 1)))) (let ((_let_16 (bvand v2 _let_9))) (let ((_let_17 (bvult (bvor ((_ zero_extend 3) _let_0) (bvxnor (bvor ((_ sign_extend 3) _let_0) (_ bv8 4)) (_ bv9 4))) _let_14))) (let ((_let_18 (bvslt ((_ sign_extend 3) _let_8) _let_7))) (let ((_let_19 (bvult ((_ zero_extend 3) (bvashr _let_8 (bvxnor _let_1 _let_6))) _let_14))) (let ((_let_20 (distinct _let_4 _let_3))) (let ((_let_21 (bvslt _let_7 _let_2))) (let ((_let_22 ((_ sign_extend 3) (bvxnor _let_1 _let_6)))) (let ((_let_23 (bvsle _let_3 _let_22))) (let ((_let_24 (bvsgt (bvor ((_ zero_extend 3) _let_0) (bvxnor (bvor ((_ sign_extend 3) _let_0) (_ bv8 4)) (_ bv9 4))) ((_ zero_extend 3) (bvneg _let_8))))) (let ((_let_25 (bvsgt _let_16 (bvor ((_ sign_extend 3) _let_0) (_ bv8 4))))) (let ((_let_26 ((_ sign_extend 3) _let_5))) (let ((_let_27 (bvsgt _let_26 v1))) (let ((_let_28 ((_ sign_extend 3) (bvnot _let_8)))) (let ((_let_29 (distinct (_ bv11 4) _let_28))) (let ((_let_30 (bvsgt _let_16 _let_28))) (let ((_let_31 (bvule (bvxnor _let_1 _let_6) _let_5))) (let ((_let_32 (= _let_12 _let_8))) (let ((_let_33 (bvult (bvashr _let_8 (bvxnor _let_1 _let_6)) (bvnot _let_8)))) (let ((_let_34 (bvugt (_ bv9 4) _let_28))) (let ((_let_35 (bvule _let_15 _let_10))) (let ((_let_36 (bvuge ((_ sign_extend 3) (bvashr _let_8 (bvxnor _let_1 _let_6))) _let_4))) (let ((_let_37 (bvsgt _let_14 v1))) (let ((_let_38 (bvule _let_7 _let_14))) (let ((_let_39 (bvsle ((_ sign_extend 3) _let_6) v1))) (let ((_let_40 (bvslt (_ bv9 4) v3))) (let ((_let_41 (bvult v1 _let_16))) (let ((_let_42 (bvsge ((_ sign_extend 3) (bvashr _let_8 (bvxnor _let_1 _let_6))) (bvor ((_ sign_extend 3) _let_0) (_ bv8 4))))) (let ((_let_43 (bvslt _let_7 _let_3))) (let ((_let_44 (bvsge _let_0 (bvneg _let_8)))) (let ((_let_45 (distinct _let_7 _let_16))) (let ((_let_46 (bvslt v3 _let_22))) (let ((_let_47 (bvsge _let_12 _let_1))) (let ((_let_48 (not (bvsgt (_ bv8 4) (_ bv9 4))))) (let ((_let_49 (not (bvslt _let_14 _let_9)))) (let ((_let_50 (not _let_33))) (let ((_let_51 (not (= _let_6 _let_8)))) (let ((_let_52 (not (bvugt ((_ zero_extend 3) _let_8) _let_3)))) (let ((_let_53 (not (bvsge _let_13 (bvneg _let_8))))) (and (or _let_44 _let_25 _let_34) (or (not _let_45) (not _let_43) (not _let_19)) (or _let_19 (not _let_24) _let_34) (or (not (bvslt v0 ((_ zero_extend 3) _let_8))) _let_48 _let_40) (or _let_36 (bvslt ((_ sign_extend 3) _let_11) (bvor ((_ zero_extend 3) _let_0) (bvxnor (bvor ((_ sign_extend 3) _let_0) (_ bv8 4)) (_ bv9 4)))) (not _let_27)) (or _let_17 (not (bvult (bvxnor _let_1 _let_6) _let_8)) (not (distinct _let_13 _let_0))) (or _let_19 _let_46 (not _let_44)) (or _let_41 (not _let_42) _let_48) (or (not _let_32) _let_46 _let_20) (or (not (bvuge (ite (bvsle (_ bv8 4) _let_3) (_ bv1 1) (_ bv0 1)) (bvneg _let_8))) _let_49 (bvslt ((_ zero_extend 3) _let_11) (_ bv9 4))) (or _let_23 _let_50 (bvsge _let_13 (bvneg _let_8))) (or _let_30 _let_51 (not (distinct (bvnot _let_8) (bvneg _let_8)))) (or _let_17 _let_32 (not _let_18)) (or _let_42 (not _let_25) _let_37) (or _let_29 (not (bvsge _let_14 _let_26)) _let_17) (or _let_52 _let_36 _let_23) (or _let_33 (not (bvult v1 (bvor ((_ zero_extend 3) _let_0) (bvxnor (bvor ((_ sign_extend 3) _let_0) (_ bv8 4)) (_ bv9 4))))) (not _let_41)) (or _let_49 _let_35 _let_52) (or _let_31 _let_20 _let_43) (or _let_50 _let_29 _let_27) (or (not _let_31) _let_43 (not _let_47)) (or _let_38 _let_24 _let_17) (or _let_51 (not (bvule (bvxnor (bvor ((_ sign_extend 3) _let_0) (_ bv8 4)) (_ bv9 4)) ((_ sign_extend 3) _let_15))) _let_39) (or _let_51 _let_33 _let_38) (or (not (distinct v0 _let_2)) (not _let_39) _let_37) (or (not (bvsge v3 _let_7)) (not _let_37) _let_45) (or (not (distinct _let_16 _let_7)) (not _let_23) (bvuge (bvashr _let_8 (bvxnor _let_1 _let_6)) _let_12)) (or (not (bvsge (bvneg _let_8) _let_6)) _let_21 (not _let_34)) (or _let_53 _let_21 (bvuge _let_6 _let_10)) (or (not (bvsge _let_2 _let_22)) _let_37 _let_18) (or _let_40 _let_38 _let_53) (or _let_51 _let_52 _let_30) (or (not (bvsgt v0 _let_16)) (not _let_35) _let_47)))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))
|
