4 files changed, 0 insertions, 125 deletions
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 17cfa3fd4..bdc7352f5 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -44,11 +44,8 @@ TESTS =	\
 	bug272.minimized.smt \
 	constarr.smt2 \
 	constarr2.smt2 \
-	constarr3.smt2 \
 	constarr.cvc \
 	constarr2.cvc \
-	constarr3.cvc \
-	parsing_ringer.cvc \
 	bug637.delta.smt2 \
 	bool-array.smt2
 
diff --git a/test/regress/regress0/arrays/constarr3.cvc b/test/regress/regress0/arrays/constarr3.cvc
deleted file mode 100644
index bf5cf961c..000000000
--- a/test/regress/regress0/arrays/constarr3.cvc
+++ /dev/null
@@ -1,12 +0,0 @@
-% EXIT: 1
-% EXPECT: Array theory solver does not yet support write-chains connecting two different constant arrays
-% should be unsat
-all1, all2 : ARRAY INT OF INT;
-aa, bb : ARRAY INT OF INT;
-a, i : INT;
-ASSERT all1 = ARRAY(INT OF INT) : 1;
-ASSERT aa = all1 WITH [i] := 0;
-ASSERT all2 = ARRAY(INT OF INT) : 2;
-ASSERT bb = all2 WITH [i] := 0;
-ASSERT aa = bb;
-CHECKSAT;
diff --git a/test/regress/regress0/arrays/constarr3.smt2 b/test/regress/regress0/arrays/constarr3.smt2
deleted file mode 100644
index d514fff70..000000000
--- a/test/regress/regress0/arrays/constarr3.smt2
+++ /dev/null
@@ -1,16 +0,0 @@
-; EXIT: 1
-; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays")
-(set-logic QF_ALIA)
-(set-info :status unsat)
-(declare-const all1 (Array Int Int))
-(declare-const all2 (Array Int Int))
-(declare-const aa (Array Int Int))
-(declare-const bb (Array Int Int))
-(declare-const a Int)
-(declare-const i Int)
-(assert (= all1 ((as const (Array Int Int)) 1)))
-(assert (= aa (store all1 i 0)))
-(assert (= all2 ((as const (Array Int Int)) 2)))
-(assert (= bb (store all2 i 0)))
-(assert (= aa bb))
-(check-sat)
diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc
deleted file mode 100644
index 2c2018ecd..000000000
--- a/test/regress/regress0/arrays/parsing_ringer.cvc
+++ /dev/null
@@ -1,94 +0,0 @@
-% Test for presentiation language parsing, some edge cases with cascading
-% store terms.  Intended to put this part of the parser "through the ringer,"
-% hence the name.
-
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: sat
-% EXPECT: sat
-% EXPECT: sat
-% EXPECT: sat
-% EXPECT: sat
-% EXPECT: sat
-% EXPECT: sat
-% EXPECT: unsat
-% EXPECT: unsat
-% EXPECT: sat
-
-PUSH;
-
-x, y : ARRAY INT OF ARRAY INT OF ARRAY INT OF INT;
-
-% multidimensional arrays
-ASSERT x[0][0][0] = 0; %% select
-ASSERT y = x WITH [0][0][1] := 1; %% partial store
-
-CHECKSAT;
-
-% mixed stores: records of arrays of tuples, oh my
-z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #];
-
-arr1 : ARRAY INT OF [# x:INT #];
-arr2 : [ ARRAY INT OF INT, ARRAY INT OF INT ];
-
-ASSERT arr1[0].x = 0;
-ASSERT arr2.0[0] = 1;
-ASSERT arr2.1[0] = 5;
-
-ASSERT z.y.1[1] /= 1;
-ASSERT (# x:=arr1, y:=arr2 #) = z;
-
-CHECKSAT;
-
-ASSERT z.x[0].x /= z.y.0[5];
-
-CHECKSAT;
-
-ASSERT z.y.0[1] = z.x[5].x;
-
-CHECKSAT;
-
-ASSERT z.y.0[5] = z.x[-2].x;
-
-CHECKSAT;
-
-POP;
-
-a : ARRAY INT OF ARRAY INT OF INT;
-b : ARRAY INT OF INT;
-
-% ambiguity in presentation language, comma needs to bind to innermost WITH
-% causes type error if the [2]:=2 at the end is attached to the wrong WITH
-ASSERT a = a WITH [0]:=b WITH [1]:=1,[2]:=2;
-
-CHECKSAT;
-
-RESET;
-
-% more mixed stores, this time with constant arrays
-z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #];
-
-ASSERT z.y.1[1] /= 1;
-ASSERT (# x:=ARRAY(INT OF [# x:INT #]):(# x:=0 #), y:=(ARRAY(INT OF INT):1, ARRAY(INT OF INT):5) #) = z;
-
-CHECKSAT;
-
-ASSERT z.x[0].x /= z.y.0[5];
-
-CHECKSAT;
-
-ASSERT z.y.0[1] = z.x[5].x;
-
-CHECKSAT;
-
-ASSERT z.y.0[5] = z.x[-2].x;
-
-CHECKSAT;
-
-RESET;
-
-a : ARRAY INT OF INT;
-
-ASSERT a = a WITH [0]:=0, [1]:=1;
-
-CHECKSAT;