From c6216f46da02f995663788399b58a9461005d1b8 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 25 May 2012 00:21:53 +0000 Subject: [PATCH] Checking in fix for bug 340 - somehow didn't get checked in earlier --- src/theory/arrays/theory_arrays.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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()) { -- 2.30.2