Merge from arrays2 branch.

9 files changed, 151 insertions, 2 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index aceef1b68..354b81470 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   blu=''; \
   std=''; \
 }
-subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/arrays regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
 check-recursive: check-pre
 .PHONY: check-pre
 check-pre:
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 319601121..89df462e5 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra bv datatypes lemmas push-pop
+SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/arrays/Makefile b/test/regress/regress0/arrays/Makefile
new file mode 100644
index 000000000..1f480a4ad
--- /dev/null
+++ b/test/regress/regress0/arrays/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/arrays
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
new file mode 100644
index 000000000..8fdeda04a
--- /dev/null
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -0,0 +1,31 @@
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	arrays0.smt2 \
+	arrays1.smt2 \
+	arrays2.smt2 \
+	arrays3.smt2 \
+	arrays4.smt2
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/arrays/arrays0.smt2 b/test/regress/regress0/arrays/arrays0.smt2
new file mode 100644
index 000000000..652ff0bcb
--- /dev/null
+++ b/test/regress/regress0/arrays/arrays0.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_AX)
+(set-info :source |
+Benchmarks used in the followin paper:
+Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
+Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
+PDPAR'05
+http://www.ai.dist.unige.it/pdpar05/
+
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort Index 0)
+(declare-sort Element 0)
+(declare-fun a1 () (Array Index Element))
+(declare-fun a2 () (Array Index Element))
+(declare-fun i1 () Index)
+(assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1))))
+(assert (not (= a1 a2)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/arrays/arrays1.smt2 b/test/regress/regress0/arrays/arrays1.smt2
new file mode 100644
index 000000000..f001cc33e
--- /dev/null
+++ b/test/regress/regress0/arrays/arrays1.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AX)
+(set-info :source |
+Benchmarks used in the followin paper:
+Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
+Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
+PDPAR'05
+http://www.ai.dist.unige.it/pdpar05/
+
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort Index 0)
+(declare-sort Element 0)
+(declare-fun a1 () (Array Index Element))
+(declare-fun i0 () Index)
+(declare-fun i1 () Index)
+(assert (let ((?v_0 (select a1 i1))) (let ((?v_1 (store (store a1 i1 ?v_0) i1 ?v_0))) (let ((?v_2 (select ?v_1 i0))) (let ((?v_3 (store (store ?v_1 i0 ?v_2) i0 ?v_2))) (not (= ?v_3 ?v_3)))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/arrays/arrays2.smt2 b/test/regress/regress0/arrays/arrays2.smt2
new file mode 100644
index 000000000..7c14477e2
--- /dev/null
+++ b/test/regress/regress0/arrays/arrays2.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AX)
+(set-info :source |
+Benchmarks used in the followin paper:
+Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
+Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
+PDPAR'05
+http://www.ai.dist.unige.it/pdpar05/
+
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-sort Index 0)
+(declare-sort Element 0)
+(declare-fun a1 () (Array Index Element))
+(declare-fun i0 () Index)
+(declare-fun i1 () Index)
+(assert (let ((?v_0 (select a1 i1))) (let ((?v_1 (store (store a1 i1 ?v_0) i1 ?v_0))) (let ((?v_2 (select ?v_1 i0))) (not (= (store (store ?v_1 i0 (select ?v_1 i1)) i1 ?v_2) (store (store ?v_1 i0 ?v_2) i0 ?v_2)))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/arrays/arrays3.smt2 b/test/regress/regress0/arrays/arrays3.smt2
new file mode 100644
index 000000000..a21397b1d
--- /dev/null
+++ b/test/regress/regress0/arrays/arrays3.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_AX)
+(set-info :source |
+Benchmarks used in the followin paper:
+Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
+Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
+PDPAR'05
+http://www.ai.dist.unige.it/pdpar05/
+
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-sort Index 0)
+(declare-sort Element 0)
+(declare-fun a1 () (Array Index Element))
+(declare-fun a2 () (Array Index Element))
+(declare-fun i1 () Index)
+(declare-fun i2 () Index)
+(assert (let ((?v_0 (store a2 i1 (select a1 i1))) (?v_1 (store a1 i1 (select a2 i1)))) (= (store ?v_1 i1 (select ?v_0 i2)) (store ?v_0 i2 (select ?v_1 i2)))))
+(assert (not (= a1 a2)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/arrays/arrays4.smt2 b/test/regress/regress0/arrays/arrays4.smt2
new file mode 100644
index 000000000..f4afded65
--- /dev/null
+++ b/test/regress/regress0/arrays/arrays4.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_AX)
+(set-info :source |
+Benchmarks used in the followin paper:
+Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
+Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
+PDPAR'05
+http://www.ai.dist.unige.it/pdpar05/
+
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort Index 0)
+(declare-sort Element 0)
+(declare-fun a1 () (Array Index Element))
+(declare-fun a2 () (Array Index Element))
+(declare-fun i1 () Index)
+(declare-fun i2 () Index)
+(assert (let ((?v_0 (store a2 i1 (select a1 i1))) (?v_1 (store a1 i1 (select a2 i1)))) (= (store ?v_1 i2 (select ?v_0 i2)) (store ?v_0 i2 (select ?v_1 i2)))))
+(assert (not (= a1 a2)))
+(check-sat)
+(exit)