diff options
Diffstat (limited to 'test')
34 files changed, 107 insertions, 91 deletions
diff --git a/test/Makefile.am b/test/Makefile.am index a71cbfe60..b2df85e97 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -2,8 +2,8 @@ SUBDIRS = unit system regress . MAKEFLAGS = -k -.PHONY: units systemtests regress regress0 regress1 regress2 regress3 -units systemtests regress regress0 regress1 regress2 regress3: +.PHONY: units systemtests regress regress0 regress1 regress2 regress3 regress4 +units systemtests regress regress0 regress1 regress2 regress3 regress4: @$(MAKE) check-pre; \ for dir in $(SUBDIRS); do \ test $$dir = . || (cd $$dir && $(MAKE) $(AM_MAKEFLAGS) $@); \ @@ -29,42 +29,55 @@ test "X$(AM_COLOR_TESTS)" != Xno \ } subdirs_to_check = \ - unit \ - system \ regress/regress0 \ regress/regress0/arith \ regress/regress0/arith/integers \ - regress/regress0/uf \ - regress/regress0/uflra \ - regress/regress0/uflia \ - regress/regress0/bv \ - regress/regress0/bv/core \ regress/regress0/arrays \ regress/regress0/aufbv \ regress/regress0/auflia \ + regress/regress0/bv \ + regress/regress0/bv/core \ regress/regress0/datatypes \ - regress/regress0/quantifiers \ - regress/regress0/rewriterules \ + regress/regress0/decision \ + regress/regress0/fmf \ regress/regress0/lemmas \ + regress/regress0/parser \ + regress/regress0/precedence \ + regress/regress0/preprocess \ regress/regress0/push-pop \ regress/regress0/push-pop/arith \ regress/regress0/push-pop/boolean \ - regress/regress0/precedence \ - regress/regress0/preprocess \ - regress/regress0/tptp \ - regress/regress0/unconstrained \ - regress/regress0/decision \ - regress/regress0/fmf \ - regress/regress0/strings \ - regress/regress0/sets \ + regress/regress0/quantifiers \ regress/regress0/rels \ - regress/regress0/parser \ - regress/regress0/sygus \ + regress/regress0/rewriterules \ regress/regress0/sep \ + regress/regress0/sets \ + regress/regress0/strings \ + regress/regress0/sygus \ + regress/regress0/tptp \ + regress/regress0/uf \ + regress/regress0/uflia \ + regress/regress0/uflra \ + regress/regress0/unconstrained \ regress/regress1 \ - regress/regress1/arith \ + regress/regress1/aufbv \ + regress/regress1/auflia \ + regress/regress1/bv \ + regress/regress1/datatypes \ + regress/regress1/decision \ + regress/regress1/fmf \ + regress/regress1/lemmas \ + regress/regress1/rewriterules \ + regress/regress1/sep \ + regress/regress1/sets \ + regress/regress1/strings \ + regress/regress1/sygus \ regress/regress2 \ - regress/regress3 + regress/regress2/arith \ + regress/regress3 \ + regress/regress4 \ + system \ + unit check-recursive: check-pre .PHONY: check-pre diff --git a/test/regress/Makefile.levels b/test/regress/Makefile.levels index f86bd4a6f..ecfb0c2e5 100644 --- a/test/regress/Makefile.levels +++ b/test/regress/Makefile.levels @@ -9,3 +9,6 @@ endif ifeq ($(REGRESSION_LEVEL),3) SUBDIRS += regress1 regress2 regress3 endif +ifeq ($(REGRESSION_LEVEL),4) +SUBDIRS += regress1 regress2 regress3 regress4 +endif diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index ec09c9a4a..a65a61dc7 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -206,5 +206,5 @@ EXTRA_DIST += $(DISABLED_TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 2fd1925f1..8a7b19461 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -75,5 +75,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index 3b6a86bc0..aa24e9c35 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -145,5 +145,5 @@ FAILING_TESTS = \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index a90b238e2..19aab3e55 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -67,5 +67,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index d88128e72..e23368e3a 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -75,5 +75,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index 82ea731d4..8ce7ae134 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -48,5 +48,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 2aeb7a220..b3c7250ff 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -125,5 +125,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 0e3133b32..ce65bcaf6 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -92,5 +92,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index c177129b4..8631a4f32 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -94,5 +94,5 @@ EXTRA_DIST += \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 6aea21f3f..ccf86e8b4 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -73,5 +73,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index c10b3c668..cea0d7686 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -77,5 +77,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am index 26610304a..89f9d83a3 100644 --- a/test/regress/regress0/lemmas/Makefile.am +++ b/test/regress/regress0/lemmas/Makefile.am @@ -37,5 +37,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am index 44318d492..ab9167943 100644 --- a/test/regress/regress0/parser/Makefile.am +++ b/test/regress/regress0/parser/Makefile.am @@ -41,5 +41,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 1afcc0293..096237106 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -21,8 +21,8 @@ MAKEFLAGS = -k TESTS = \ and-xor.cvc \ and-not.cvc \ - bool-cmp.cvc \ - cmp-plus.cvc \ + bool-cmp.cvc \ + cmp-plus.cvc \ eq-fun.cvc \ iff-assoc.cvc \ iff-implies.cvc \ @@ -31,7 +31,7 @@ TESTS = \ implies-or.cvc \ not-and.cvc \ not-eq.cvc \ - plus-mult.cvc \ + plus-mult.cvc \ or-implies.cvc \ or-xor.cvc \ xor-or.cvc \ @@ -55,5 +55,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am index d83df4192..8ec5e35f6 100644 --- a/test/regress/regress0/preprocess/Makefile.am +++ b/test/regress/regress0/preprocess/Makefile.am @@ -58,5 +58,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 4bc16ea25..8f1126ef5 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -58,5 +58,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/push-pop/arith/Makefile.am b/test/regress/regress0/push-pop/arith/Makefile.am index 7838e202d..e692c86b2 100644 --- a/test/regress/regress0/push-pop/arith/Makefile.am +++ b/test/regress/regress0/push-pop/arith/Makefile.am @@ -58,5 +58,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/push-pop/boolean/Makefile.am b/test/regress/regress0/push-pop/boolean/Makefile.am index 995312cee..a1eb4fd31 100644 --- a/test/regress/regress0/push-pop/boolean/Makefile.am +++ b/test/regress/regress0/push-pop/boolean/Makefile.am @@ -92,5 +92,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 43c77973f..faa2abe9a 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -123,5 +123,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am index 6b8fdfec7..50f979fbd 100644 --- a/test/regress/regress0/rels/Makefile.am +++ b/test/regress/regress0/rels/Makefile.am @@ -111,5 +111,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 3224563ab..fcaa9dc2b 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -49,5 +49,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 2d35aef51..f731bd15e 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -75,5 +75,5 @@ EXTRA_DIST += regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 9c970c45a..f68b9b036 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -83,5 +83,5 @@ EXTRA_DIST += \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 88f3763e1..21d51199d 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -100,5 +100,5 @@ EXTRA_DIST += regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 695c52cc6..0764b5d77 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -26,7 +26,7 @@ TESTS = commutative.sy \ array_sum_2_5.sy \ parity-AIG-d0.sy \ twolets1.sy \ - array_search_2.sy \ + array_search_2.sy \ hd-01-d1-prog.sy \ icfp_28_10.sy \ const-var-test.sy \ @@ -74,5 +74,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index e9274d2ee..a6444c3cb 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -81,5 +81,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index c9a47c26f..91b276889 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -70,5 +70,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 2946d886a..db67df18e 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -74,5 +74,5 @@ EXTRA_DIST = $(TESTS) \ regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index cd39284b8..09c012ffa 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -61,5 +61,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index f79f68c76..b21227253 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -91,5 +91,5 @@ EXTRA_DIST = $(TESTS) regress regress0 test: check # do nothing in this subdir -.PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 6d278409e..55a6c2b09 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -115,5 +115,5 @@ export VERBOSE = 1 test systemtests: check # no-ops here -.PHONY: units regress regress0 regress1 regress2 regress3 -units regress regress0 regress1 regress2 regress3: +.PHONY: units regress regress0 regress1 regress2 regress3 regress4 +units regress regress0 regress1 regress2 regress3 regress4: diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 9d934a6e0..129d086df 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -209,8 +209,8 @@ endif units test: check # no-ops here -.PHONY: systemtests regress regress0 regress1 regress2 regress3 -regress regress0 regress1 regress2 regress3: +.PHONY: systemtests regress regress0 regress1 regress2 regress3 regress4 +regress regress0 regress1 regress2 regress3 regress4: if HAVE_CXXTESTGEN # all is fine with the world |