Extended parsing testcase, with constant arrays and RESET.

diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc
index c9f8c9e2239f4b8e26f6163bb93aff68b08fa67f..2c2018ecd01cadc35a8e259994b69f0bea20a6d8 100644 (file)
--- a/test/regress/regress0/arrays/parsing_ringer.cvc
+++ b/test/regress/regress0/arrays/parsing_ringer.cvc
@@ -9,6 +9,11 @@
 % EXPECT: sat
 % EXPECT: sat
 % EXPECT: sat
+% EXPECT: sat
+% EXPECT: sat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: sat
 
 PUSH;
 
@@ -57,3 +62,33 @@ b : ARRAY INT OF INT;
 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;