From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 3 Apr 2013 07:09:17 +0000 (-0500)
Subject: abort quantifiers check if master equality engine is inconsistent.
X-Git-Tag: cvc5-1.0.0~7335
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=19ce1179438b41ebfdc8bbabed080ac1a0ed8c0c;p=cvc5.git

abort quantifiers check if master equality engine is inconsistent.
---

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