diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-15 13:38:45 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-15 13:38:45 -0600 |
| commit | 39ec2fb797623bd1556f81b963ace1997c74e920 (patch) | |
| tree | adf5872fdfdc6b5a1b4f833db62c32b5cca67940 /test/regress | |
| parent | eddabf66104dcc061943655e530d8d8b8d8a7041 (diff) | |
Reenable some regressions, minor. (#1369)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/nl/Makefile.am | 2 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 17 | ||||
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 7 |
3 files changed, 12 insertions, 14 deletions
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 |