diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2017-04-21 15:09:33 -0700 |
---|---|---|
committer | Clark Barrett <barrett@cs.stanford.edu> | 2017-04-21 15:09:33 -0700 |
commit | 8740a03cf22b0e05bbdab4cdd799cb7469a6ae6e (patch) | |
tree | 4cb6094be4ea788469d6333005bf27b6e06f62ea /src/theory/arrays | |
parent | 23e5362ba8d356b72ba8b488278327cf43c59f66 (diff) |
Fix for bug 681 (now gives reasonable error message about using constant
arrays).
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
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"); } } |