diff options
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 15 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
2 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index ce024fe8b..81ade68fc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -88,6 +88,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) { return; } + Assert(!d_quantEngine->inConflict()); double clSet = 0; if (Trace.isOn("fs-engine")) { @@ -140,10 +141,10 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } // added lemma addedLemmas++; - if (d_quantEngine->inConflict()) - { - break; - } + } + if (d_quantEngine->inConflict()) + { + break; } } } @@ -324,6 +325,12 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { index--; } + if (d_quantEngine->inConflict()) + { + // could be conflicting for an internal reason (such as term + // indices computed in above calls) + return false; + } } } while (success); max_i++; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4339ee75f..6e60780d6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -601,6 +601,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ << " Theory engine finished : " << !theoryEngineNeedsCheck() << std::endl; Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl; + Trace("quant-engine-debug") + << " In conflict : " << d_conflict << std::endl; } if( Trace.isOn("quant-engine-ee-pre") ){ Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl; |