diff options
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6ec5ea2a4..0bb0f1f79 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -122,6 +122,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; + if( !getMasterEqualityEngine()->consistent() ){ + Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl; + return; + } //reset relevant information d_hasAddedLemma = false; d_term_db->reset( e ); |