diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-12 10:38:36 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-12 10:38:36 -0600 |
| commit | fd3844131f334e929bfb04eb2dcb6229cf1190cd (patch) | |
| tree | e8a66486a618598d3a901f15f5169ed1b946d38a /test | |
| parent | d0df704a60696d7f824eb01781b413d91a0e4202 (diff) | |
Add options related to interleaving quantifiers and theory combination, changes default behavior.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 6e7b25286..e8000eff1 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -38,10 +38,9 @@ TESTS = \ gauss_init_0030.fof.smt2 \ qcft-javafe.filespace.TreeWalker.006.smt2 \ qcft-smtlib3dbc51.smt2 \ - symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ ARI176e1.smt2 \ - bi-artm-s.smt2 \ + bi-artm-s.smt2 \ simp-typ-test.smt2 \ macros-int-real.smt2 \ stream-x2014-09-18-unsat.smt2 \ @@ -65,18 +64,18 @@ TESTS = \ ext-ex-deq-trigger.smt2 \ matching-lia-1arg.smt2 \ RND_4_16.smt2 \ - cdt-0208-to.smt2 \ - psyco-196.smt2 \ - agg-rew-test.smt2 \ - agg-rew-test-cf.smt2 \ - rew-to-0211-dd.smt2 \ - rew-to-scala.smt2 \ - macro-subtype-param.smt2 \ - macros-real-arg.smt2 \ - subtype-param-unk.smt2 \ - subtype-param.smt2 \ - anti-sk-simp.smt2 \ - pure_dt_cbqi.smt2 + cdt-0208-to.smt2 \ + psyco-196.smt2 \ + agg-rew-test.smt2 \ + agg-rew-test-cf.smt2 \ + rew-to-0211-dd.smt2 \ + rew-to-scala.smt2 \ + macro-subtype-param.smt2 \ + macros-real-arg.smt2 \ + subtype-param-unk.smt2 \ + subtype-param.smt2 \ + anti-sk-simp.smt2 \ + pure_dt_cbqi.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine |