diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-30 11:12:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-30 11:12:39 -0500 |
| commit | f9e61ad68d6e5811c7471fa36061b50709ab2fa3 (patch) | |
| tree | 88515d22b969dc8c69486517050b4071b7ae6a93 /src/expr/expr_manager_template.h | |
| parent | 724d8cf23ae74158b36b408643298c49c3b20833 (diff) | |
Simplify quantifiers strategy for when to apply last call effort check with fmfBound (#4673)
There was a strategy in place for alternating which rounds quantifier instantiation would run on when --fmf-bound is enabled.
However, this made it so that in some cases, no instantiation strategy would be applied, if e.g. fmfBound was enabled but no quantified formulas were handled by that strategy.
It is not clear if this strategy is a good idea, considering all use cases of quantifiers, and hence this PR deletes this block of code.
This makes it so that several eqrange benchmarks are answered "unsat" quickly.
Diffstat (limited to 'src/expr/expr_manager_template.h')
0 files changed, 0 insertions, 0 deletions