From: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri, 21 Apr 2017 22:09:33 +0000 (-0700)
Subject: Fix for bug 681 (now gives reasonable error message about using constant
X-Git-Tag: cvc5-1.0.0~5824
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8740a03cf22b0e05bbdab4cdd799cb7469a6ae6e;p=cvc5.git

Fix for bug 681 (now gives reasonable error message about using constant
arrays).
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3165e1f18..f67112eec 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1754,18 +1754,20 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
       }
     }
 
-    // If a and b have different default values associated with their mayequal equivalence classes,
-    // things get complicated - disallow this for now.  -Clark
     TNode mayRepA = d_mayEqualEqualityEngine.getRepresentative(a);
     TNode mayRepB = d_mayEqualEqualityEngine.getRepresentative(b);
 
+    // If a and b have different default values associated with their mayequal equivalence classes,
+    // things get complicated.  Similarly, if two mayequal equivalence classes have different
+    // constant representatives, it's not clear what to do. - disallow these cases for now.  -Clark
     DefValMap::iterator it = d_defValues.find(mayRepA);
     DefValMap::iterator it2 = d_defValues.find(mayRepB);
     TNode defValue;
 
     if (it != d_defValues.end()) {
       defValue = (*it).second;
-      if (it2 != d_defValues.end() && (defValue != (*it2).second)) {
+      if ((it2 != d_defValues.end() && (defValue != (*it2).second)) ||
+          (mayRepA.isConst() && mayRepB.isConst() && mayRepA != mayRepB)) {
         throw LogicException("Array theory solver does not yet support write-chains connecting two different constant arrays");
       }
     }