abort quantifiers check if master equality engine is inconsistent.

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 );