From 734b93747d8db91671542d77d0538322acd688b0 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Tue, 18 Apr 2017 16:57:40 -0700 Subject: [PATCH] Fix for bug 639. --- src/theory/arrays/theory_arrays.cpp | 5 +++++ 1 file changed, 5 insertions(+) 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()) { -- 2.30.2