Fixed failing assertion when EqualityEngine is in conflict

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0cd487d323cde412f77cd1ad36d3c2885431e485..9717f628690d86d49a5cc5b96b39d432b2cba001 100644 (file)
--- 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: