diff options
| author | Tim King <taking@cs.nyu.edu> | 2014-04-30 17:28:00 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-30 19:07:28 -0400 |
| commit | c5e4a56d4895ce29cd37bac027bb3d486d687f9d (patch) | |
| tree | 6712748188bcfa6dc4e6074e091ee9106729f058 /test/regress/regress0/quantifiers/Makefile.am | |
| parent | 221e509c0eb230aa549fe0107ba88514b6944ca2 (diff) | |
T-entailment work, and QCF (quant conflict find) work that uses it.
This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'test/regress/regress0/quantifiers/Makefile.am')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 9f4998fd8..b21311da1 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -36,15 +36,15 @@ TESTS = \ smtlib384a03.smt2 \ smtlib46f14a.smt2 \ smtlibf957ea.smt2 \ - gauss_init_0030.fof.smt2 + gauss_init_0030.fof.smt2 \ + qcft-javafe.filespace.TreeWalker.006.smt2 \ + qcft-smtlib3dbc51.smt2 \ + symmetric_unsat_7.smt2 \ + javafe.ast.StmtVec.009.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 -# removed because it now reports unknown -# symmetric_unsat_7.smt2 \ -# - # removed because they take more than 20s # ex1.smt2 \ @@ -57,12 +57,11 @@ TESTS = \ # javafe.ast.WhileStmt.447.smt2 \ # javafe.tc.CheckCompilationUnit.001.smt2 \ # javafe.tc.FlowInsensitiveChecks.682.smt2 \ -# array-unsat-simp3.smt2 \ +# array-unsat-simp3.smt2 # EXTRA_DIST = $(TESTS) \ - bug291.smt2.expect \ - array-unsat-simp3.smt2.expect + bug291.smt2.expect #if CVC4_BUILD_PROFILE_COMPETITION #else |