Add some (so far trivial) regressions for constant arrays.

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 345856d856abc95ba0907599c3e5b35b2178eee2..8af912395be92356749748746cbe006e081173ba 100644 (file)
--- 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 (file)
index 0000000..406a1ce
--- /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 (file)
index 0000000..b1fb02b
--- /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 (file)
index 0000000..90ff114
--- /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 (file)
index 0000000..c84e678
--- /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 (file)
index 0000000..bf5cf96
--- /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 (file)
index 0000000..d514fff
--- /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)