From 6294adeb83155c54539b2d2d31fa9e3a5b6f1a00 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 3 Oct 2014 14:28:30 -0400
Subject: [PATCH] Add some (so far trivial) regressions for constant arrays.

---
 test/regress/regress0/arrays/Makefile.am    |  8 +++++++-
 test/regress/regress0/arrays/constarr.cvc   |  7 +++++++
 test/regress/regress0/arrays/constarr.smt2  |  9 +++++++++
 test/regress/regress0/arrays/constarr2.cvc  |  7 +++++++
 test/regress/regress0/arrays/constarr2.smt2 | 10 ++++++++++
 test/regress/regress0/arrays/constarr3.cvc  | 12 ++++++++++++
 test/regress/regress0/arrays/constarr3.smt2 | 16 ++++++++++++++++
 7 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/arrays/constarr.cvc
 create mode 100644 test/regress/regress0/arrays/constarr.smt2
 create mode 100644 test/regress/regress0/arrays/constarr2.cvc
 create mode 100644 test/regress/regress0/arrays/constarr2.smt2
 create mode 100644 test/regress/regress0/arrays/constarr3.cvc
 create mode 100644 test/regress/regress0/arrays/constarr3.smt2

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 345856d85..8af912395 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -39,7 +39,13 @@ TESTS =	\
 	incorrect11.smt \
 	swap_t1_np_nf_ai_00005_007.cvc.smt \
 	x2.smt \
-	x3.smt
+	x3.smt \
+	constarr.smt2 \
+	constarr2.smt2 \
+	constarr3.smt2 \
+	constarr.cvc \
+	constarr2.cvc \
+	constarr3.cvc
 
 EXTRA_DIST = $(TESTS) \
 	bug272.smt \
diff --git a/test/regress/regress0/arrays/constarr.cvc b/test/regress/regress0/arrays/constarr.cvc
new file mode 100644
index 000000000..406a1ce2b
--- /dev/null
+++ b/test/regress/regress0/arrays/constarr.cvc
@@ -0,0 +1,7 @@
+% EXPECT: unsat
+all1 : ARRAY INT OF INT;
+a, i : INT;
+ASSERT all1 = ARRAY(INT OF INT) : 1;
+ASSERT a = all1[i];
+ASSERT a /= 1;
+CHECKSAT TRUE;
diff --git a/test/regress/regress0/arrays/constarr.smt2 b/test/regress/regress0/arrays/constarr.smt2
new file mode 100644
index 000000000..b1fb02bed
--- /dev/null
+++ b/test/regress/regress0/arrays/constarr.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_ALIA)
+(set-info :status unsat)
+(declare-const all1 (Array Int Int))
+(declare-const a Int)
+(declare-const i Int)
+(assert (= all1 ((as const (Array Int Int)) 1)))
+(assert (= a (select all1 i)))
+(assert (not (= a 1)))
+(check-sat)
diff --git a/test/regress/regress0/arrays/constarr2.cvc b/test/regress/regress0/arrays/constarr2.cvc
new file mode 100644
index 000000000..90ff11430
--- /dev/null
+++ b/test/regress/regress0/arrays/constarr2.cvc
@@ -0,0 +1,7 @@
+% EXPECT: unsat
+all1, all2 : ARRAY INT OF INT;
+a, i : INT;
+ASSERT all1 = ARRAY(INT OF INT) : 1;
+ASSERT all2 = ARRAY(INT OF INT) : 2;
+ASSERT all1 = all2;
+CHECKSAT;
diff --git a/test/regress/regress0/arrays/constarr2.smt2 b/test/regress/regress0/arrays/constarr2.smt2
new file mode 100644
index 000000000..c84e6781a
--- /dev/null
+++ b/test/regress/regress0/arrays/constarr2.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_ALIA)
+(set-info :status unsat)
+(declare-const all1 (Array Int Int))
+(declare-const all2 (Array Int Int))
+(declare-const a Int)
+(declare-const i Int)
+(assert (= all1 ((as const (Array Int Int)) 1)))
+(assert (= all2 ((as const (Array Int Int)) 2)))
+(assert (= all1 all2))
+(check-sat)
diff --git a/test/regress/regress0/arrays/constarr3.cvc b/test/regress/regress0/arrays/constarr3.cvc
new file mode 100644
index 000000000..bf5cf961c
--- /dev/null
+++ b/test/regress/regress0/arrays/constarr3.cvc
@@ -0,0 +1,12 @@
+% 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
new file mode 100644
index 000000000..d514fff70
--- /dev/null
+++ b/test/regress/regress0/arrays/constarr3.smt2
@@ -0,0 +1,16 @@
+; 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)
-- 
2.30.2