diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 11:31:59 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 11:31:59 +0100 |
commit | 9df318ca1ab33001bd203c24ae57a8b5739b8f36 (patch) | |
tree | 3b104cc97f5daa2f69285056d81ace0ed7c916e9 /test | |
parent | 458b2b7eb5bdf09a1a886f4e2a165380d5fd918f (diff) |
Fix some mistakes in datatypes theory combination, disable two regressions. Minor fix for fun defs.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 6 |
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 |