diff options
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 18 |
1 files changed, 10 insertions, 8 deletions
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]); |