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 /src/theory/arrays/theory_arrays.cpp | |
| parent | dfaba6987ded6afc0d9502b5f85088260a5a2d96 (diff) | |
Checking in fix for bug 340 - somehow didn't get checked in earlier
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -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()) { |