summaryrefslogtreecommitdiff
path: root/test/regress/regress1/nl/Makefile.am
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/nl/Makefile.am')
-rw-r--r--test/regress/regress1/nl/Makefile.am49
1 files changed, 47 insertions, 2 deletions
diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am
index a7e4c1411..bafaf665a 100644
--- a/test/regress/regress1/nl/Makefile.am
+++ b/test/regress/regress1/nl/Makefile.am
@@ -17,8 +17,53 @@ endif
# If a test shouldn't be run in e.g. competition mode,
# put it below in "TESTS +="
TESTS = \
- siegel-nl-bases.smt2 \
- mirko-050417.smt2
+ mirko-050417.smt2 \
+ arrowsmith-050317.smt2 \
+ bug698.smt2 \
+ dist-big.smt2 \
+ dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \
+ exp-4.5-lt.smt2 \
+ metitarski_3_4_2e.smt2 \
+ metitarski-3-4.smt2 \
+ nl-help-unsat-quant.smt2 \
+ poly-1025.smt2 \
+ quant-nl.smt2 \
+ red-exp.smt2 \
+ rewriting-sums.smt2 \
+ simple-mono.smt2 \
+ sin1-sat.smt2 \
+ sin-compare.smt2 \
+ sin-compare-across-phase.smt2 \
+ sqrt-problem-1.smt2 \
+ sugar-ident-2.smt2 \
+ sugar-ident-3.smt2 \
+ tan-rewrite2.smt2 \
+ bad-050217.smt2 \
+ coeff-unsat-base.smt2 \
+ coeff-unsat.smt2 \
+ combine.smt2 \
+ cos-bound.smt2 \
+ cos1-tc.smt2 \
+ disj-eval.smt2 \
+ div-mod-partial.smt2 \
+ exp_monotone.smt2 \
+ exp1-lb.smt2 \
+ metitarski-1025.smt2 \
+ NAVIGATION2.smt2 \
+ nl-unk-quant.smt2 \
+ ones.smt2 \
+ shifting.smt2 \
+ shifting2.smt2 \
+ simple-mono-unsat.smt2 \
+ sin-init-tangents.smt2 \
+ sin-sign.smt2 \
+ sin-sym2.smt2 \
+ sin1-lb.smt2 \
+ sin1-ub.smt2 \
+ sin2-lb.smt2 \
+ sin2-ub.smt2 \
+ sugar-ident.smt2 \
+ zero-subset.smt2
EXTRA_DIST = $(TESTS)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback