diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-31 11:49:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-31 11:49:02 -0500 |
| commit | 5272f5d02f109b7dbfdb5088a1efbf7d13b64487 (patch) | |
| tree | 04ec8b49d602d7d73ca22126f648b4725972f75a /src/options/idl_options.toml | |
| parent | 5726447e3864c7d2289b458b2d2c5f31b5933a81 (diff) | |
Fix strange bound regression (#4192)
Several things have happened with this regression lately, in chronological order:
(1) Instantiations involving bounded set quantifiers were changed to use choice to represent symbolic instantiations,
(2) fmf-bound was decoupled from finite-model-find (the latter is not enabled when the former is),
(3) choice was set to be an "unevaluated" kind (in 0060de3).
After (1) and (2), for the regression test/regress/regress1/fmf/fmf-strange-bounds.smt2, CVC4 was answering "sat" correctly but internally there was a source of incompleteness. In particular, a choice term was being generated in an instantiation that was later incorrectly evaluated, thus allowing CVC4 to skip an instantiation it shouldn't have.
The recent commit of (3) resolved this issue, making it so that choice is not an evaluated kind. This meant the benchmark went "sat" -> "unknown".
This PR fixes this issue by enabling --finite-model-find, which is now necessary to answer "sat".
It also adds a further test quantifier that was used in debugging this issue.
Fixes regress1.
Diffstat (limited to 'src/options/idl_options.toml')
0 files changed, 0 insertions, 0 deletions