(benchmark fuzzsmt
:logic QF_BV
:status sat
:extrafuns ((v0 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:extrafuns ((v2 BitVec[4]))
:extrafuns ((v3 BitVec[4]))
:extrafuns ((v4 BitVec[4]))
:formula
(let (?e5 bv12[4])
(let (?e6 bv12[4])
(let (?e7 (ite (= bv1[1] (extract[2:2] v0)) v1 v2))
(let (?e8 (rotate_left[1] v0))
(let (?e9 (bvnot ?e8))
(let (?e10 (bvnot v2))
(let (?e11 (bvcomp v0 ?e5))
(let (?e12 (bvashr v1 ?e10))
(let (?e13 (repeat[1] ?e9))
(let (?e14 (zero_extend[0] ?e6))
(let (?e15 (ite (bvsge ?e7 ?e14) bv1[1] bv0[1]))
(let (?e16 (bvlshr ?e12 ?e9))
(let (?e17 (bvxor v4 ?e8))
(let (?e18 (bvneg ?e10))
(let (?e19 (bvnor ?e14 ?e5))
(let (?e20 (bvneg ?e16))
(let (?e21 (ite (bvsgt ?e8 ?e10) bv1[1] bv0[1]))
(let (?e22 (ite (bvslt ?e18 v4) bv1[1] bv0[1]))
(let (?e23 (ite (= bv1[1] (extract[0:0] ?e21)) (zero_extend[3] ?e15) ?e10))
(let (?e24 (bvshl ?e6 ?e14))
(let (?e25 (rotate_left[0] ?e10))
(let (?e26 (ite (bvult ?e25 ?e17) bv1[1] bv0[1]))
(let (?e27 (ite (bvult v1 ?e9) bv1[1] bv0[1]))
(let (?e28 (zero_extend[0] ?e19))
(let (?e29 (bvor ?e10 ?e9))
(let (?e30 (ite (bvule ?e6 ?e20) bv1[1] bv0[1]))
(let (?e31 (bvxor v2 ?e6))
(let (?e32 (bvmul ?e13 (zero_extend[3] ?e21)))
(let (?e33 (bvnot ?e27))
(let (?e34 (sign_extend[0] ?e16))
(let (?e35 (bvashr ?e16 ?e13))
(let (?e36 (bvnot ?e7))
(let (?e37 (bvxnor ?e25 (zero_extend[3] ?e11)))
(let (?e38 (rotate_right[3] ?e37))
(let (?e39 (ite (bvult ?e14 (sign_extend[3] ?e33)) bv1[1] bv0[1]))
(let (?e40 (bvxor ?e34 ?e6))
(let (?e41 (bvlshr ?e16 v3))
(flet ($e42 (bvult ?e14 ?e6))
(flet ($e43 (distinct ?e22 ?e15))
(flet ($e44 (bvslt v0 ?e7))
(flet ($e45 (= ?e7 ?e37))
(flet ($e46 (bvslt ?e13 ?e9))
(flet ($e47 (bvsge ?e32 (sign_extend[3] ?e39)))
(flet ($e48 (bvuge ?e37 ?e32))
(flet ($e49 (bvsgt ?e36 ?e17))
(flet ($e50 (bvslt v3 ?e7))
(flet ($e51 (bvult ?e24 ?e16))
(flet ($e52 (bvuge ?e16 (zero_extend[3] ?e39)))
(flet ($e53 (= v3 ?e38))
(flet ($e54 (bvult ?e8 (sign_extend[3] ?e21)))
(flet ($e55 (= ?e37 v4))
(flet ($e56 (bvslt v2 (sign_extend[3] ?e30)))
(flet ($e57 (bvule ?e37 (zero_extend[3] ?e26)))
(flet ($e58 (bvult v3 ?e19))
(flet ($e59 (bvslt ?e10 (sign_extend[3] ?e15)))
(flet ($e60 (= ?e6 ?e12))
(flet ($e61 (bvule ?e28 (sign_extend[3] ?e39)))
(flet ($e62 (= ?e17 ?e35))
(flet ($e63 (bvslt ?e41 (zero_extend[3] ?e21)))
(flet ($e64 (bvugt v0 ?e13))
(flet ($e65 (bvuge ?e14 v1))
(flet ($e66 (bvuge (sign_extend[3] ?e26) ?e18))
(flet ($e67 (bvult v3 ?e29))
(flet ($e68 (bvule ?e10 v1))
(flet ($e69 (bvule ?e19 ?e13))
(flet ($e70 (= ?e23 ?e12))
(flet ($e71 (bvslt ?e17 ?e28))
(flet ($e72 (bvule (zero_extend[3] ?e33) ?e16))
(flet ($e73 (bvsge ?e23 ?e8))
(flet ($e74 (bvsle ?e9 ?e10))
(flet ($e75 (bvslt ?e41 ?e20))
(flet ($e76 (bvsle (sign_extend[3] ?e30) ?e38))
(flet ($e77 (bvuge ?e41 (sign_extend[3] ?e11)))
(flet ($e78 (bvsle ?e24 ?e41))
(flet ($e79 (bvuge ?e25 (sign_extend[3] ?e21)))
(flet ($e80 (bvuge ?e24 ?e9))
(flet ($e81 (bvuge ?e6 v2))
(flet ($e82 (bvsge ?e13 (sign_extend[3] ?e30)))
(flet ($e83 (bvsge ?e5 (sign_extend[3] ?e39)))
(flet ($e84 (bvsgt ?e7 (sign_extend[3] ?e27)))
(flet ($e85 (bvsle ?e23 ?e14))
(flet ($e86 (bvult ?e8 (zero_extend[3] ?e39)))
(flet ($e87 (bvugt ?e25 v2))
(flet ($e88 (bvslt ?e12 (sign_extend[3] ?e11)))
(flet ($e89 (bvult v3 ?e14))
(flet ($e90 (distinct ?e8 ?e38))
(flet ($e91 (bvslt ?e10 ?e9))
(flet ($e92 (bvslt ?e32 ?e8))
(flet ($e93 (bvsle v0 (sign_extend[3] ?e39)))
(flet ($e94 (= v1 ?e32))
(flet ($e95 (bvule ?e30 ?e15))
(flet ($e96 (bvult (sign_extend[3] ?e33) ?e9))
(flet ($e97 (bvsge ?e16 ?e23))
(flet ($e98 (bvsge ?e40 (sign_extend[3] ?e21)))
(flet ($e99 (bvuge ?e14 ?e31))
(flet ($e100 (bvslt ?e40 ?e9))
(flet ($e101 (bvsge ?e41 ?e6))
(flet ($e102 (bvsgt ?e24 ?e24))
(flet ($e103 (distinct ?e37 v2))
(flet ($e104 (distinct ?e35 v3))
(flet ($e105 (distinct v1 (zero_extend[3] ?e21)))
(flet ($e106 (bvsgt ?e9 v1))
(flet ($e107 (bvugt ?e10 ?e37))
(flet ($e108 (bvsgt ?e8 (zero_extend[3] ?e21)))
(flet ($e109 (bvule (sign_extend[3] ?e27) ?e16))
(flet ($e110 (= ?e19 ?e20))
(flet ($e111 (bvslt (sign_extend[3] ?e22) ?e38))
(flet ($e112 (bvugt ?e34 ?e17))
(flet ($e113 
(and
 (or (not $e110) $e45 $e110)
 (or $e45 $e103 (not $e97))
 (or (not $e58) (not $e78) (not $e74))
 (or (not $e42) (not $e55) (not $e70))
 (or $e101 (not $e66) $e107)
 (or $e50 $e98 (not $e86))
 (or $e74 (not $e76) (not $e106))
 (or $e93 (not $e79) (not $e49))
 (or (not $e80) (not $e98) (not $e108))
 (or (not $e47) (not $e103) $e55)
 (or (not $e112) (not $e88) (not $e108))
 (or $e75 (not $e43) $e45)
 (or (not $e54) (not $e83) (not $e62))
 (or (not $e45) (not $e56) $e84)
 (or $e43 (not $e73) $e84)
 (or (not $e90) (not $e94) $e72)
 (or (not $e101) $e80 $e91)
 (or (not $e64) $e89 $e71)
 (or $e43 $e100 $e101)
 (or (not $e106) (not $e65) (not $e70))
 (or (not $e47) $e103 (not $e63))
 (or (not $e81) (not $e90) $e55)
 (or $e67 (not $e109) (not $e84))
 (or $e70 $e73 $e67)
 (or $e109 $e85 $e89)
 (or (not $e86) $e75 (not $e70))
 (or $e91 $e109 $e68)
 (or (not $e110) $e102 (not $e106))
 (or (not $e63) (not $e62) $e111)
 (or $e87 (not $e53) (not $e92))
 (or $e99 $e43 (not $e94))
 (or $e69 $e60 $e90)
 (or (not $e53) $e103 (not $e79))
 (or (not $e89) (not $e82) $e64)
 (or $e69 (not $e91) $e103)
))
$e113
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))