Reenable some regressions, minor. (#1369)

diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index 7e4b391ccddb10e4c19ba18dc84670c3eaf1aaf4..d26d53d074b3689343d0213e5a863ea8d44f6dd3 100644 (file)
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -68,8 +68,6 @@ TESTS =       \
   nta/sin-init-tangents.smt2 \
   nta/cos1-tc.smt2
 
-# unsolved : garbage_collect.cvc
-
 EXTRA_DIST = $(TESTS)
 
 # synonyms for "check"

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 135a2c8d2205b1fcfa2590e157fac5a3f360338e..274dcaff0a3765ed48e3091e2b19b3905f269f08 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -114,7 +114,13 @@ TESTS =    \
        small-pipeline-fixpoint-3.smt2 \
        NUM878.smt2 \
        psyco-107-bv.smt2 \
-       ari118-bv-2occ-x.smt2
+       ari118-bv-2occ-x.smt2 \
+       javafe.ast.StandardPrettyPrint.319.smt2 \
+       javafe.ast.StmtVec.009.smt2 \
+       javafe.ast.WhileStmt.447.smt2 \
+       clock-10.smt2 \
+       javafe.tc.FlowInsensitiveChecks.682.smt2 \
+       javafe.tc.CheckCompilationUnit.001.smt2
  
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
@@ -122,14 +128,7 @@ TESTS =    \
 
 
 # removed because they take more than 20s
-#              javafe.ast.ArrayInit.35.smt2 \
-#              javafe.ast.StandardPrettyPrint.319.smt2 \
-#              javafe.ast.StmtVec.009.smt2 \
-#              javafe.ast.WhileStmt.447.smt2 \
-#              javafe.tc.CheckCompilationUnit.001.smt2 \
-#              javafe.tc.FlowInsensitiveChecks.682.smt2 \
-#              clock-10.smt2
-#              extract-nproc.smt2
+#              javafe.ast.ArrayInit.35.smt2
 
 # FIXME: I've disabled these since they give different error messages on production and debug
 #      macro-subtype-param.smt2 

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index cd3351c59e1d57b95aa94210516014411ba59f8c..c4fb8dd94d34838ee04de5732f0d65f9ccff37c8 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -91,7 +91,9 @@ TESTS = \
   strings-charat.cvc \
   issue1105.smt2 \
   issue1189.smt2 \
-  rewrites-v2.smt2
+  rewrites-v2.smt2 \
+  norn-ab.smt2 \
+  type002.smt2
 
 FAILING_TESTS =
 
@@ -101,8 +103,7 @@ EXTRA_DIST = $(TESTS)
 EXTRA_DIST +=
 
 #norn-dis-0707-3.smt2
-#norn-ab.smt2
-#type002.smt2
+
 
 # synonyms for "check"
 .PHONY: regress regress0 test