From 13a9ee796ab23d69509544a48c55d4fd281a7de0 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 30 May 2018 15:02:29 -0700 Subject: [PATCH] Fix for issue #2002 (#2012) --- src/theory/arrays/theory_arrays.cpp | 18 ++++++++++-------- 1 file 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]); -- 2.30.2