Another small bug fix in the ArrayInterpolator.

Open A-paths with main diseq.
ultimate-pa · Feb 2, 2018 · 80ac777 · 80ac777
1 parent af68637
commit 80ac777
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/...ol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java b/...ol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java
@@ -996,9 +996,11 @@ public void addDiseq(Occurrence headOcc, Occurrence tailOcc) {
 				mHead.closeAPath(mTail, boundaryHeadTerm, headOcc);
 				mHead.openAPath(mTail, boundaryHeadTerm, headOcc);
 				mHead.closeAPath(mTail, boundaryHeadTerm, mDiseqInfo);
+				mHead.openAPath(mTail, boundaryHeadTerm, mDiseqInfo);
 				mTail.closeAPath(mHead, boundaryTailTerm, tailOcc);
 				mTail.openAPath(mHead, boundaryTailTerm, tailOcc);
 				mTail.closeAPath(mHead, boundaryTailTerm, mDiseqInfo);
+				mTail.openAPath(mHead, boundaryTailTerm, mDiseqInfo);
 
 				if (mLemmaInfo.getLemmaType().equals(":read-over-weakeq")) {
 					if (mIndexEquality != null) {