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