diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-04-03 02:09:17 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-04-03 02:09:17 -0500 |
commit | 19ce1179438b41ebfdc8bbabed080ac1a0ed8c0c (patch) | |
tree | 9ce049b6acbe30c32fb2c730c46597138bf840b7 | |
parent | de93aad21f843d54d02d0304343dffcb36dc2e09 (diff) |
abort quantifiers check if master equality engine is inconsistent.
-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 ); |