diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
| commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
| tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress1/Makefile.am | |
| parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) | |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress1/Makefile.am')
| -rw-r--r-- | test/regress/regress1/Makefile.am | 55 |
1 files changed, 49 insertions, 6 deletions
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 9bf23f555..af3f65370 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf nl strings sets sygus sep quantifiers +SUBDIRS = . arith bv aufbv auflia datatypes rewriterules lemmas decision fmf ho nl push-pop quantifiers rels strings sets sygus sep uflia # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) @@ -20,11 +20,54 @@ MAKEFLAGS = -k # 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 = bug425.cvc \ - bug519.smt2 \ - bug521.smt2 - -EXTRA_DIST = $(TESTS) +TESTS = \ + bug425.cvc \ + bug519.smt2 \ + bug521.smt2 \ + bug694-Unapply1.scala-0.smt2 \ + fmf-fun-dbu.smt2 \ + bug296.smt2 \ + bug507.smt2 \ + gensys_brn001.smt2 \ + simplification_bug4.smt2 \ + trim.cvc \ + constarr3.cvc \ + constarr3.smt2 \ + parsing_ringer.cvc \ + arrayinuf_error.smt2 \ + boolean-terms-kernel2.smt2 \ + boolean.cvc \ + bug216.smt2 \ + bug512.smt2 \ + bug516.smt2 \ + bug520.smt2 \ + bug543.smt2 \ + bug567.smt2 \ + bug593.smt2 \ + bug681.smt2 \ + bug800.smt2 \ + bvdiv2.smt2 \ + error.cvc \ + errorcrash.smt2 \ + hole6.cvc \ + ite5.smt2 \ + non-fatal-errors.smt2 \ + proof00.smt2 \ + sqrt2-sort-inf-unk.smt2 \ + test12.cvc \ + uf2.smt2 + +EXTRA_DIST = $(TESTS) \ + simplification_bug4.smt2.expect \ + bug590.smt2.expect \ + bug216.smt2.expect \ + bug590.smt2 \ + bug585.cvc \ + crash_burn_locusts.smt2 \ + bug472.smt2 \ + simple-rdl-definefun.smt2 + +# issue1048-arrays-int-real.smt2 -- different errors on debug and production # synonyms for "check" in this directory .PHONY: regress regress1 test |