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/regress0/quantifiers | |
| parent | eddabf66104dcc061943655e530d8d8b8d8a7041 (diff) | |
Reenable some regressions, minor. (#1369)
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 17 |
1 files changed, 8 insertions, 9 deletions
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 |