(benchmark fuzzsmt
:logic QF_BV
:status unsat
:extrafuns ((v0 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:formula
(let (?e2 bv15[4])
(let (?e3 bv6[4])
(let (?e4 bv13[4])
(let (?e5 bv12[4])
(let (?e6 (ite (bvslt v1 ?e4) bv1[1] bv0[1]))
(let (?e7 (bvxor ?e2 ?e5))
(let (?e8 (sign_extend[1] ?e6))
(let (?e9 (rotate_right[2] ?e2))
(let (?e10 (bvshl v1 ?e4))
(let (?e11 (bvmul v1 (zero_extend[2] ?e8)))
(let (?e12 (ite (bvugt ?e11 ?e10) bv1[1] bv0[1]))
(let (?e13 (bvshl ?e4 ?e5))
(let (?e14 (bvashr (zero_extend[3] ?e12) ?e5))
(let (?e15 (bvnor ?e4 ?e10))
(let (?e16 (ite (bvsgt ?e5 ?e13) bv1[1] bv0[1]))
(let (?e17 (zero_extend[0] ?e11))
(let (?e18 (bvneg ?e14))
(let (?e19 (repeat[4] ?e6))
(let (?e20 (sign_extend[0] ?e9))
(let (?e21 (bvsub v1 ?e2))
(let (?e22 (ite (distinct ?e17 (sign_extend[3] ?e16)) bv1[1] bv0[1]))
(let (?e23 (ite (bvult ?e2 ?e11) bv1[1] bv0[1]))
(let (?e24 (ite (= bv1[1] (extract[3:3] ?e21)) ?e13 ?e4))
(let (?e25 (bvand ?e10 ?e24))
(let (?e26 (ite (= bv1[1] (extract[2:2] ?e14)) (sign_extend[3] ?e6) ?e24))
(let (?e27 (rotate_left[0] ?e23))
(let (?e28 (ite (bvule ?e18 (zero_extend[3] ?e22)) bv1[1] bv0[1]))
(let (?e29 (ite (bvult ?e19 ?e3) bv1[1] bv0[1]))
(let (?e30 (ite (= bv1[1] (extract[0:0] ?e27)) ?e20 ?e20))
(let (?e31 (bvneg ?e29))
(let (?e32 (ite (bvsge ?e10 ?e30) bv1[1] bv0[1]))
(let (?e33 (bvashr ?e28 ?e27))
(let (?e34 (bvnot ?e6))
(let (?e35 (bvnand (zero_extend[3] ?e6) ?e26))
(let (?e36 (ite (bvsge (sign_extend[3] ?e16) ?e18) bv1[1] bv0[1]))
(let (?e37 (ite (bvsgt (sign_extend[3] ?e16) ?e30) bv1[1] bv0[1]))
(let (?e38 (ite (bvsgt ?e31 ?e28) bv1[1] bv0[1]))
(let (?e39 (ite (bvuge ?e32 ?e22) bv1[1] bv0[1]))
(let (?e40 (ite (distinct ?e21 (sign_extend[3] ?e27)) bv1[1] bv0[1]))
(let (?e41 (bvsub ?e15 ?e20))
(let (?e42 (bvcomp (zero_extend[3] ?e34) ?e25))
(let (?e43 (bvneg ?e6))
(let (?e44 (ite (bvslt ?e34 ?e39) bv1[1] bv0[1]))
(let (?e45 (ite (bvsge ?e31 ?e42) bv1[1] bv0[1]))
(let (?e46 (bvnand ?e44 ?e32))
(let (?e47 (ite (bvslt ?e39 ?e6) bv1[1] bv0[1]))
(let (?e48 (ite (distinct v0 ?e35) bv1[1] bv0[1]))
(flet ($e49 (bvult ?e13 (sign_extend[2] ?e8)))
(flet ($e50 (bvsgt ?e39 ?e46))
(flet ($e51 (bvult ?e38 ?e42))
(flet ($e52 (bvult ?e14 (zero_extend[3] ?e33)))
(flet ($e53 (= ?e30 ?e24))
(flet ($e54 (bvult (zero_extend[3] ?e34) ?e35))
(flet ($e55 (bvsle ?e41 (zero_extend[3] ?e27)))
(flet ($e56 (distinct (sign_extend[3] ?e46) v1))
(flet ($e57 (bvsge (sign_extend[3] ?e12) ?e26))
(flet ($e58 (bvule ?e13 (sign_extend[3] ?e22)))
(flet ($e59 (bvsle ?e47 ?e28))
(flet ($e60 (= (zero_extend[3] ?e47) ?e11))
(flet ($e61 (bvsge (zero_extend[3] ?e22) ?e9))
(flet ($e62 (bvult ?e44 ?e37))
(flet ($e63 (distinct ?e30 ?e19))
(flet ($e64 (bvugt ?e38 ?e42))
(flet ($e65 (bvult ?e21 (zero_extend[3] ?e47)))
(flet ($e66 (= ?e43 ?e34))
(flet ($e67 (bvult ?e38 ?e38))
(flet ($e68 (= v0 (sign_extend[3] ?e6)))
(flet ($e69 (bvsle (zero_extend[3] ?e37) ?e7))
(flet ($e70 (bvult ?e12 ?e47))
(flet ($e71 (bvsle (zero_extend[3] ?e6) v1))
(flet ($e72 (bvsle ?e5 ?e13))
(flet ($e73 (bvult ?e33 ?e39))
(flet ($e74 (bvule (sign_extend[3] ?e46) ?e24))
(flet ($e75 (distinct ?e20 ?e20))
(flet ($e76 (bvslt ?e17 (zero_extend[3] ?e40)))
(flet ($e77 (= ?e7 (zero_extend[3] ?e34)))
(flet ($e78 (bvslt ?e15 ?e41))
(flet ($e79 (bvsle ?e34 ?e47))
(flet ($e80 (bvslt (zero_extend[3] ?e36) ?e2))
(flet ($e81 (bvult (sign_extend[3] ?e37) ?e18))
(flet ($e82 (bvugt (zero_extend[3] ?e27) ?e18))
(flet ($e83 (bvugt ?e30 ?e2))
(flet ($e84 (bvsle (sign_extend[3] ?e12) ?e41))
(flet ($e85 (bvsgt ?e10 (zero_extend[3] ?e47)))
(flet ($e86 (bvslt ?e36 ?e38))
(flet ($e87 (bvsgt ?e25 (sign_extend[3] ?e40)))
(flet ($e88 (bvsle (sign_extend[3] ?e32) ?e17))
(flet ($e89 (bvugt (zero_extend[3] ?e6) v0))
(flet ($e90 (bvugt ?e39 ?e47))
(flet ($e91 (bvule ?e18 (zero_extend[3] ?e34)))
(flet ($e92 (bvult ?e43 ?e47))
(flet ($e93 (bvsge (sign_extend[3] ?e29) ?e20))
(flet ($e94 (bvsgt ?e13 (zero_extend[3] ?e36)))
(flet ($e95 (distinct ?e7 ?e7))
(flet ($e96 (bvslt (zero_extend[3] ?e16) ?e30))
(flet ($e97 (bvsgt v1 ?e35))
(flet ($e98 (bvugt ?e22 ?e44))
(flet ($e99 (bvuge ?e2 ?e5))
(flet ($e100 (distinct ?e19 (sign_extend[3] ?e39)))
(flet ($e101 (bvsge ?e4 (sign_extend[3] ?e44)))
(flet ($e102 (bvsgt ?e6 ?e6))
(flet ($e103 (bvsge ?e32 ?e12))
(flet ($e104 (bvsle ?e17 ?e17))
(flet ($e105 (bvsgt ?e16 ?e34))
(flet ($e106 (bvsle ?e26 v1))
(flet ($e107 (bvult ?e13 v0))
(flet ($e108 (bvugt (zero_extend[3] ?e12) ?e25))
(flet ($e109 (= ?e27 ?e34))
(flet ($e110 (bvsge ?e26 (zero_extend[3] ?e28)))
(flet ($e111 (bvslt ?e22 ?e33))
(flet ($e112 (= (zero_extend[1] ?e48) ?e8))
(flet ($e113 (bvslt (sign_extend[3] ?e12) ?e15))
(flet ($e114 (bvsle ?e11 ?e26))
(flet ($e115 (bvult ?e38 ?e16))
(flet ($e116 (bvuge (sign_extend[3] ?e38) ?e4))
(flet ($e117 (= ?e10 (zero_extend[3] ?e32)))
(flet ($e118 (bvsgt (zero_extend[3] ?e27) ?e41))
(flet ($e119 (bvslt ?e10 ?e21))
(flet ($e120 (= ?e12 ?e44))
(flet ($e121 (bvugt ?e9 (sign_extend[3] ?e22)))
(flet ($e122 (bvsle ?e24 (sign_extend[3] ?e29)))
(flet ($e123 (bvule ?e16 ?e44))
(flet ($e124 (bvuge (zero_extend[3] ?e48) ?e11))
(flet ($e125 (bvult ?e39 ?e45))
(flet ($e126 (bvugt ?e40 ?e16))
(flet ($e127 (bvsgt ?e9 ?e3))
(flet ($e128 (bvsgt ?e36 ?e47))
(flet ($e129 (= (zero_extend[3] ?e22) ?e9))
(flet ($e130 (bvule ?e11 (zero_extend[3] ?e16)))
(flet ($e131 (bvslt ?e32 ?e39))
(flet ($e132 (= (zero_extend[3] ?e38) ?e35))
(flet ($e133 (bvsge (sign_extend[3] ?e12) ?e7))
(flet ($e134 (bvult ?e13 ?e14))
(flet ($e135 (bvuge (sign_extend[1] ?e16) ?e8))
(flet ($e136 (bvuge ?e9 (zero_extend[3] ?e33)))
(flet ($e137 (bvule ?e14 ?e10))
(flet ($e138 (= (sign_extend[3] ?e43) ?e11))
(flet ($e139 (bvsge ?e39 ?e44))
(flet ($e140 (bvsle ?e2 ?e18))
(flet ($e141 (bvslt (sign_extend[3] ?e31) ?e4))
(flet ($e142 (bvsge ?e9 (zero_extend[3] ?e27)))
(flet ($e143 (bvsgt ?e18 (zero_extend[3] ?e39)))
(flet ($e144 (bvsge ?e5 (zero_extend[3] ?e23)))
(flet ($e145 
(and
 (or $e117 (not $e78) $e113)
 (or (not $e104) (not $e95) (not $e138))
 (or (not $e105) $e83 (not $e138))
 (or $e121 (not $e67) (not $e106))
 (or (not $e75) $e116 $e131)
 (or $e96 (not $e103) $e120)
 (or $e64 (not $e105) $e86)
 (or $e132 (not $e131) (not $e127))
 (or $e67 (not $e121) $e135)
 (or $e58 (not $e73) (not $e120))
 (or (not $e90) (not $e54) $e119)
 (or $e103 (not $e122) (not $e144))
 (or (not $e141) $e140 $e89)
 (or (not $e73) $e60 $e79)
 (or $e89 $e129 (not $e74))
 (or $e92 (not $e112) (not $e60))
 (or (not $e139) (not $e126) (not $e101))
 (or $e64 $e104 $e101)
 (or (not $e112) $e53 $e91)
 (or (not $e128) $e93 (not $e131))
 (or $e113 (not $e99) (not $e73))
 (or $e86 (not $e70) $e66)
 (or $e131 (not $e125) $e140)
 (or (not $e51) $e140 (not $e102))
 (or $e68 (not $e144) (not $e119))
 (or (not $e132) $e66 $e114)
 (or (not $e137) (not $e73) $e108)
 (or $e86 (not $e57) (not $e75))
 (or (not $e59) (not $e124) (not $e81))
 (or $e130 $e121 $e130)
 (or $e138 (not $e136) (not $e129))
 (or $e108 $e115 $e55)
 (or (not $e130) $e63 $e107)
 (or $e142 $e92 $e65)
 (or (not $e130) $e140 (not $e64))
 (or $e123 (not $e92) (not $e115))
 (or (not $e51) $e54 (not $e77))
 (or $e70 (not $e75) $e129)
 (or $e93 (not $e74) (not $e144))
 (or $e104 $e68 (not $e136))
 (or (not $e92) (not $e126) $e111)
 (or (not $e105) $e91 (not $e52))
 (or (not $e57) (not $e88) (not $e75))
 (or $e127 $e114 $e99)
 (or $e125 (not $e85) $e123)
 (or (not $e90) (not $e49) (not $e112))
 (or $e135 (not $e110) (not $e61))
 (or $e73 $e124 (not $e115))
))
$e145
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))