summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-11-09 12:17:55 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2014-11-09 12:17:55 +0100
commit4475cfe82e97f549b41b465e71670794cbcd77e4 (patch)
tree159c60c0dadb638965e7de33d5277e7265dec9b5 /test/regress/regress0/Makefile.am
parente6150efc1ab45debb10e3ebf560432d8dae68790 (diff)
Fix dt shared terms issue, reenable regression.
Diffstat (limited to 'test/regress/regress0/Makefile.am')
-rw-r--r--test/regress/regress0/Makefile.am3
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 7ffcff4e3..ad4e8a602 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -145,6 +145,7 @@ BUG_TESTS = \
bug421b.smt2 \
bug425.cvc \
bug480.smt2 \
+ bug484.smt2 \
bug486.cvc \
bug507.smt2 \
bug512.minimized.smt2 \
@@ -174,8 +175,6 @@ 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