From 095d208d95a682ac63b80a059b1a0900e676759f Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 13 Jun 2012 17:06:08 +0000
Subject: [PATCH] Fixed failing assertion when EqualityEngine is in conflict

---
 src/theory/arrays/theory_arrays.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0cd487d32..9717f6286 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -359,6 +359,9 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
  */
 void TheoryArrays::preRegisterTerm(TNode node)
 {
+  if (d_conflict) {
+    return;
+  }
   Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
   switch (node.getKind()) {
   case kind::EQUAL:
-- 
2.30.2