diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 15:51:35 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 15:51:40 -0500 |
| commit | 73a60e60a6036f635e8819c672c227156b351964 (patch) | |
| tree | 7a6693b16d956eb8c676d453b0a289f4be94420b /test/regress/regress0/quantifiers/Makefile.am | |
| parent | d121faf54238a0859cdc2cf1d3d2889631cbfa3a (diff) | |
Fix model construction for BV with cbqi. Minor change to defaults.
Diffstat (limited to 'test/regress/regress0/quantifiers/Makefile.am')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 9c31204e8..eb28efdf6 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -89,8 +89,9 @@ TESTS = \ bug749-rounding.smt2 \ RNDPRE_4_1-dd-nqe.smt2 \ mix-complete-strat.smt2 \ - cbqi-sdlx-fixpoint-3-dd.smt2 - + cbqi-sdlx-fixpoint-3-dd.smt2 \ + qbv-simp.smt2 \ + psyco-001-bv.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 |