From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 30 May 2018 22:02:29 +0000 (-0700)
Subject: Fix for issue #2002 (#2012)
X-Git-Tag: cvc5-1.0.0~4993
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13a9ee796ab23d69509544a48c55d4fd281a7de0;p=cvc5.git

Fix for issue #2002 (#2012)
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dfa543ff3..87edbe316 100644
--- 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]);