#295, fixes that came up when running on "difficult" path programs

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java

@@ -191,7 +191,7 @@ private void mergeBlocks(final SelectInfo selectInfo, final int dim,
 
 	private void createPartitionAndBlockIfNecessary(final SelectInfo selectInfo, final int dim, final StoreInfo sample) {
 		final ArrayGroup arrayGroup = selectInfo.getArrayGroup();//mArrayToArrayGroup.get(array);
-		assert selectInfo.getArrayGroup().equals(sample.getArrayGroup());
+		assert selectInfo.getArrayGroup().equals(sample.getArrayGroup()) || sample instanceof NoStoreInfo;
 
 		UnionFind<StoreInfo> partition = mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim);
 		if (partition == null) {

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java

@@ -287,11 +287,18 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 		 * 2. run the equality analysis
 		 */
 		{
-//			final List<String> trackedArraySubstrings = null;
+
+			/*
+			 * tracked arrays are
+			 *  - the loc arrays, because we want information about them
+			 *  - the valid array, because it is important in order for inferring that malloc always returns fresh
+			 *   (valid) values
+			 */
 			final List<String> trackedArraySubstrings = new ArrayList<>();
 			trackedArraySubstrings.add(MemlocArrayManager.LOC_ARRAY_PREFIX);
 			trackedArraySubstrings.add("valid");
 //			trackedArraySubstrings.add("rep");
+
 			equalityProvider.setTrackedArrays(trackedArraySubstrings);
 			equalityProvider.preprocess(preprocessedIcfg);
 			mLogger.info("finished equality analysis");

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/MemlocArrayManager.java

@@ -120,7 +120,9 @@ public LocArrayInfo getOrConstructLocArray(final EdgeInfo edgeInfo, final Term b
 				assert !edgeInfo.getEdge().getTransformula().getAssignedVars().contains(pvoc);
 
 				final Sort locArraySort = computeLocArraySort(baseArrayTerm.getSort(), dim);
+				mMgdScript.lock(this);
 				final IProgramVarOrConst locPvoc = getLocArrayPvocForArrayPvoc(pvoc, dim, locArraySort);
+				mMgdScript.unlock(this);
 
 				/*
 				 *  because there is no update to the array, no LocArray was constructed here during pre-ai-processing
@@ -211,13 +213,13 @@ private HeapSepProgramConst getOrConstructInitLocLitForLocArraySort(final Sort l
 
 	private IProgramVarOrConst getLocArrayPvocForArrayPvoc(final IProgramVarOrConst pvoc, final int dim,
 			final Sort locArraySort) {
+		assert mMgdScript.isLockOwner(this) : "locking before calling this, by convention "
+				+ "(unclear if there are compelling arguments for the convention)";
 		IProgramVarOrConst result = mArrayPvocToDimToLocArrayPvoc.get(pvoc, dim);
 		if (result == null) {
 			if (pvoc instanceof IProgramNonOldVar) {
-				mMgdScript.lock(this);
 				result = ProgramVarUtils.constructGlobalProgramVarPair(
 						sanitizeVarName(LOC_ARRAY_PREFIX + "_" + pvoc + "_" + locArraySort), locArraySort, mMgdScript, this);
-				mMgdScript.unlock(this);
 				mGlobalLocArrays.add((IProgramNonOldVar) result);
 			} else if (pvoc instanceof ILocalProgramVar) {
 				result = constructLocalBoogieVar(sanitizeVarName(LOC_ARRAY_PREFIX + "_" + pvoc + "_" + locArraySort),

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/AddInitializingEdgesIcfgTransformer.java

@@ -224,6 +224,16 @@ private void processLocationsOmitInitEdges(final Set<INLOC> initLocations,
 
 				mBuilder.createNewTransition(split.getSecond(), mBuilder.createNewLocation(oldInitTarget), initEdge);
 
+				/*
+				 * recreate the outgoing transitions of the original init edge, still outgoing from s2
+				 * (doing this because the "initEdge instanceof IcfgCallTransition" case works this way)
+				 */
+				for (final IcfgEdge succEdge : edgesSucceedingInitEdges.getImage(initEdge)) {
+					mBuilder.createNewTransition(mBuilder.createNewLocation(oldInitTarget),
+							mBuilder.createNewLocation((INLOC) succEdge.getTarget()), succEdge);
+				}
+
+
 			} else {
 				throw new AssertionError("init edge is neither call nor internal transition");
 			}

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTransitionTransformer.java

@@ -200,10 +200,7 @@ public TransformulaTransformationResult transform(final IIcfgTransition<? extend
 							arrayCellAccessToDimensionToLocationBlock,
 							edgeInfo, mArrayGroupToDimensionToLocationBlocks,
 							mCsiag,
-//							mArrayToArrayGroup,
-//							mCsiag.getArrayToArrayGroup(),
-//							mEdgeToIndexToStoreIndexInfo,
-							mHeapArrays);//,
+							mHeapArrays);
 			final Term transformedFormulaRaw = ppttf.transform(tf.getFormula());
 			ppttf.finish();
 
@@ -225,6 +222,14 @@ public TransformulaTransformationResult transform(final IIcfgTransition<? extend
 
 				final TermVariable inTv = ppttf.getNewInVars().get(ov.getKey());
 				final TermVariable outTv = ov.getValue();
+				assert outTv != null;
+
+				if (inTv == null) {
+					/* outvar has no corresponding invar --> there are no "neutral" terms like a1' = a1,
+					 *  --> current equation is definitely an actual update */
+					  continue;
+				}
+
 				if (inTv.equals(outTv)) {
 					// not an assigned var
 					continue;