diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0bcf1d19c..21c82e9eb 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -205,6 +205,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_qim.reset(); bool setIncomplete = false; + IncompleteId setIncompleteId = IncompleteId::QUANTIFIERS; Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; if( needsCheck ){ @@ -354,7 +355,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //sources of incompleteness for (QuantifiersUtil*& util : d_util) { - if (!util->checkComplete()) + if (!util->checkComplete(setIncompleteId)) { Trace("quant-engine-debug") << "Set incomplete because utility " << util->identify().c_str() @@ -372,7 +373,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //check if we should set the incomplete flag for (QuantifiersModule*& mdl : d_modules) { - if (!mdl->checkComplete()) + if (!mdl->checkComplete(setIncompleteId)) { Trace("quant-engine-debug") << "Set incomplete because module " @@ -447,7 +448,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ { if( setIncomplete ){ Trace("quant-engine") << "Set incomplete flag." << std::endl; - d_qim.setIncomplete(); + d_qim.setIncomplete(setIncompleteId); } //output debug stats d_qim.getInstantiate()->debugPrintModel(); |