diff options
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8c619eeae..3165e1f18 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1699,6 +1699,11 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) Node n; while (true) { + // Normally, a is its own representative, but it's possible for a to have + // been merged with another array after it got queued up by the equality engine, + // so we take its representative to be safe. + a = d_equalityEngine.getRepresentative(a); + Assert(d_equalityEngine.getRepresentative(b) == a); Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n"; if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { |