Modify slow regressions.

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 60b10666eff7a3d906a42001b4cac50560f6c70a..1306fac5f6716090031bf6c17ade440b79ede206 100644 (file)
--- 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 (file)
index 0000000..7847608
--- /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 cf0f005b93302ad4078ba48a186985900c51c8ad..0c78fd7bf7299346330489de16ed1d329c18d685 100644 (file)
--- 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