1 files changed, 0 insertions, 185 deletions
diff --git a/test/regress/regress0/bug239.smt b/test/regress/regress0/bug239.smt
deleted file mode 100644
index b80f56c44..000000000
--- a/test/regress/regress0/bug239.smt
+++ /dev/null
@@ -1,185 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_LRA
-:status sat
-:extrafuns ((v0 Real))
-:extrafuns ((v1 Real))
-:extrafuns ((v2 Real))
-:formula
-(let (?e3 5)
-(let (?e4 0)
-(let (?e5 2)
-(let (?e6 (+ v0 v1))
-(let (?e7 (* v1 ?e3))
-(let (?e8 (~ v0))
-(let (?e9 (- v2 v1))
-(let (?e10 (- v0 ?e9))
-(let (?e11 (* v0 (~ ?e3)))
-(let (?e12 (/ ?e4 (~ ?e3)))
-(let (?e13 (+ ?e8 ?e7))
-(let (?e14 (/ ?e4 (~ ?e5)))
-(flet ($e15 (<= v2 ?e7))
-(flet ($e16 (<= ?e11 ?e11))
-(flet ($e17 (= ?e11 ?e13))
-(flet ($e18 (<= ?e7 ?e14))
-(flet ($e19 (> ?e14 v1))
-(flet ($e20 (< v0 ?e10))
-(flet ($e21 (= ?e8 ?e11))
-(flet ($e22 (>= ?e8 ?e13))
-(flet ($e23 (< ?e10 v2))
-(flet ($e24 (>= ?e10 ?e8))
-(flet ($e25 (= ?e6 ?e7))
-(flet ($e26 (distinct ?e12 ?e11))
-(flet ($e27 (distinct ?e10 ?e9))
-(let (?e28 (ite $e27 ?e13 ?e6))
-(let (?e29 (ite $e21 v2 ?e28))
-(let (?e30 (ite $e26 ?e12 ?e12))
-(let (?e31 (ite $e18 ?e28 v0))
-(let (?e32 (ite $e20 ?e9 ?e10))
-(let (?e33 (ite $e22 ?e11 ?e28))
-(let (?e34 (ite $e17 ?e8 ?e13))
-(let (?e35 (ite $e26 ?e14 v1))
-(let (?e36 (ite $e21 ?e14 ?e30))
-(let (?e37 (ite $e19 ?e7 ?e11))
-(let (?e38 (ite $e25 v1 ?e8))
-(let (?e39 (ite $e22 ?e28 ?e28))
-(let (?e40 (ite $e25 v0 ?e14))
-(let (?e41 (ite $e24 ?e37 v2))
-(let (?e42 (ite $e16 ?e6 v2))
-(let (?e43 (ite $e19 ?e11 ?e7))
-(let (?e44 (ite $e23 ?e36 v2))
-(let (?e45 (ite $e20 v1 ?e7))
-(let (?e46 (ite $e15 ?e45 ?e13))
-(flet ($e47 (= ?e32 ?e9))
-(flet ($e48 (< ?e41 v0))
-(flet ($e49 (distinct ?e14 ?e43))
-(flet ($e50 (distinct ?e8 ?e10))
-(flet ($e51 (> ?e8 ?e37))
-(flet ($e52 (< v1 ?e11))
-(flet ($e53 (< ?e30 ?e8))
-(flet ($e54 (< v2 ?e12))
-(flet ($e55 (>= ?e8 ?e31))
-(flet ($e56 (= ?e12 ?e44))
-(flet ($e57 (= ?e45 v0))
-(flet ($e58 (= ?e36 ?e39))
-(flet ($e59 (= ?e31 v0))
-(flet ($e60 (< ?e9 ?e43))
-(flet ($e61 (distinct ?e14 ?e44))
-(flet ($e62 (= ?e45 ?e29))
-(flet ($e63 (<= ?e12 ?e9))
-(flet ($e64 (>= ?e41 ?e28))
-(flet ($e65 (<= ?e11 v0))
-(flet ($e66 (< ?e29 ?e14))
-(flet ($e67 (< ?e44 v2))
-(flet ($e68 (< ?e40 ?e45))
-(flet ($e69 (> ?e34 ?e7))
-(flet ($e70 (= ?e38 ?e30))
-(flet ($e71 (>= ?e36 ?e31))
-(flet ($e72 (= ?e32 ?e38))
-(flet ($e73 (<= ?e30 ?e42))
-(flet ($e74 (= ?e11 ?e9))
-(flet ($e75 (> ?e40 ?e7))
-(flet ($e76 (distinct ?e39 ?e41))
-(flet ($e77 (< ?e11 ?e28))
-(flet ($e78 (distinct ?e31 ?e45))
-(flet ($e79 (= ?e45 ?e11))
-(flet ($e80 (>= ?e11 ?e42))
-(flet ($e81 (< ?e12 ?e7))
-(flet ($e82 (>= ?e11 ?e41))
-(flet ($e83 (<= ?e8 v0))
-(flet ($e84 (< ?e8 ?e8))
-(flet ($e85 (> ?e30 v2))
-(flet ($e86 (= ?e9 ?e30))
-(flet ($e87 (= ?e33 ?e7))
-(flet ($e88 (<= ?e32 ?e44))
-(flet ($e89 (<= ?e36 ?e33))
-(flet ($e90 (distinct ?e45 ?e45))
-(flet ($e91 (distinct ?e14 ?e44))
-(flet ($e92 (<= v1 ?e12))
-(flet ($e93 (>= v0 ?e12))
-(flet ($e94 (>= ?e46 ?e29))
-(flet ($e95 (> ?e14 ?e6))
-(flet ($e96 (>= v2 ?e14))
-(flet ($e97 (>= ?e39 ?e44))
-(flet ($e98 (>= ?e38 ?e28))
-(flet ($e99 (> v2 ?e9))
-(flet ($e100 (<= ?e42 ?e33))
-(flet ($e101 (= ?e30 ?e29))
-(flet ($e102 (= ?e9 v0))
-(flet ($e103 (distinct ?e37 ?e40))
-(flet ($e104 (= ?e43 ?e14))
-(flet ($e105 (<= ?e35 ?e13))
-(flet ($e106 (and $e102 $e70))
-(flet ($e107 (implies $e84 $e84))
-(flet ($e108 (implies $e69 $e60))
-(flet ($e109 (iff $e105 $e99))
-(flet ($e110 (iff $e100 $e80))
-(flet ($e111 (or $e52 $e86))
-(flet ($e112 (xor $e26 $e18))
-(flet ($e113 (or $e20 $e107))
-(flet ($e114 (not $e94))
-(flet ($e115 (or $e79 $e104))
-(flet ($e116 (not $e76))
-(flet ($e117 (if_then_else $e112 $e22 $e90))
-(flet ($e118 (xor $e77 $e57))
-(flet ($e119 (xor $e88 $e55))
-(flet ($e120 (and $e92 $e68))
-(flet ($e121 (or $e82 $e25))
-(flet ($e122 (implies $e19 $e119))
-(flet ($e123 (implies $e66 $e117))
-(flet ($e124 (if_then_else $e15 $e73 $e65))
-(flet ($e125 (iff $e64 $e103))
-(flet ($e126 (iff $e121 $e122))
-(flet ($e127 (if_then_else $e50 $e47 $e101))
-(flet ($e128 (iff $e81 $e127))
-(flet ($e129 (implies $e124 $e21))
-(flet ($e130 (iff $e87 $e129))
-(flet ($e131 (iff $e116 $e51))
-(flet ($e132 (implies $e72 $e97))
-(flet ($e133 (and $e56 $e98))
-(flet ($e134 (implies $e91 $e53))
-(flet ($e135 (xor $e133 $e114))
-(flet ($e136 (xor $e17 $e110))
-(flet ($e137 (iff $e96 $e128))
-(flet ($e138 (or $e125 $e59))
-(flet ($e139 (or $e23 $e48))
-(flet ($e140 (iff $e62 $e95))
-(flet ($e141 (not $e61))
-(flet ($e142 (and $e132 $e63))
-(flet ($e143 (xor $e109 $e131))
-(flet ($e144 (iff $e54 $e126))
-(flet ($e145 (xor $e74 $e67))
-(flet ($e146 (if_then_else $e89 $e93 $e140))
-(flet ($e147 (iff $e71 $e138))
-(flet ($e148 (and $e143 $e146))
-(flet ($e149 (xor $e147 $e142))
-(flet ($e150 (implies $e85 $e58))
-(flet ($e151 (or $e24 $e78))
-(flet ($e152 (if_then_else $e137 $e113 $e123))
-(flet ($e153 (and $e145 $e16))
-(flet ($e154 (not $e150))
-(flet ($e155 (implies $e151 $e154))
-(flet ($e156 (if_then_else $e118 $e136 $e75))
-(flet ($e157 (and $e108 $e108))
-(flet ($e158 (or $e83 $e141))
-(flet ($e159 (iff $e155 $e149))
-(flet ($e160 (iff $e158 $e156))
-(flet ($e161 (or $e115 $e130))
-(flet ($e162 (or $e157 $e160))
-(flet ($e163 (if_then_else $e152 $e153 $e139))
-(flet ($e164 (not $e144))
-(flet ($e165 (not $e27))
-(flet ($e166 (or $e148 $e162))
-(flet ($e167 (iff $e134 $e166))
-(flet ($e168 (or $e111 $e159))
-(flet ($e169 (or $e106 $e164))
-(flet ($e170 (xor $e161 $e120))
-(flet ($e171 (and $e168 $e165))
-(flet ($e172 (or $e170 $e135))
-(flet ($e173 (or $e169 $e163))
-(flet ($e174 (implies $e49 $e172))
-(flet ($e175 (xor $e174 $e173))
-(flet ($e176 (and $e171 $e175))
-(flet ($e177 (implies $e167 $e176))
-$e177
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-