Enabled more regress tests. Takes 26s on my machine to run a make -k check in debug...
authorTim King <taking@cs.nyu.edu>
Wed, 3 Feb 2010 19:19:36 +0000 (19:19 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 3 Feb 2010 19:19:36 +0000 (19:19 +0000)
test/regress/Makefile.am

index bf5c21af3faa938a1a9537fd37b4060d4478595e..819a892bd6831c97f2027b874b77722f42e6cf99 100644 (file)
@@ -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