From: Clark Barrett <barrett@cs.stanford.edu>
Date: Tue, 18 Apr 2017 23:57:40 +0000 (-0700)
Subject: Fix for bug 639.
X-Git-Tag: cvc5-1.0.0~5833
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=734b93747d8db91671542d77d0538322acd688b0;p=cvc5.git

Fix for bug 639.
---

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()) {