diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2017-04-18 16:57:40 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.stanford.edu> | 2017-04-18 16:57:40 -0700 |
| commit | 734b93747d8db91671542d77d0538322acd688b0 (patch) | |
| tree | 37726c4b27176a0bea0f2fc52a9ed97b43950480 /src/theory/arrays/theory_arrays.cpp | |
| parent | 25fcfe393d1d8808a866a5f1cfc4f7edf273316d (diff) | |
Fix for bug 639.
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -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()) { |