(benchmark fuzzsmt
:logic QF_BV
:status unknown
:extrafuns ((v0 BitVec[10]))
:formula
(let (?e1 bv30369[16])
(let (?e2 bv3[2])
(let (?e3 (ite (bvule ?e1 ?e1) bv1[1] bv0[1]))
(let (?e4 (bvcomp (zero_extend[1] ?e3) ?e2))
(let (?e5 (ite (bvsgt (sign_extend[15] ?e4) ?e1) bv1[1] bv0[1]))
(let (?e6 (bvsmod ?e1 ?e1))
(let (?e7 (bvsdiv v0 v0))
(flet ($e8 (bvult ?e2 ?e2))
(flet ($e9 (bvsge ?e7 (zero_extend[9] ?e3)))
(flet ($e10 (bvugt (sign_extend[15] ?e4) ?e6))
(flet ($e11 (bvsgt (sign_extend[15] ?e3) ?e6))
(flet ($e12 (bvsgt v0 (sign_extend[9] ?e3)))
(flet ($e13 (bvsgt ?e4 ?e4))
(flet ($e14 (bvsle ?e1 (zero_extend[14] ?e2)))
(flet ($e15 (bvslt (sign_extend[14] ?e2) ?e6))
(flet ($e16 (bvslt (zero_extend[9] ?e3) ?e7))
(flet ($e17 (= ?e6 (sign_extend[15] ?e3)))
(flet ($e18 (= (zero_extend[8] ?e2) v0))
(flet ($e19 (bvsgt ?e2 (sign_extend[1] ?e3)))
(flet ($e20 (bvslt ?e3 ?e4))
(flet ($e21 (bvslt ?e6 (zero_extend[15] ?e4)))
(flet ($e22 (distinct (zero_extend[9] ?e4) v0))
(flet ($e23 (bvuge ?e1 (sign_extend[15] ?e5)))
(flet ($e24 (or $e12 $e19))
(flet ($e25 (implies $e16 $e8))
(flet ($e26 (and $e14 $e20))
(flet ($e27 (not $e13))
(flet ($e28 (not $e22))
(flet ($e29 (xor $e11 $e23))
(flet ($e30 (or $e29 $e15))
(flet ($e31 (not $e26))
(flet ($e32 (iff $e31 $e18))
(flet ($e33 (and $e27 $e17))
(flet ($e34 (xor $e21 $e10))
(flet ($e35 (xor $e32 $e33))
(flet ($e36 (and $e30 $e30))
(flet ($e37 (xor $e9 $e9))
(flet ($e38 (xor $e36 $e34))
(flet ($e39 (or $e24 $e25))
(flet ($e40 (iff $e38 $e28))
(flet ($e41 (iff $e40 $e35))
(flet ($e42 (not $e37))
(flet ($e43 (and $e42 $e42))
(flet ($e44 (iff $e43 $e41))
(flet ($e45 (iff $e39 $e44))
(flet ($e46 (and $e45 (not (= v0 bv0[10]))))
(flet ($e47 (and $e46 (not (= v0 (bvnot bv0[10])))))
(flet ($e48 (and $e47 (not (= ?e1 bv0[16]))))
(flet ($e49 (and $e48 (not (= ?e1 (bvnot bv0[16])))))
$e49
))))))))))))))))))))))))))))))))))))))))))))))))))