From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 25 May 2012 00:21:53 +0000 (+0000)
Subject: Checking in fix for bug 340 - somehow didn't get checked in earlier
X-Git-Tag: cvc5-1.0.0~8144
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6216f46da02f995663788399b58a9461005d1b8;p=cvc5.git

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 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()) {