abort quantifiers check if master equality engine is inconsistent.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6ec5ea2a406b003309b4396c9844d287f7780d02..0bb0f1f798699947fd7435b9d335900f61366a1a 100644 (file)
--- 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 );