From 19ce1179438b41ebfdc8bbabed080ac1a0ed8c0c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 3 Apr 2013 02:09:17 -0500
Subject: [PATCH] abort quantifiers check if master equality engine is
 inconsistent.

---
 src/theory/quantifiers_engine.cpp | 4 ++++
 1 file changed, 4 insertions(+)

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