summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-11-08 17:42:50 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2014-11-08 17:42:57 +0100
commite6150efc1ab45debb10e3ebf560432d8dae68790 (patch)
tree7670c4b6b784285303da03ca9e27e8c4bcb5dcf1 /test/regress/regress0/Makefile.am
parent5f4e66786b24d76bcd20cede25473ba326a2e381 (diff)
Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug484, enable parsing_ringer.
Diffstat (limited to 'test/regress/regress0/Makefile.am')
-rw-r--r--test/regress/regress0/Makefile.am3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index ad4e8a602..7ffcff4e3 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -145,7 +145,6 @@ BUG_TESTS = \
bug421b.smt2 \
bug425.cvc \
bug480.smt2 \
- bug484.smt2 \
bug486.cvc \
bug507.smt2 \
bug512.minimized.smt2 \
@@ -175,6 +174,8 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
# bug512 -- taking too long, --time-per not working perhaps? in any case,
# we have a minimized version still getting tested
+# disabled for now (dt sharing issue):
+# bug484.smt2
DISABLED_TESTS = \
bug512.smt2
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback