From: Andrew Reynolds 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