From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 14 Apr 2012 23:59:17 +0000 (+0000)
Subject: Fixed bug in sharing with arrays of different types
X-Git-Tag: cvc5-1.0.0~8230
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9644b6e12fbd3b649daafa43c5400d272e27bfb4;p=cvc5.git

Fixed bug in sharing with arrays of different types
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 718483143..4a61ca64d 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -545,6 +545,9 @@ void TheoryArrays::computeCareGraph()
     context::CDHashMap<TNode, bool, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
     for (; it1 != iend; ++it1) {
       for (it2 = it1, ++it2; it2 != iend; ++it2) {
+        if ((*it1).first.getType() != (*it2).first.getType()) {
+          continue;
+        }
         EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first);
         if (eqStatusArr != EQUALITY_UNKNOWN) {
           continue;
@@ -578,8 +581,9 @@ void TheoryArrays::computeCareGraph()
 
         if (r1[0] != r2[0]) {
           // If arrays are known to be disequal, or cannot become equal, we can continue
-          if (d_equalityEngine.areDisequal(r1[0], r2[0]) ||
-              (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0]))) {
+          if (r1[0].getType() != r2[0].getType() ||
+              (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) ||
+              d_equalityEngine.areDisequal(r1[0], r2[0])) {
             Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
             continue;
           }