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