From 41862bfee0f82649400db413a8d4a51dd82eb1b7 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 3 Feb 2010 19:19:36 +0000 Subject: [PATCH] Enabled more regress tests. Takes 26s on my machine to run a make -k check in debug mode. All regress tests currently pass. --- test/regress/Makefile.am | 75 ++++++++++++++++++++++------------------ 1 file 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 -- 2.30.2