diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-25 21:40:58 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-25 20:40:58 +0000 |
| commit | fa6c3db414d27f47e0bee55480df939e78c14eb3 (patch) | |
| tree | 6c4e69973a078b3bd29c212c1d9945cbba0f5497 /src/theory/quantifiers/inst_strategy_enumerative.h | |
| parent | 99a74de90a064133a8e3d03ee9334d59be34ba1d (diff) | |
Ensure nonlinear extensions properly reconsiders its model (#6204)
In certain cases, the nonlinear extension would not re-check properly but only repeat an (already failed) model repair. The result lemma would then already be in cache and thus not be sent to the solver.
This PR ensures that modelBasedRefinement is always run and entirely removes the d_builtModel flag that was responsible for this behavior. Additionally, it asserts that the lemma that (tries to) force the model to be reconciled during theory combination is actually sent.
Fixes #6192.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_enumerative.h')
0 files changed, 0 insertions, 0 deletions