From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 6 Oct 2014 18:27:46 +0000 (-0400)
Subject: Extended parsing testcase, with constant arrays and RESET.
X-Git-Tag: cvc5-1.0.0~6593
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d9d1933a32df3a0b1deeef5adab019fad4f74d0;p=cvc5.git

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 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;