#295, don't crash when no set constraint for a loc-array access can b…

…efound, log a warning and merge all blocks

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

@@ -502,6 +502,12 @@ public ArrayGroup getArrayGroupForArrayPvoc(final IProgramVarOrConst pvoc) {
 	public Collection<ArrayGroup> getArrayGroups() {
 		return Collections.unmodifiableCollection(mArrayToArrayGroup.values());
 	}
+
+	public List<StoreInfo> getStoreInfosForDimensionAndArrayGroup(final int dim, final ArrayGroup arrayGroup) {
+		return mLocLitToStoreInfo.values().stream()
+				.filter(si -> si.getDimension() == dim && si.getArrayGroup().equals(arrayGroup))
+				.collect(Collectors.toList());
+	}
 }
 
 class BuildStoreInfos extends NonRecursive {

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

@@ -149,15 +149,19 @@ void processSelect(final SelectInfo selectInfo, final IEqualityProvidingIntermed
 			final Set<Term> setConstraint = eps.getSetConstraintForExpression(locArraySelect);
 
 			if (setConstraint == null) {
-				// analysis found no constraint --> having to merge all
-				// throw an error for now, for debugging
-				throw new AssertionError();
+				/* analysis found no constraint --> having to merge all (this may be ok, in the sense that there still
+				 * may be separation, in particular if it happens in a dimension > 1)
+				 */
+				mLogger.warn("No literal set constraint found for loc-array access " + locArraySelect + " at "
+						+ locArray.getEdge());
+				final List<StoreInfo> allStoreInfos = mCsiaag.getStoreInfosForDimensionAndArrayGroup(dim,
+						selectInfo.getArrayGroup());
+				mergeBlocks(selectInfo, dim, allStoreInfos);
 			} else {
 				final List<StoreInfo> setConstraintAsStoreInfos =
 						setConstraint.stream().map(t -> mCsiaag.getStoreInfoForLocLitTerm(t))
 							.collect(Collectors.toList());
 				mergeBlocks(selectInfo, dim, setConstraintAsStoreInfos);
-
 			}
 		}
 	}

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

@@ -5,6 +5,15 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramNonOldVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 
+/**
+ * Represents a loc-array.
+ * Each loc-array corresponds to one array-term (typically a TermVariable) in some IcfgEdge.
+ * The array-term may or may not be related to an {@link IProgramVarOrConst} (it is, if it belongs to an in var or out
+ * var in the given edge).
+ *
+ * @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
+ *
+ */
 public class LocArrayInfo {
 
 	private final EdgeInfo mEdge;
@@ -13,6 +22,8 @@ public class LocArrayInfo {
 	private final Term mInitializingConstantArray;
 
 	/**
+	 *
+	 * See {@link LocArrayInfo}
 	 *
 	 * Note: the term is not the term from the pvoc (even if it exists)
 	 *
@@ -45,4 +56,8 @@ public Term getInitializingConstantArray() {
 	public boolean isGlobalPvoc() {
 		return mPvoc != null && mPvoc instanceof IProgramNonOldVar;
 	}
+
+	public EdgeInfo getEdge() {
+		return mEdge;
+	}
 }

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java

@@ -459,7 +459,8 @@ public Set<NODE> getSetConstraintForExpression(final NODE exp) {
 		try {
 			result = cLits.get();
 		} catch (final NoSuchElementException nsee) {
-			throw new AssertionError();
+			// no set constraint found --> return null
+			return null;
 		}
 		assert result.hasOnlyLiterals();
 		return result.getLiterals();

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqDisjunctiveConstraint.java

@@ -307,6 +307,9 @@ public Set<Term> getSetConstraintForExpression(final Term exp) {
 		final EqConstraint<NODE> flat = this.flatten();
 
 		final Set<NODE> nodes = flat.getSetConstraintForExpression(node);
+		if (nodes == null) {
+			return null;
+		}
 
 		return nodes.stream().map(n -> n.getTerm()).collect(Collectors.toSet());
 	}