diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/arrays/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 31 | ||||
-rw-r--r-- | test/regress/regress0/arrays/arrays0.smt2 | 22 | ||||
-rw-r--r-- | test/regress/regress0/arrays/arrays1.smt2 | 21 | ||||
-rw-r--r-- | test/regress/regress0/arrays/arrays2.smt2 | 21 | ||||
-rw-r--r-- | test/regress/regress0/arrays/arrays3.smt2 | 23 | ||||
-rw-r--r-- | test/regress/regress0/arrays/arrays4.smt2 | 23 |
8 files changed, 150 insertions, 1 deletions
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) |