Checking in fix for bug 340 - somehow didn't get checked in earlier

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index bcdb75845f68efaf5dd0c310ea66f14a3299f38e..44e362f906d4090a733665d0659aa83325084e9b 100644 (file)
--- 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()) {