(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 bv2[4])
(let (?e6 bv2[4])
(let (?e7 (bvlshr v4 v3))
(let (?e8 (ite (bvugt ?e5 v1) bv1[1] bv0[1]))
(let (?e9 (bvor v3 v1))
(let (?e10 (bvnot v4))
(let (?e11 (bvsub v0 ?e6))
(let (?e12 (bvnor ?e5 (zero_extend[3] ?e8)))
(let (?e13 (bvmul ?e12 v1))
(let (?e14 (ite (= ?e10 v3) bv1[1] bv0[1]))
(let (?e15 (ite (bvult v0 ?e11) bv1[1] bv0[1]))
(let (?e16 (bvashr ?e9 ?e5))
(let (?e17 (bvnor v1 ?e11))
(let (?e18 (bvcomp ?e17 ?e11))
(let (?e19 (zero_extend[0] ?e13))
(let (?e20 (bvsub v3 ?e19))
(let (?e21 (bvshl v4 ?e10))
(let (?e22 (ite (bvule ?e10 (sign_extend[3] ?e14)) bv1[1] bv0[1]))
(let (?e23 (concat ?e15 ?e15))
(let (?e24 (rotate_left[0] v1))
(let (?e25 (bvshl ?e21 v1))
(let (?e26 (bvnor ?e24 ?e7))
(let (?e27 (bvand ?e11 v0))
(let (?e28 (bvlshr ?e20 (zero_extend[3] ?e8)))
(let (?e29 (bvcomp ?e10 v2))
(flet ($e30 (bvuge (zero_extend[3] ?e14) v2))
(flet ($e31 (bvult ?e17 ?e12))
(flet ($e32 (distinct ?e16 ?e17))
(flet ($e33 (bvuge (zero_extend[3] ?e18) ?e21))
(flet ($e34 (= ?e20 ?e19))
(flet ($e35 (bvuge ?e27 (sign_extend[3] ?e18)))
(flet ($e36 (bvult ?e10 ?e27))
(flet ($e37 (bvugt v3 v1))
(flet ($e38 (bvuge ?e24 ?e17))
(flet ($e39 (bvult v1 (sign_extend[2] ?e23)))
(flet ($e40 (bvsle (sign_extend[3] ?e22) ?e5))
(flet ($e41 (bvult ?e25 ?e5))
(flet ($e42 (distinct ?e10 ?e16))
(flet ($e43 (bvugt ?e24 (sign_extend[3] ?e22)))
(flet ($e44 (bvuge (zero_extend[3] ?e8) ?e20))
(flet ($e45 (bvsgt ?e6 ?e11))
(flet ($e46 (bvslt v1 ?e26))
(flet ($e47 (bvsgt v1 ?e16))
(flet ($e48 (bvsgt ?e7 v3))
(flet ($e49 (bvugt ?e16 ?e12))
(flet ($e50 (bvule ?e14 ?e22))
(flet ($e51 (bvsgt v3 ?e9))
(flet ($e52 (bvugt ?e24 (zero_extend[3] ?e14)))
(flet ($e53 (= v2 (zero_extend[3] ?e22)))
(flet ($e54 (bvuge ?e5 (sign_extend[3] ?e29)))
(flet ($e55 (bvsgt ?e13 ?e16))
(flet ($e56 (bvsge ?e21 ?e6))
(flet ($e57 (bvuge ?e11 v4))
(flet ($e58 (bvslt ?e6 ?e28))
(flet ($e59 (bvsle (sign_extend[3] ?e29) ?e27))
(flet ($e60 (bvslt ?e20 ?e24))
(flet ($e61 (bvsge (zero_extend[3] ?e14) ?e28))
(flet ($e62 (bvsle ?e20 ?e13))
(flet ($e63 (bvsge ?e25 ?e21))
(flet ($e64 (distinct (sign_extend[3] ?e29) v4))
(flet ($e65 (distinct (zero_extend[3] ?e29) ?e10))
(flet ($e66 (bvsle (zero_extend[2] ?e23) ?e27))
(flet ($e67 (bvsgt ?e17 v3))
(flet ($e68 (bvule v1 (sign_extend[3] ?e18)))
(flet ($e69 (bvule ?e25 ?e7))
(flet ($e70 (bvuge v1 ?e28))
(flet ($e71 (bvugt v2 ?e9))
(flet ($e72 (distinct (zero_extend[3] ?e29) ?e6))
(flet ($e73 (bvslt v1 ?e13))
(flet ($e74 (bvuge (zero_extend[3] ?e14) ?e12))
(flet ($e75 (bvult (zero_extend[3] ?e8) v4))
(flet ($e76 (bvslt v0 ?e19))
(flet ($e77 (bvule ?e29 ?e22))
(flet ($e78 (distinct (sign_extend[3] ?e14) ?e16))
(flet ($e79 (bvule ?e27 ?e20))
(flet ($e80 (bvsgt v0 (zero_extend[2] ?e23)))
(flet ($e81 (bvule ?e21 v2))
(flet ($e82 (bvsge ?e28 v3))
(flet ($e83 (distinct (sign_extend[3] ?e8) ?e13))
(flet ($e84 (bvule (sign_extend[3] ?e15) v2))
(flet ($e85 
(and
 (or $e32 $e81 (not $e60))
 (or (not $e60) $e69 $e50)
 (or (not $e53) (not $e67) $e51)
 (or $e30 $e62 $e78)
 (or $e37 $e65 (not $e81))
 (or $e38 (not $e81) (not $e69))
 (or $e80 (not $e84) $e36)
 (or (not $e46) (not $e63) $e33)
 (or (not $e78) (not $e61) (not $e84))
 (or $e50 (not $e35) (not $e52))
 (or (not $e32) (not $e77) (not $e63))
 (or $e66 $e65 (not $e84))
 (or $e72 (not $e53) $e42)
 (or $e44 (not $e60) $e78)
 (or (not $e61) (not $e34) $e53)
 (or (not $e49) (not $e40) $e79)
 (or $e81 $e42 (not $e44))
 (or $e37 (not $e74) $e51)
 (or (not $e47) (not $e57) $e72)
 (or (not $e34) (not $e52) (not $e62))
 (or $e58 (not $e56) $e72)
 (or $e43 $e34 (not $e62))
 (or (not $e50) (not $e75) (not $e42))
 (or $e61 $e39 (not $e73))
 (or $e34 (not $e50) $e78)
 (or $e46 $e68 (not $e37))
 (or $e79 (not $e78) (not $e31))
))
$e85
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))