diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-14 21:58:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-14 21:58:08 -0500 |
| commit | 4a1b5ea5568fb6c688f407946f9a7fbb1cec3c31 (patch) | |
| tree | 016119f36abe7835183ce3ca3e2b7ffdaa383fcb /src/theory/quantifiers_engine.h | |
| parent | 996f6f9e2ecf76e39c236f9c410c109807c7073d (diff) | |
Fix needsModel method for CEGQI (#5048)
There was a bug in CEGQI's needModel method which could say that it doesnt need a model built when there are no active quantifiers. However, computing active quantifiers is not done in QuantifiersEngine::check until after this method is called, meaning it was using stale data on whether a quantifier was active or not. This could lead to the use of bogus models in CEGQI in incremental mode in some corner cases, leading to the assertion failure in #5019.
Fixes #5019.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
0 files changed, 0 insertions, 0 deletions