(benchmark fuzzsmt
:logic QF_UFLIA
:status sat
:extrafuns ((f0 Int Int Int))
:extrapreds ((p0 Int Int))
:extrafuns ((v0 Int))
:extrafuns ((v1 Int))
:extrafuns ((v2 Int))
:formula
(let (?e3 6)
(let (?e4 (f0 v2 v2))
(let (?e5 (* ?e3 v0))
(let (?e6 (+ v1 v0))
(let (?e7 (* v0 ?e3))
(let (?e8 (* ?e6 (~ ?e3)))
(let (?e9 (* v1 (~ ?e3)))
(let (?e10 (ite (p0 ?e8 v2) 1 0))
(flet ($e11 (>= ?e7 v2))
(flet ($e12 (p0 v0 ?e4))
(flet ($e13 (distinct v2 ?e7))
(flet ($e14 (> ?e9 ?e6))
(flet ($e15 (>= ?e9 ?e9))
(flet ($e16 (< v1 ?e8))
(flet ($e17 (p0 v1 ?e5))
(flet ($e18 (> ?e9 v0))
(flet ($e19 (>= ?e5 ?e7))
(flet ($e20 (= v1 ?e8))
(flet ($e21 (p0 ?e5 v0))
(flet ($e22 (= ?e10 ?e5))
(let (?e23 (ite $e19 ?e5 v1))
(let (?e24 (ite $e22 v2 ?e10))
(let (?e25 (ite $e15 ?e10 ?e24))
(let (?e26 (ite $e20 ?e4 ?e23))
(let (?e27 (ite $e16 ?e10 v2))
(let (?e28 (ite $e17 ?e23 ?e26))
(let (?e29 (ite $e22 ?e25 ?e26))
(let (?e30 (ite $e18 ?e10 ?e23))
(let (?e31 (ite $e11 ?e7 ?e26))
(let (?e32 (ite $e14 ?e9 ?e27))
(let (?e33 (ite $e12 ?e8 ?e9))
(let (?e34 (ite $e13 ?e24 v0))
(let (?e35 (ite $e21 ?e6 ?e30))
(flet ($e36 (distinct ?e4 ?e30))
(flet ($e37 (= ?e8 ?e29))
(flet ($e38 (p0 ?e6 ?e8))
(flet ($e39 (p0 ?e7 v0))
(flet ($e40 (distinct ?e32 ?e5))
(flet ($e41 (distinct v2 ?e24))
(flet ($e42 (= v1 ?e29))
(flet ($e43 (distinct ?e26 ?e26))
(flet ($e44 (= ?e9 ?e4))
(flet ($e45 (p0 ?e8 v1))
(flet ($e46 (= v0 ?e33))
(flet ($e47 (p0 v0 ?e26))
(flet ($e48 (distinct ?e32 ?e24))
(flet ($e49 (= ?e33 ?e29))
(flet ($e50 (= ?e10 ?e25))
(flet ($e51 (= v0 ?e30))
(flet ($e52 (= ?e25 ?e23))
(flet ($e53 (>= ?e27 ?e31))
(flet ($e54 (distinct ?e25 ?e25))
(flet ($e55 (p0 ?e28 ?e30))
(flet ($e56 (> ?e29 ?e8))
(flet ($e57 (p0 ?e8 ?e35))
(flet ($e58 (distinct ?e7 v1))
(flet ($e59 (distinct ?e7 v1))
(flet ($e60 (> ?e9 ?e25))
(flet ($e61 (< ?e33 ?e31))
(flet ($e62 (< ?e4 ?e6))
(flet ($e63 (< ?e35 ?e27))
(flet ($e64 (<= ?e28 ?e23))
(flet ($e65 (<= ?e8 ?e26))
(flet ($e66 (<= ?e28 ?e29))
(flet ($e67 (p0 ?e9 ?e29))
(flet ($e68 (p0 ?e4 ?e24))
(flet ($e69 (< ?e24 ?e25))
(flet ($e70 (= ?e31 ?e7))
(flet ($e71 (p0 ?e31 ?e10))
(flet ($e72 (>= ?e28 ?e24))
(flet ($e73 (< ?e34 ?e31))
(flet ($e74 (implies $e53 $e22))
(flet ($e75 (iff $e41 $e55))
(flet ($e76 (if_then_else $e40 $e20 $e51))
(flet ($e77 (xor $e75 $e12))
(flet ($e78 (not $e39))
(flet ($e79 (iff $e69 $e70))
(flet ($e80 (or $e21 $e17))
(flet ($e81 (not $e11))
(flet ($e82 (if_then_else $e77 $e56 $e79))
(flet ($e83 (implies $e64 $e38))
(flet ($e84 (xor $e13 $e74))
(flet ($e85 (implies $e67 $e68))
(flet ($e86 (not $e66))
(flet ($e87 (xor $e19 $e85))
(flet ($e88 (not $e49))
(flet ($e89 (iff $e72 $e15))
(flet ($e90 (not $e16))
(flet ($e91 (and $e48 $e63))
(flet ($e92 (iff $e65 $e89))
(flet ($e93 (xor $e81 $e91))
(flet ($e94 (implies $e73 $e60))
(flet ($e95 (iff $e45 $e44))
(flet ($e96 (xor $e52 $e84))
(flet ($e97 (not $e43))
(flet ($e98 (if_then_else $e42 $e96 $e86))
(flet ($e99 (or $e82 $e57))
(flet ($e100 (iff $e92 $e47))
(flet ($e101 (if_then_else $e83 $e83 $e14))
(flet ($e102 (xor $e95 $e99))
(flet ($e103 (xor $e58 $e50))
(flet ($e104 (implies $e36 $e88))
(flet ($e105 (implies $e18 $e71))
(flet ($e106 (if_then_else $e59 $e37 $e78))
(flet ($e107 (xor $e106 $e93))
(flet ($e108 (iff $e80 $e105))
(flet ($e109 (not $e100))
(flet ($e110 (and $e107 $e54))
(flet ($e111 (if_then_else $e61 $e61 $e76))
(flet ($e112 (if_then_else $e98 $e108 $e108))
(flet ($e113 (iff $e112 $e104))
(flet ($e114 (if_then_else $e46 $e46 $e110))
(flet ($e115 (not $e90))
(flet ($e116 (iff $e62 $e114))
(flet ($e117 (if_then_else $e97 $e115 $e97))
(flet ($e118 (iff $e117 $e101))
(flet ($e119 (and $e109 $e109))
(flet ($e120 (and $e111 $e111))
(flet ($e121 (xor $e119 $e94))
(flet ($e122 (xor $e118 $e102))
(flet ($e123 (implies $e87 $e120))
(flet ($e124 (xor $e103 $e123))
(flet ($e125 (implies $e121 $e121))
(flet ($e126 (or $e113 $e113))
(flet ($e127 (not $e126))
(flet ($e128 (if_then_else $e125 $e116 $e127))
(flet ($e129 (iff $e122 $e128))
(flet ($e130 (or $e124 $e124))
(flet ($e131 (or $e130 $e130))
(flet ($e132 (implies $e129 $e129))
(flet ($e133 (or $e131 $e131))
(flet ($e134 (not $e133))
(flet ($e135 (implies $e132 $e134))
$e135
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))