(benchmark fuzzsmt
:logic QF_AUFBV
:status sat
:extrafuns ((v0 BitVec[9]))
:extrafuns ((v1 BitVec[14]))
:extrafuns ((a2 Array[2:5]))
:extrafuns ((a3 Array[8:5]))
:formula
(let (?e4 bv712[10])
(let (?e5 (ite (bvslt ?e4 ?e4) bv1[1] bv0[1]))
(let (?e6 (ite (= bv1[1] (extract[2:2] v1)) (sign_extend[5] v0) v1))
(let (?e7 (store a2 (sign_extend[1] ?e5) (extract[12:8] ?e6)))
(let (?e8 (store ?e7 (zero_extend[1] ?e5) (extract[6:2] v1)))
(let (?e9 (select ?e8 (extract[12:11] v1)))
(let (?e10 (select a2 (extract[2:1] ?e4)))
(let (?e11 (store ?e8 (zero_extend[1] ?e5) ?e10))
(let (?e12 (select ?e11 (extract[1:0] ?e10)))
(let (?e13 (select a2 (extract[3:2] ?e9)))
(let (?e14 (ite (bvsge (zero_extend[4] ?e10) v0) bv1[1] bv0[1]))
(let (?e15 (bvnand ?e4 (zero_extend[5] ?e13)))
(let (?e16 (ite (bvule ?e12 ?e12) bv1[1] bv0[1]))
(let (?e17 (extract[0:0] ?e5))
(let (?e18 (zero_extend[0] ?e6))
(let (?e19 (bvsdiv (zero_extend[9] ?e12) v1))
(let (?e20 (bvsdiv (zero_extend[9] ?e9) ?e6))
(flet ($e21 (bvugt v1 (zero_extend[9] ?e12)))
(flet ($e22 (bvuge ?e9 (sign_extend[4] ?e14)))
(flet ($e23 (bvslt ?e6 (sign_extend[9] ?e10)))
(flet ($e24 (bvugt ?e19 v1))
(flet ($e25 (bvult (sign_extend[4] ?e12) v0))
(flet ($e26 (= (sign_extend[4] ?e15) v1))
(flet ($e27 (= ?e19 (sign_extend[9] ?e12)))
(flet ($e28 (bvsge (zero_extend[9] ?e9) ?e6))
(flet ($e29 (bvuge ?e13 (zero_extend[4] ?e5)))
(flet ($e30 (distinct (zero_extend[4] ?e14) ?e9))
(flet ($e31 (bvsle (zero_extend[4] ?e14) ?e12))
(flet ($e32 (bvslt ?e10 ?e12))
(flet ($e33 (distinct ?e6 ?e18))
(flet ($e34 (bvsge (sign_extend[4] ?e12) v0))
(flet ($e35 (bvsge ?e6 (zero_extend[5] v0)))
(flet ($e36 (distinct v0 (sign_extend[4] ?e13)))
(flet ($e37 (= ?e18 (sign_extend[5] v0)))
(flet ($e38 (bvugt ?e16 ?e5))
(flet ($e39 (bvslt ?e9 (sign_extend[4] ?e16)))
(flet ($e40 (distinct (zero_extend[9] ?e13) ?e19))
(flet ($e41 (bvsle ?e19 (zero_extend[13] ?e5)))
(flet ($e42 (bvslt (zero_extend[4] ?e12) v0))
(flet ($e43 (bvugt ?e14 ?e17))
(flet ($e44 (bvsle (sign_extend[4] ?e14) ?e13))
(flet ($e45 (bvugt (zero_extend[4] ?e14) ?e12))
(flet ($e46 (bvsge ?e19 ?e6))
(flet ($e47 (bvsle ?e10 (zero_extend[4] ?e14)))
(flet ($e48 (bvsle ?e20 (zero_extend[4] ?e4)))
(flet ($e49 (and $e22 $e30))
(flet ($e50 (or $e38 $e29))
(flet ($e51 (xor $e41 $e34))
(flet ($e52 (iff $e21 $e48))
(flet ($e53 (iff $e46 $e23))
(flet ($e54 (iff $e33 $e44))
(flet ($e55 (and $e24 $e43))
(flet ($e56 (implies $e32 $e31))
(flet ($e57 (or $e56 $e47))
(flet ($e58 (xor $e50 $e40))
(flet ($e59 (or $e57 $e45))
(flet ($e60 (iff $e42 $e59))
(flet ($e61 (or $e35 $e36))
(flet ($e62 (if_then_else $e51 $e60 $e25))
(flet ($e63 (or $e55 $e54))
(flet ($e64 (xor $e53 $e39))
(flet ($e65 (and $e63 $e63))
(flet ($e66 (or $e61 $e28))
(flet ($e67 (and $e27 $e27))
(flet ($e68 (or $e26 $e26))
(flet ($e69 (or $e65 $e49))
(flet ($e70 (xor $e58 $e62))
(flet ($e71 (implies $e68 $e37))
(flet ($e72 (if_then_else $e52 $e52 $e70))
(flet ($e73 (implies $e66 $e67))
(flet ($e74 (xor $e64 $e71))
(flet ($e75 (and $e73 $e73))
(flet ($e76 (implies $e72 $e69))
(flet ($e77 (xor $e76 $e75))
(flet ($e78 (iff $e77 $e74))
(flet ($e79 (and $e78 (not (= v1 bv0[14]))))
(flet ($e80 (and $e79 (not (= v1 (bvnot bv0[14])))))
(flet ($e81 (and $e80 (not (= ?e6 bv0[14]))))
(flet ($e82 (and $e81 (not (= ?e6 (bvnot bv0[14])))))
$e82
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))