summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-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