Updated SMTInterpol to 2.1-431-g374a72f

danieldietsch · danieldietsch · commit 6eb8ea92ed1a · 2017-11-28T12:28:12.000+01:00
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
@@ -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
@@ -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)));
 				}
 			}
 		}

Original file line number	Diff line number	Diff line change
`@@ -435,6 +435,8 @@ private void addIndexEqualityReadOverWeakeq(WeakPathInfo mainPath) {`
`435`	`435`	`if (mainPath.mSharedIndex[color] != null && mainPath.mSharedIndex[color] == mStorePath.getIndex()) {`
`436`	`436`	`if (indexEqInfo.isALocal(color) && otherSelectOccur.isBorShared(color)) {`
`437`	`437`	`mInterpolants[color].add(mInterpolator.unquote(mIndexEquality));`
	`438`	`+ } else if (indexEqInfo.isBLocal(color) && mDiseqInfo.isALocal(color)) {`
	`439`	`+ mInterpolants[color].add(mTheory.not(mInterpolator.unquote(mIndexEquality)));`
`438`	`440`	`}`
`439`	`441`	`}`
`440`	`442`	`}`