From: Tim King <taking@cs.nyu.edu>
Date: Wed, 3 Feb 2010 19:19:36 +0000 (+0000)
Subject: Enabled more regress tests. Takes 26s on my machine to run a make -k check in debug... 
X-Git-Tag: cvc5-1.0.0~9306
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41862bfee0f82649400db413a8d4a51dd82eb1b7;p=cvc5.git

Enabled more regress tests. Takes 26s on my machine to run a make -k check in debug mode.  All regress tests currently pass.
---

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