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