diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-02-03 19:19:36 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-02-03 19:19:36 +0000 |
| commit | 41862bfee0f82649400db413a8d4a51dd82eb1b7 (patch) | |
| tree | 72c348c30fe2691ee96057c01cb217ad3a58daad /test/regress/Makefile.am | |
| parent | 690bd6341c0ede1ff9edc30f8a8ce384fa936008 (diff) | |
Enabled more regress tests. Takes 26s on my machine to run a make -k check in debug mode. All regress tests currently pass.
Diffstat (limited to 'test/regress/Makefile.am')
| -rw-r--r-- | test/regress/Makefile.am | 75 |
1 files changed, 41 insertions, 34 deletions
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index bf5c21af3..819a892bd 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,40 +1,47 @@ TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4 TESTS = \ simple.cvc \ - simple.smt -# bug1.cvc \ -# boolean.cvc \ -# hole10.cvc \ -# hole6.cvc \ -# hole7.cvc \ -# hole8.cvc \ -# hole9.cvc \ -# test9.cvc \ -# test12.cvc \ -# test11.cvc \ -# uf20-03.cvc \ -# qwh.35.405.shuffled-as.sat03-1651.smt \ -# C880mul.miter.shuffled-as.sat03-348.smt \ -# instance_1151.smt \ -# instance_1444.smt \ -# friedman_n4_i5.smt \ -# friedman_n6_i4.smt \ -# bmc-galileo-8.smt \ -# bmc-galileo-9.smt \ -# bmc-ibm-1.smt \ -# bmc-ibm-2.smt \ -# bmc-ibm-3.smt \ -# bmc-ibm-4.smt \ -# bmc-ibm-5.smt \ -# bmc-ibm-6.smt \ -# bmc-ibm-7.smt \ -# bmc-ibm-10.smt \ -# bmc-ibm-11.smt \ -# bmc-ibm-12.smt \ -# bmc-ibm-13.smt \ -# wiki.cvc \ -# logops.cvc \ -# comb2.shuffled-as.sat03-420.smt + simple.smt \ + hole6.cvc \ + hole7.cvc \ + hole8.cvc \ + hole9.cvc \ + hole10.cvc \ + wiki.cvc \ + test9.cvc \ + test11.cvc \ + bmc-ibm-1.smt \ + bmc-ibm-2.smt \ + bmc-ibm-3.smt \ + bmc-ibm-4.smt \ + bmc-ibm-5.smt \ + uf20-03.cvc \ + qwh.35.405.shuffled-as.sat03-1651.smt \ + C880mul.miter.shuffled-as.sat03-348.smt \ + instance_1151.smt \ + instance_1444.smt + +#Tests that currently do not work +FUTURETESTS = \ + logops.cvc \ + test12.cvc \ + bug1.cvc \ + boolean.cvc + +#Tests that take too long to be put in the default regress level +#TODO Make multiple regression levels. Some of which are off by default. +LONGTESTS = \ + friedman_n4_i5.smt \ + friedman_n6_i4.smt \ + bmc-galileo-8.smt \ + bmc-galileo-9.smt \ + bmc-ibm-6.smt \ + bmc-ibm-7.smt \ + bmc-ibm-10.smt \ + bmc-ibm-11.smt \ + bmc-ibm-12.smt \ + bmc-ibm-13.smt \ + comb2.shuffled-as.sat03-420.smt # synonyms for "check" .PHONY: regress regress0 regress1 regress2 regress3 test |