From d4a7b0cf0500e971c9c01e7628f3c1b567715059 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 27 Aug 2015 09:32:14 +0200
Subject: [PATCH] Modify slow regressions.

---
 test/regress/regress0/quantifiers/Makefile.am  | 5 +++--
 test/regress/regress0/quantifiers/clock-3.smt2 | 5 +++++
 test/regress/regress0/sygus/Makefile.am        | 2 +-
 3 files changed, 9 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/quantifiers/clock-3.smt2

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 60b10666e..1306fac5f 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -53,7 +53,7 @@ TESTS =	\
 	nested-delta.smt2 \
 	nested-inf.smt2 \
 	RND-small.smt2 \
-	clock-10.smt2 \
+	clock-3.smt2 \
 	006-cbqi-ite.smt2
 
 
@@ -73,7 +73,8 @@ TESTS =	\
 #		javafe.ast.WhileStmt.447.smt2 \
 #		javafe.tc.CheckCompilationUnit.001.smt2 \
 #		javafe.tc.FlowInsensitiveChecks.682.smt2 \
-#		array-unsat-simp3.smt2
+#		array-unsat-simp3.smt2 \
+#		clock-10.smt2
 #
 
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/quantifiers/clock-3.smt2 b/test/regress/regress0/quantifiers/clock-3.smt2
new file mode 100644
index 000000000..78476083d
--- /dev/null
+++ b/test/regress/regress0/quantifiers/clock-3.smt2
@@ -0,0 +1,5 @@
+(set-logic LIA)
+(set-info :status unsat)
+(declare-fun t () Int)
+(assert (forall ((s Int) (m Int)) (or (not (= (+ (* 3 m) s) t)) (< s 0) (>= s 3))))
+(check-sat)
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index cf0f005b9..0c78fd7bf 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -31,7 +31,6 @@ TESTS = commutative.sy \
         icfp_28_10.sy \
         const-var-test.sy \
         no-syntax-test.sy \
-        no-syntax-test-no-si.sy \
         no-flat-simp.sy \
         twolets2-orig.sy \
         let-ringer.sy \
@@ -62,6 +61,7 @@ EXTRA_DIST = $(TESTS) \
 # disabled tests, yet distribute
 #EXTRA_DIST += \
 # setofsets-disequal.smt2
+# no-syntax-test-no-si.sy
 
 # synonyms for "check"
 .PHONY: regress regress0 test
-- 
2.30.2