diff options
Diffstat (limited to 'src/theory/quantifiers/quant_module.h')
| -rw-r--r-- | src/theory/quantifiers/quant_module.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index e6d5eee76..01a51ccff 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -104,8 +104,11 @@ class QuantifiersModule * * This is called just before the quantifiers engine will return * with no lemmas added during a LAST_CALL effort check. + * + * If this method returns false, it should update incId to the reason for + * why the module was incomplete. */ - virtual bool checkComplete() { return true; } + virtual bool checkComplete(IncompleteId& incId) { return true; } /** Check was complete for quantified formula q * * If for each quantified formula q, some module returns true for |