From: Andres Noetzli 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]);