From 1d9d1933a32df3a0b1deeef5adab019fad4f74d0 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 6 Oct 2014 14:27:46 -0400
Subject: [PATCH] Extended parsing testcase, with constant arrays and RESET.

---
 .../regress0/arrays/parsing_ringer.cvc        | 35 +++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc
index c9f8c9e22..2c2018ecd 100644
--- 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;
-- 
2.30.2