Fix for issue #2002 (#2012)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dfa543ff37229dedab8e5e2d76c704cc7396b1f9..87edbe3163b9c0fb782794acc3d37e3f826cdea4 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -659,6 +659,16 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     // The may equal needs the store
     d_mayEqualEqualityEngine.addTerm(store);
 
+    if (node.getType().isArray())
+    {
+      d_mayEqualEqualityEngine.addTerm(node);
+      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+    }
+    else
+    {
+      d_equalityEngine.addTerm(node);
+    }
+
     if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) {
       // Apply RIntro1 rule to any stores equal to store if not done already
       const CTNodeList* stores = d_infoMap.getStores(store);
@@ -679,14 +689,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
       }
     }
 
-    if (node.getType().isArray()) {
-      d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
-    }
-    else {
-      d_equalityEngine.addTerm(node);
-    }
-
     Assert(d_equalityEngine.getRepresentative(store) == store);
     d_infoMap.addIndex(store, node[1]);