From e6150efc1ab45debb10e3ebf560432d8dae68790 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 8 Nov 2014 17:42:50 +0100
Subject: Fix bug with incremental+datatypes.  Minor cleanup.  Disable
 regression bug484, enable parsing_ringer.

---
 test/regress/regress0/Makefile.am        | 3 ++-
 test/regress/regress0/arrays/Makefile.am | 5 ++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'test/regress')

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
 
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index a1232196e..a90b238e2 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -47,7 +47,8 @@ TESTS =	\
 	constarr3.smt2 \
 	constarr.cvc \
 	constarr2.cvc \
-	constarr3.cvc
+	constarr3.cvc \
+	parsing_ringer.cvc
 
 EXTRA_DIST = $(TESTS)
 
@@ -60,8 +61,6 @@ EXTRA_DIST = $(TESTS)
 # and make sure to distribute it
 #EXTRA_DIST += \
 #	error.cvc
-# disabled for now (problem is related to records in model):
-#   parsing_ringer.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
-- 
cgit v1.2.3