From 6eb8ea92ed1a8f8989f5e6ec297f7b65ede6cec3 Mon Sep 17 00:00:00 2001 From: danieldietsch Date: Tue, 28 Nov 2017 12:28:12 +0100 Subject: [PATCH] Updated SMTInterpol to 2.1-431-g374a72f --- .../informatik/ultimate/smtinterpol/Version.properties | 4 ++-- .../ultimate/smtinterpol/interpolate/ArrayInterpolator.java | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/Version.properties b/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/Version.properties index 0fa39d6eb78..e7af36b825a 100644 --- a/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/Version.properties +++ b/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/Version.properties @@ -1,5 +1,5 @@ -#Tue, 28 Nov 2017 11:03:22 +0100 +#Tue, 28 Nov 2017 12:28:07 +0100 -version=2.1-429-gfab41a1 +version=2.1-431-g374a72f build.date=2017-11-28 build.year=2017 diff --git a/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java b/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java index 7d09080ca15..8c265d748a7 100644 --- a/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java +++ b/trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/interpolate/ArrayInterpolator.java @@ -435,6 +435,8 @@ private void addIndexEqualityReadOverWeakeq(WeakPathInfo mainPath) { if (mainPath.mSharedIndex[color] != null && mainPath.mSharedIndex[color] == mStorePath.getIndex()) { if (indexEqInfo.isALocal(color) && otherSelectOccur.isBorShared(color)) { mInterpolants[color].add(mInterpolator.unquote(mIndexEquality)); + } else if (indexEqInfo.isBLocal(color) && mDiseqInfo.isALocal(color)) { + mInterpolants[color].add(mTheory.not(mInterpolator.unquote(mIndexEquality))); } } }