diff options
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 |