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