diff --git a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java index 4604a05af..e1887cefa 100644 --- a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java +++ b/SMTInterpol/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) {