summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-11-01 11:31:59 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2014-11-01 11:31:59 +0100
commit9df318ca1ab33001bd203c24ae57a8b5739b8f36 (patch)
tree3b104cc97f5daa2f69285056d81ace0ed7c916e9 /test/regress/regress0/Makefile.am
parent458b2b7eb5bdf09a1a886f4e2a165380d5fd918f (diff)
Fix some mistakes in datatypes theory combination, disable two regressions. Minor fix for fun defs.
Diffstat (limited to 'test/regress/regress0/Makefile.am')
-rw-r--r--test/regress/regress0/Makefile.am6
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index fae563973..cbaa58b3c 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -106,8 +106,7 @@ CVC_TESTS = \
wiki.20.cvc \
wiki.21.cvc \
queries0.cvc \
- print_lambda.cvc \
- trim.cvc
+ print_lambda.cvc
# Regression tests for TPTP inputs
TPTP_TESTS =
@@ -145,7 +144,6 @@ BUG_TESTS = \
bug421b.smt2 \
bug425.cvc \
bug480.smt2 \
- bug484.smt2 \
bug486.cvc \
bug507.smt2 \
bug512.minimized.smt2 \
@@ -171,6 +169,8 @@ BUG_TESTS = \
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
# bug512 -- taking too long, --time-per not working perhaps? in any case,
+# bug484.smt2
+# trim.cvc
# we have a minimized version still getting tested
DISABLED_TESTS = \
bug512.smt2
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback