diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-25 00:21:53 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-25 00:21:53 +0000 |
commit | c6216f46da02f995663788399b58a9461005d1b8 (patch) | |
tree | b195d4e13b733ce3b50d8ca5e2342910e9716497 | |
parent | dfaba6987ded6afc0d9502b5f85088260a5a2d96 (diff) |
Checking in fix for bug 340 - somehow didn't get checked in earlier
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index bcdb75845..44e362f90 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -403,7 +403,12 @@ void TheoryArrays::preRegisterTerm(TNode node) } } - d_equalityEngine.addTerm(node); + if (node.getType().isArray()) { + d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY); + } + else { + d_equalityEngine.addTerm(node); + } // Maybe it's a predicate // TODO: remove this or keep it if we allow Boolean elements in arrays. if (node.getType().isBoolean()) { |