1 files changed, 0 insertions, 257 deletions
diff --git a/test/regress/regress0/uflra/fuzz01.smt b/test/regress/regress0/uflra/fuzz01.smt
deleted file mode 100644
index 2c6286e3a..000000000
--- a/test/regress/regress0/uflra/fuzz01.smt
+++ /dev/null
@@ -1,257 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_UFLRA
-:status sat
-:extrafuns ((f0 Real Real))
-:extrafuns ((f1 Real Real Real Real))
-:extrapreds ((p0 Real Real Real))
-:extrafuns ((v0 Real))
-:extrafuns ((v1 Real))
-:extrafuns ((v2 Real))
-:formula
-(let (?e3 5)
-(let (?e4 2)
-(let (?e5 0)
-(let (?e6 (f1 v0 v1 v0))
-(let (?e7 (f0 v0))
-(let (?e8 (ite (p0 v1 ?e7 v0) 1 0))
-(let (?e9 (ite (p0 ?e8 v1 v0) 1 0))
-(let (?e10 (- ?e9 ?e9))
-(let (?e11 (~ v1))
-(let (?e12 (ite (p0 v0 ?e8 v2) 1 0))
-(let (?e13 (/ ?e5 ?e4))
-(let (?e14 (/ ?e4 ?e4))
-(let (?e15 (~ v0))
-(let (?e16 (* ?e6 (~ ?e3)))
-(flet ($e17 (< ?e8 ?e8))
-(flet ($e18 (<= v0 v1))
-(flet ($e19 (distinct ?e16 ?e15))
-(flet ($e20 (distinct ?e13 ?e12))
-(flet ($e21 (> ?e11 ?e11))
-(flet ($e22 (= v0 ?e11))
-(flet ($e23 (p0 ?e16 ?e13 ?e11))
-(flet ($e24 (> ?e16 ?e12))
-(flet ($e25 (= ?e13 ?e12))
-(flet ($e26 (<= ?e12 ?e12))
-(flet ($e27 (p0 ?e12 ?e12 ?e14))
-(flet ($e28 (distinct ?e7 ?e12))
-(flet ($e29 (>= ?e9 ?e13))
-(flet ($e30 (< v2 v0))
-(flet ($e31 (> v2 v1))
-(flet ($e32 (p0 ?e9 v1 ?e6))
-(flet ($e33 (= ?e16 v2))
-(flet ($e34 (p0 ?e7 ?e12 ?e14))
-(flet ($e35 (distinct ?e12 ?e15))
-(flet ($e36 (>= ?e9 ?e15))
-(flet ($e37 (< ?e11 ?e10))
-(let (?e38 (ite $e24 ?e9 ?e14))
-(let (?e39 (ite $e24 ?e12 ?e6))
-(let (?e40 (ite $e30 ?e15 ?e11))
-(let (?e41 (ite $e32 v1 v2))
-(let (?e42 (ite $e36 v1 ?e39))
-(let (?e43 (ite $e33 ?e10 ?e15))
-(let (?e44 (ite $e19 ?e8 ?e16))
-(let (?e45 (ite $e26 v0 ?e12))
-(let (?e46 (ite $e36 ?e7 ?e14))
-(let (?e47 (ite $e20 ?e40 ?e14))
-(let (?e48 (ite $e26 ?e15 ?e9))
-(let (?e49 (ite $e22 ?e13 ?e13))
-(let (?e50 (ite $e31 ?e16 ?e47))
-(let (?e51 (ite $e30 ?e41 ?e11))
-(let (?e52 (ite $e17 ?e6 ?e9))
-(let (?e53 (ite $e18 ?e46 v2))
-(let (?e54 (ite $e19 ?e9 ?e9))
-(let (?e55 (ite $e37 ?e51 v2))
-(let (?e56 (ite $e28 ?e14 ?e46))
-(let (?e57 (ite $e29 ?e12 ?e14))
-(let (?e58 (ite $e17 ?e47 ?e7))
-(let (?e59 (ite $e34 ?e46 v2))
-(let (?e60 (ite $e21 ?e55 ?e51))
-(let (?e61 (ite $e24 ?e14 ?e50))
-(let (?e62 (ite $e17 ?e47 ?e61))
-(let (?e63 (ite $e30 ?e45 ?e12))
-(let (?e64 (ite $e35 ?e45 ?e47))
-(let (?e65 (ite $e25 v1 ?e38))
-(let (?e66 (ite $e23 ?e16 ?e59))
-(let (?e67 (ite $e26 ?e61 ?e38))
-(let (?e68 (ite $e27 ?e57 ?e50))
-(flet ($e69 (> v0 ?e12))
-(flet ($e70 (p0 ?e8 ?e66 ?e43))
-(flet ($e71 (<= ?e64 ?e8))
-(flet ($e72 (> ?e49 ?e43))
-(flet ($e73 (>= v0 ?e46))
-(flet ($e74 (<= v1 ?e49))
-(flet ($e75 (< ?e11 ?e38))
-(flet ($e76 (>= v2 ?e10))
-(flet ($e77 (= ?e51 ?e40))
-(flet ($e78 (>= ?e14 ?e50))
-(flet ($e79 (> ?e49 ?e8))
-(flet ($e80 (= ?e47 ?e12))
-(flet ($e81 (> ?e64 ?e54))
-(flet ($e82 (<= ?e48 ?e57))
-(flet ($e83 (> ?e57 ?e54))
-(flet ($e84 (p0 ?e44 ?e39 ?e65))
-(flet ($e85 (< ?e51 ?e11))
-(flet ($e86 (distinct ?e51 ?e53))
-(flet ($e87 (= ?e57 ?e46))
-(flet ($e88 (p0 ?e6 ?e47 ?e41))
-(flet ($e89 (<= ?e58 ?e14))
-(flet ($e90 (>= ?e67 v1))
-(flet ($e91 (<= ?e39 ?e59))
-(flet ($e92 (>= ?e10 v1))
-(flet ($e93 (> ?e10 ?e10))
-(flet ($e94 (<= ?e57 ?e10))
-(flet ($e95 (< ?e47 ?e42))
-(flet ($e96 (>= ?e41 ?e63))
-(flet ($e97 (<= ?e9 ?e14))
-(flet ($e98 (distinct v0 ?e64))
-(flet ($e99 (distinct ?e49 ?e61))
-(flet ($e100 (p0 ?e61 ?e52 v1))
-(flet ($e101 (>= ?e12 ?e6))
-(flet ($e102 (p0 ?e59 ?e57 ?e62))
-(flet ($e103 (distinct ?e66 ?e15))
-(flet ($e104 (<= ?e46 ?e50))
-(flet ($e105 (>= ?e57 ?e46))
-(flet ($e106 (= ?e44 ?e58))
-(flet ($e107 (p0 ?e6 ?e8 ?e40))
-(flet ($e108 (distinct ?e12 ?e58))
-(flet ($e109 (>= ?e56 ?e15))
-(flet ($e110 (< ?e62 ?e44))
-(flet ($e111 (distinct v2 ?e14))
-(flet ($e112 (< ?e44 ?e39))
-(flet ($e113 (= ?e40 ?e11))
-(flet ($e114 (= ?e55 ?e56))
-(flet ($e115 (p0 ?e66 ?e40 ?e62))
-(flet ($e116 (= ?e13 ?e14))
-(flet ($e117 (> ?e59 ?e68))
-(flet ($e118 (p0 ?e45 ?e50 ?e6))
-(flet ($e119 (p0 ?e67 v2 v1))
-(flet ($e120 (= v2 ?e15))
-(flet ($e121 (< ?e42 ?e12))
-(flet ($e122 (distinct ?e52 ?e40))
-(flet ($e123 (= v1 ?e14))
-(flet ($e124 (< ?e13 ?e66))
-(flet ($e125 (= ?e12 ?e61))
-(flet ($e126 (>= ?e66 v0))
-(flet ($e127 (> ?e58 ?e13))
-(flet ($e128 (distinct ?e41 ?e41))
-(flet ($e129 (>= ?e47 ?e16))
-(flet ($e130 (p0 v2 ?e59 ?e62))
-(flet ($e131 (<= ?e12 ?e41))
-(flet ($e132 (> ?e68 ?e51))
-(flet ($e133 (>= ?e59 ?e38))
-(flet ($e134 (< ?e65 ?e13))
-(flet ($e135 (< ?e39 ?e45))
-(flet ($e136 (>= ?e54 ?e16))
-(flet ($e137 (>= ?e62 ?e54))
-(flet ($e138 (p0 ?e59 ?e54 ?e41))
-(flet ($e139 (p0 ?e53 ?e12 ?e45))
-(flet ($e140 (distinct ?e52 ?e14))
-(flet ($e141 (= ?e51 ?e63))
-(flet ($e142 (p0 ?e65 ?e59 ?e64))
-(flet ($e143 (<= ?e52 ?e45))
-(flet ($e144 (p0 ?e49 ?e12 ?e63))
-(flet ($e145 (> ?e39 ?e7))
-(flet ($e146 (>= ?e60 ?e8))
-(flet ($e147 (if_then_else $e78 $e34 $e87))
-(flet ($e148 (iff $e28 $e83))
-(flet ($e149 (or $e19 $e107))
-(flet ($e150 (not $e29))
-(flet ($e151 (or $e25 $e113))
-(flet ($e152 (implies $e82 $e133))
-(flet ($e153 (or $e120 $e30))
-(flet ($e154 (not $e81))
-(flet ($e155 (xor $e26 $e99))
-(flet ($e156 (not $e105))
-(flet ($e157 (xor $e122 $e126))
-(flet ($e158 (implies $e70 $e97))
-(flet ($e159 (iff $e21 $e150))
-(flet ($e160 (iff $e37 $e33))
-(flet ($e161 (if_then_else $e149 $e139 $e129))
-(flet ($e162 (iff $e96 $e18))
-(flet ($e163 (if_then_else $e116 $e36 $e160))
-(flet ($e164 (implies $e125 $e17))
-(flet ($e165 (iff $e74 $e98))
-(flet ($e166 (and $e159 $e110))
-(flet ($e167 (implies $e152 $e31))
-(flet ($e168 (if_then_else $e141 $e86 $e124))
-(flet ($e169 (and $e80 $e118))
-(flet ($e170 (implies $e22 $e154))
-(flet ($e171 (xor $e84 $e153))
-(flet ($e172 (and $e102 $e77))
-(flet ($e173 (and $e164 $e100))
-(flet ($e174 (if_then_else $e134 $e76 $e90))
-(flet ($e175 (and $e157 $e138))
-(flet ($e176 (or $e92 $e158))
-(flet ($e177 (xor $e103 $e130))
-(flet ($e178 (or $e73 $e101))
-(flet ($e179 (if_then_else $e104 $e174 $e27))
-(flet ($e180 (and $e156 $e172))
-(flet ($e181 (implies $e93 $e176))
-(flet ($e182 (xor $e121 $e32))
-(flet ($e183 (and $e148 $e112))
-(flet ($e184 (and $e165 $e165))
-(flet ($e185 (iff $e72 $e162))
-(flet ($e186 (if_then_else $e151 $e23 $e171))
-(flet ($e187 (or $e111 $e94))
-(flet ($e188 (xor $e144 $e177))
-(flet ($e189 (implies $e185 $e188))
-(flet ($e190 (not $e167))
-(flet ($e191 (xor $e115 $e155))
-(flet ($e192 (and $e95 $e179))
-(flet ($e193 (iff $e180 $e182))
-(flet ($e194 (or $e88 $e131))
-(flet ($e195 (iff $e123 $e168))
-(flet ($e196 (xor $e106 $e194))
-(flet ($e197 (iff $e170 $e191))
-(flet ($e198 (iff $e196 $e117))
-(flet ($e199 (and $e71 $e197))
-(flet ($e200 (or $e119 $e108))
-(flet ($e201 (not $e163))
-(flet ($e202 (iff $e183 $e201))
-(flet ($e203 (implies $e178 $e91))
-(flet ($e204 (or $e142 $e175))
-(flet ($e205 (not $e145))
-(flet ($e206 (and $e146 $e132))
-(flet ($e207 (if_then_else $e173 $e147 $e20))
-(flet ($e208 (or $e195 $e166))
-(flet ($e209 (and $e35 $e79))
-(flet ($e210 (if_then_else $e69 $e75 $e184))
-(flet ($e211 (not $e199))
-(flet ($e212 (iff $e204 $e143))
-(flet ($e213 (xor $e161 $e89))
-(flet ($e214 (iff $e114 $e114))
-(flet ($e215 (not $e214))
-(flet ($e216 (xor $e186 $e189))
-(flet ($e217 (implies $e212 $e24))
-(flet ($e218 (xor $e136 $e202))
-(flet ($e219 (not $e213))
-(flet ($e220 (iff $e135 $e198))
-(flet ($e221 (iff $e169 $e128))
-(flet ($e222 (implies $e207 $e187))
-(flet ($e223 (or $e219 $e211))
-(flet ($e224 (and $e223 $e137))
-(flet ($e225 (and $e205 $e109))
-(flet ($e226 (xor $e200 $e220))
-(flet ($e227 (implies $e208 $e226))
-(flet ($e228 (if_then_else $e193 $e222 $e192))
-(flet ($e229 (xor $e227 $e210))
-(flet ($e230 (and $e216 $e217))
-(flet ($e231 (not $e218))
-(flet ($e232 (implies $e225 $e203))
-(flet ($e233 (xor $e221 $e140))
-(flet ($e234 (xor $e224 $e232))
-(flet ($e235 (if_then_else $e233 $e231 $e181))
-(flet ($e236 (if_then_else $e206 $e228 $e215))
-(flet ($e237 (implies $e236 $e85))
-(flet ($e238 (implies $e229 $e235))
-(flet ($e239 (or $e190 $e237))
-(flet ($e240 (or $e234 $e230))
-(flet ($e241 (iff $e238 $e127))
-(flet ($e242 (not $e240))
-(flet ($e243 (iff $e239 $e241))
-(flet ($e244 (if_then_else $e243 $e242 $e243))
-(flet ($e245 (xor $e244 $e244))
-(flet ($e246 (iff $e209 $e245))
-$e246
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-