From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Nov 2017 19:38:45 +0000 (-0600)
Subject: Reenable some regressions, minor. (#1369)
X-Git-Tag: cvc5-1.0.0~5471
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39ec2fb797623bd1556f81b963ace1997c74e920;p=cvc5.git

Reenable some regressions, minor. (#1369)
---

diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index 7e4b391cc..d26d53d07 100644
--- 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 135a2c8d2..274dcaff0 100644
--- 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 cd3351c59..c4fb8dd94 100644
--- 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