(set-option :incremental false)
(set-info :status unsat)
(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 (bvlshr (_ bv4 4) v0))) (let ((_let_1 (ite (= (_ bv1 1) ((_ extract 1 1) (_ bv4 4))) v2 v1))) (let ((_let_2 (bvnot (_ bv4 4)))) (let ((_let_3 (bvlshr (_ bv4 4) v3))) (let ((_let_4 (bvneg (bvsub (_ bv4 4) (_ bv12 4))))) (let ((_let_5 (bvadd _let_0 _let_3))) (let ((_let_6 (bvsub ((_ zero_extend 0) (_ bv4 4)) _let_3))) (let ((_let_7 (ite (bvugt v1 (_ bv4 4)) (_ bv1 1) (_ bv0 1)))) (let ((_let_8 (bvashr _let_3 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)))) (let ((_let_9 (bvadd (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_1))) (let ((_let_10 ((_ zero_extend 3) _let_7))) (let ((_let_11 (ite (bvslt _let_10 v3) (_ bv1 1) (_ bv0 1)))) (let ((_let_12 (ite (bvugt _let_1 ((_ sign_extend 0) _let_1)) (_ bv1 1) (_ bv0 1)))) (let ((_let_13 (bvnot (bvadd ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)))))) (let ((_let_14 (ite (bvult (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ zero_extend 0) (_ bv4 4))) (_ bv1 1) (_ bv0 1)))) (let ((_let_15 (bvsub v1 ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (let ((_let_16 ((_ zero_extend 0) _let_8))) (let ((_let_17 ((_ sign_extend 0) _let_6))) (let ((_let_18 (ite (bvult _let_9 (bvsub (_ bv4 4) (_ bv12 4))) (_ bv1 1) (_ bv0 1)))) (let ((_let_19 (bvcomp v0 _let_15))) (let ((_let_20 (bvand v0 _let_15))) (let ((_let_21 ((_ zero_extend 0) (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (let ((_let_22 (ite (= (_ bv1 1) ((_ extract 0 0) _let_3)) _let_20 ((_ sign_extend 3) _let_7)))) (let ((_let_23 ((_ sign_extend 0) (ite (bvslt _let_5 ((_ zero_extend 3) _let_12)) (_ bv1 1) (_ bv0 1))))) (let ((_let_24 ((_ sign_extend 0) _let_5))) (let ((_let_25 ((_ sign_extend 3) _let_11))) (let ((_let_26 (bvnot (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (let ((_let_27 (bvand _let_20 _let_26))) (let ((_let_28 (bvneg _let_6))) (let ((_let_29 (bvor _let_21 _let_6))) (let ((_let_30 (ite (bvslt v1 _let_2) (_ bv1 1) (_ bv0 1)))) (let ((_let_31 ((_ sign_extend 3) (bvashr _let_11 _let_7)))) (let ((_let_32 (bvshl ((_ zero_extend 0) (_ bv4 4)) _let_31))) (let ((_let_33 (ite (bvsge ((_ zero_extend 3) (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))) _let_20) (_ bv1 1) (_ bv0 1)))) (let ((_let_34 ((_ extract 3 0) ((_ rotate_right 3) v3)))) (let ((_let_35 ((_ zero_extend 0) (bvxnor ((_ zero_extend 2) ((_ extract 1 0) v0)) (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8))))) (let ((_let_36 (bvule ((_ extract 1 0) v0) ((_ zero_extend 1) (bvashr _let_11 _let_7))))) (let ((_let_37 ((_ sign_extend 3) _let_14))) (let ((_let_38 (distinct _let_4 _let_37))) (let ((_let_39 (bvule ((_ sign_extend 3) _let_19) _let_21))) (let ((_let_40 (bvugt _let_17 _let_8))) (let ((_let_41 (bvsle _let_9 ((_ zero_extend 3) (ite (bvslt _let_5 ((_ zero_extend 3) _let_12)) (_ bv1 1) (_ bv0 1)))))) (let ((_let_42 (bvsgt _let_18 (bvneg (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (let ((_let_43 (bvsge ((_ zero_extend 1) _let_12) ((_ rotate_right 0) ((_ extract 1 0) v0))))) (let ((_let_44 (bvule _let_33 (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))))) (let ((_let_45 (= (bvadd ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))) _let_6))) (let ((_let_46 (bvsge _let_8 ((_ zero_extend 3) (bvneg (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))))))) (let ((_let_47 (bvsgt _let_13 (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (let ((_let_48 (bvslt _let_21 _let_8))) (let ((_let_49 (bvsge _let_2 _let_24))) (let ((_let_50 (bvugt _let_28 _let_22))) (let ((_let_51 (bvsle ((_ rotate_right 3) v3) (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8)))) (let ((_let_52 (distinct (_ bv4 4) (bvnot _let_3)))) (let ((_let_53 ((_ zero_extend 3) (bvashr _let_11 _let_7)))) (let ((_let_54 (bvsle ((_ zero_extend 3) (ite (bvslt _let_5 ((_ zero_extend 3) _let_12)) (_ bv1 1) (_ bv0 1))) (_ bv4 4)))) (let ((_let_55 (bvsle (_ bv4 4) _let_31))) (let ((_let_56 (= _let_9 (_ bv12 4)))) (let ((_let_57 (distinct _let_2 _let_25))) (let ((_let_58 (bvugt (bvsub (_ bv4 4) (_ bv12 4)) (_ bv4 4)))) (let ((_let_59 (= _let_0 _let_34))) (let ((_let_60 (distinct (bvashr _let_11 _let_7) _let_30))) (let ((_let_61 (bvule ((_ zero_extend 3) (ite (bvsle ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_15) (_ bv1 1) (_ bv0 1))) _let_16))) (let ((_let_62 (bvslt v4 _let_24))) (let ((_let_63 (= _let_3 v0))) (let ((_let_64 (bvslt v0 ((_ zero_extend 3) (bvneg (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))))))) (let ((_let_65 (bvule ((_ sign_extend 3) (ite (distinct _let_29 ((_ zero_extend 3) (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))) _let_21))) (let ((_let_66 (bvule ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_2))) (let ((_let_67 (bvugt _let_28 ((_ zero_extend 3) _let_12)))) (let ((_let_68 (= _let_35 _let_4))) (let ((_let_69 (distinct v1 (bvnot _let_3)))) (let ((_let_70 (bvsgt _let_24 ((_ zero_extend 3) _let_23)))) (let ((_let_71 (bvsge ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_24))) (let ((_let_72 (= _let_13 ((_ zero_extend 3) _let_14)))) (let ((_let_73 (distinct (ite (distinct _let_29 ((_ zero_extend 3) (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)) _let_14))) (let ((_let_74 (bvsle (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_12))) (let ((_let_75 (bvuge _let_35 _let_24))) (let ((_let_76 (bvule _let_22 _let_8))) (let ((_let_77 (distinct (_ bv4 4) _let_25))) (let ((_let_78 (bvule _let_9 v1))) (let ((_let_79 (= _let_26 (bvnot _let_3)))) (let ((_let_80 (bvsgt (_ bv4 4) ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (let ((_let_81 (= _let_9 (bvsub (_ bv4 4) (_ bv12 4))))) (let ((_let_82 (bvugt _let_34 _let_32))) (let ((_let_83 (distinct (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ zero_extend 3) _let_11)))) (let ((_let_84 (= ((_ sign_extend 3) _let_23) _let_2))) (let ((_let_85 (bvsle (bvsub (_ bv4 4) (_ bv12 4)) _let_28))) (let ((_let_86 (bvugt ((_ sign_extend 0) _let_1) ((_ zero_extend 2) ((_ rotate_right 0) ((_ extract 1 0) v0)))))) (let ((_let_87 (bvslt ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_37))) (let ((_let_88 (bvsge _let_30 _let_18))) (let ((_let_89 (bvuge _let_53 _let_13))) (let ((_let_90 (distinct _let_34 _let_31))) (let ((_let_91 (bvult (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8) _let_16))) (let ((_let_92 (not _let_67))) (let ((_let_93 (not (bvsle _let_5 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (let ((_let_94 (not (bvsge _let_22 _let_27)))) (let ((_let_95 (not _let_88))) (let ((_let_96 (not (bvule (bvxnor ((_ zero_extend 2) ((_ extract 1 0) v0)) (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8)) ((_ zero_extend 3) _let_30))))) (let ((_let_97 (not (bvult (_ bv4 4) _let_32)))) (let ((_let_98 (not (= v0 _let_35)))) (let ((_let_99 (not (bvsge ((_ sign_extend 3) _let_18) v0)))) (let ((_let_100 (not (bvule (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ rotate_right 3) v3))))) (let ((_let_101 (not (distinct _let_35 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (let ((_let_102 (not _let_44))) (let ((_let_103 (not _let_77))) (let ((_let_104 (not _let_75))) (let ((_let_105 (not (bvslt _let_25 _let_20)))) (let ((_let_106 (not _let_56))) (let ((_let_107 (not _let_52))) (let ((_let_108 (not _let_48))) (let ((_let_109 (not _let_60))) (let ((_let_110 (not _let_70))) (let ((_let_111 (not _let_78))) (let ((_let_112 (not (bvsle (bvshl ((_ sign_extend 3) (ite (bvugt _let_14 (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) v4) ((_ zero_extend 3) _let_18))))) (let ((_let_113 (not (bvsgt _let_4 ((_ sign_extend 3) _let_12))))) (let ((_let_114 (not _let_39))) (let ((_let_115 (not _let_45))) (let ((_let_116 (not (bvsle (_ bv12 4) _let_17)))) (let ((_let_117 (not _let_58))) (let ((_let_118 (not (bvule _let_15 ((_ sign_extend 0) _let_1))))) (let ((_let_119 (not (bvuge (bvsub (_ bv4 4) (_ bv12 4)) _let_31)))) (let ((_let_120 (not (= ((_ zero_extend 3) (ite (bvslt _let_5 ((_ zero_extend 3) _let_12)) (_ bv1 1) (_ bv0 1))) _let_3)))) (and (or (not _let_47) (bvslt (bvsub (_ bv4 4) (_ bv12 4)) ((_ zero_extend 3) (bvneg (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))))) _let_68) (or _let_76 _let_92 _let_45) (or _let_93 (bvslt _let_6 ((_ zero_extend 3) (ite (distinct _let_29 ((_ zero_extend 3) (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (not _let_41)) (or _let_61 (not _let_65) _let_70) (or _let_51 (not (bvsge _let_29 ((_ zero_extend 3) (ite (bvsle ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_15) (_ bv1 1) (_ bv0 1))))) _let_94) (or _let_74 (bvult _let_9 _let_17) (not (bvslt _let_34 (bvxnor ((_ zero_extend 2) ((_ extract 1 0) v0)) (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8))))) (or _let_48 _let_36 (= v3 _let_32)) (or _let_79 _let_65 _let_61) (or _let_83 (not _let_54) (not _let_79)) (or (not _let_89) _let_95 _let_96) (or _let_97 _let_98 _let_99) (or (not _let_82) _let_85 _let_69) (or _let_76 _let_100 _let_101) (or _let_78 _let_84 (= _let_22 (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8))) (or _let_72 (not (bvuge ((_ sign_extend 3) (ite (bvsle ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_15) (_ bv1 1) (_ bv0 1))) (bvadd ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) _let_59) (or (not (bvuge ((_ zero_extend 3) (ite (bvsle ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_15) (_ bv1 1) (_ bv0 1))) v3)) (not (bvugt (bvnot _let_3) _let_25)) _let_54) (or (not _let_76) (not (bvult _let_0 (_ bv4 4))) (not _let_91)) (or _let_57 (bvugt _let_2 ((_ zero_extend 3) _let_12)) _let_102) (or (not (bvugt _let_0 v3)) _let_103 _let_104) (or _let_102 _let_59 _let_88) (or (not (bvult _let_28 ((_ zero_extend 3) _let_18))) (not _let_61) _let_42) (or _let_38 _let_105 _let_64) (or (not (bvsgt _let_8 _let_29)) (not _let_85) _let_49) (or _let_50 (bvule _let_11 _let_30) (not (bvult _let_22 ((_ zero_extend 0) (_ bv4 4))))) (or _let_106 _let_58 _let_62) (or (not (= (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) _let_27)) _let_89 _let_86) (or (not _let_74) (= _let_29 _let_13) _let_107) (or _let_36 _let_81 _let_91) (or _let_67 _let_93 _let_51) (or _let_66 _let_57 _let_42) (or (not _let_36) _let_94 (distinct _let_9 ((_ sign_extend 3) _let_33))) (or _let_108 _let_109 (not (bvsgt _let_33 _let_11))) (or _let_110 (not (bvsle ((_ zero_extend 3) (ite (bvugt _let_14 (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) _let_20)) (not _let_87)) (or (not _let_73) _let_108 _let_84) (or _let_90 _let_111 (bvugt _let_53 _let_13)) (or (bvule _let_23 _let_19) _let_81 (bvsle (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))) (or (not (bvsgt _let_35 ((_ zero_extend 3) (bvneg (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1)))))) _let_92 _let_71) (or (not _let_46) (not (bvsgt ((_ zero_extend 3) (ite (bvslt _let_5 ((_ zero_extend 3) _let_12)) (_ bv1 1) (_ bv0 1))) (bvshl ((_ sign_extend 3) (ite (bvugt _let_14 (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) v4))) (bvugt _let_15 _let_32)) (or _let_44 _let_112 _let_70) (or _let_93 (not _let_55) _let_86) (or _let_82 (not _let_71) _let_111) (or _let_113 _let_114 _let_115) (or (not _let_49) _let_101 _let_56) (or (not (= _let_1 _let_29)) _let_109 (not (= (bvneg (ite (= _let_1 v2) (_ bv1 1) (_ bv0 1))) _let_33))) (or _let_115 _let_102 _let_78) (or _let_75 (not (distinct (bvsub (_ bv4 4) (_ bv12 4)) (bvadd ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))))) (not (bvult _let_18 _let_12))) (or _let_75 _let_92 (not _let_83)) (or _let_106 (not (bvsgt (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8) _let_22)) _let_97) (or (bvsgt _let_8 _let_28) _let_64 _let_116) (or _let_45 _let_41 _let_73) (or _let_96 _let_103 _let_117) (or _let_67 _let_58 _let_88) (or _let_38 _let_44 _let_118) (or _let_95 (not (bvsge (bvmul _let_0 (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) (bvsub (_ bv4 4) (_ bv12 4)))) (not (bvslt (bvsub (_ bv4 4) (_ bv12 4)) _let_24))) (or _let_63 _let_118 _let_112) (or _let_104 _let_55 _let_93) (or _let_87 (bvsge _let_35 ((_ zero_extend 0) (_ bv4 4))) (= _let_33 _let_33)) (or _let_110 (distinct _let_28 (bvsub (_ bv4 4) (_ bv12 4))) _let_77) (or _let_39 _let_80 _let_93) (or _let_99 _let_116 (not _let_63)) (or (not (bvsge ((_ zero_extend 1) _let_19) ((_ rotate_right 0) ((_ extract 1 0) v0)))) (not (bvslt _let_35 _let_26)) _let_46) (or _let_68 _let_119 _let_47) (or _let_111 (not _let_43) (not _let_57)) (or _let_60 _let_57 (bvslt v2 v3)) (or _let_98 (not (bvugt (bvadd ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0)) ((_ zero_extend 0) (bvmul (bvsub (_ bv4 4) (_ bv12 4)) v0))) ((_ zero_extend 0) (_ bv4 4)))) _let_43) (or _let_117 (not _let_84) _let_104) (or (distinct _let_28 _let_9) (not _let_40) _let_116) (or _let_69 _let_62 _let_52) (or (not _let_81) (not _let_72) (bvuge (bvxnor ((_ zero_extend 2) ((_ extract 1 0) v0)) (ite (= (_ bv1 1) ((_ extract 2 2) _let_20)) _let_25 _let_8)) ((_ rotate_right 3) v3))) (or _let_68 _let_100 _let_80) (or _let_52 _let_90 _let_120) (or _let_119 _let_56 _let_46) (or (not _let_90) _let_105 (= _let_9 _let_3)) (or _let_114 _let_40 _let_113) (or (not _let_50) _let_75 _let_61) (or _let_120 _let_66 _let_48) (or (not (bvuge _let_31 _let_34)) _let_107 (bvuge _let_13 _let_10)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))