diff options
Diffstat (limited to 'test/regress/regress0/uflia/Makefile.am')
| -rw-r--r-- | test/regress/regress0/uflia/Makefile.am | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 21479bac5..e9516d383 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -25,11 +25,25 @@ SMT_TESTS = \ error30.smt # Regression tests for SMT2 inputs -SMT2_TESTS = +SMT2_TESTS = \ + check01.smt2 \ + check02.smt2 \ + check03.smt2 \ + check04.smt2 \ + DRAGON_11_e1_2450.ec.minimized.smt2 \ + FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \ + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ + FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \ + stalmark_e7_27_e7_31.ec.minimized.smt2 \ + stalmark_e7_27_e7_31.ec.smt2 \ + tiny.smt2 # simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 -# javafe.ast.StandardPrettyPrint.319_no_forall.smt2 \ +# javafe.ast.StandardPrettyPrint.319_no_forall.smt2 # javafe.ast.WhileStmt.447_no_forall.smt2 +# CURRENTLY FAILING: +# speed2_e8_449_e8_517.ec.smt2 +# microwave21.ec.minimized.smt2 # Regression tests for PL inputs CVC_TESTS = @@ -41,7 +55,17 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) # Necessary to get automake's attention when splitting TESTS into # SMT_TESTS, SMT2_TESTS, etc.. -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + check02.smt2.expect \ + check03.smt2.expect \ + check04.smt2.expect \ + DRAGON_11_e1_2450.ec.minimized.smt2.expect \ + FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \ + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ + speed2_e8_449_e8_517.ec.smt2.expect \ + stalmark_e7_27_e7_31.ec.minimized.smt2.expect \ + stalmark_e7_27_e7_31.ec.smt2.expect \ + tiny.smt2.expect # synonyms for "check" in this directory .PHONY: regress regress0 test |