diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-30 15:02:29 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-30 15:02:29 -0700 |
commit | 13a9ee796ab23d69509544a48c55d4fd281a7de0 (patch) | |
tree | 499e2402cde02b7d295daf5240e318c76fb5fb36 /src/theory/arrays | |
parent | eb733c1a2c806b34abcdf0d8497fa579f2b1e66e (diff) |
Fix for issue #2002 (#2012)
Diffstat (limited to 'src/theory/arrays')
-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]); |