From 875d0f0b01339aab4e60c408f1d7aa601e9653e6 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 17 Jun 2014 23:03:22 -0400
Subject: disable unate lemmas when using incremental mode

---
 test/regress/regress0/Makefile.am | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 10148e5bc..18931e3fa 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -147,7 +147,6 @@ BUG_TESTS = \
 	bug484.smt2 \
 	bug486.cvc \
 	bug507.smt2 \
-	bug512.smt2 \
 	bug512.minimized.smt2 \
 	bug516.smt2 \
 	bug519.smt2 \
@@ -162,6 +161,11 @@ 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,
+# we have a minimized version still getting tested
+DISABLED_TESTS = \
+	bug512.smt2
+
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect \
 	bug216.smt2.expect
@@ -175,7 +179,7 @@ TESTS += \
 endif
 
 # and make sure to distribute it
-EXTRA_DIST += \
+EXTRA_DIST += $(DISABLED_TESTS) \
 	subranges.cvc \
 	arrayinuf_error.smt2 \
 	errorcrash.smt2 \
-- 
cgit v1.2.3