fixed verification of variant

de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java

@@ -55,6 +55,7 @@ public class KeYFileContent {
 	private List<Condition> postConditions;
 	// TODO: ProveWithKey passes this to us as String. It would be better to keep it as Variable.
 	private List<String> unmodifiableVars;
+	private String variant;
 
 	private Map<String, List<Field>> methodClassVarMap = null;
 	private Map<String, String> returnTypeMap = null;
@@ -453,7 +454,7 @@ private String getAssignmentString(Map<String, OldReplacement> oldReplacements)
         assignments.add("heapAtPre := heap");
         assignments.addAll(getUnmodifiableAssignments());
         assignments.addAll(getOldAssignments(oldReplacements));
-
+        if (variant != null) assignments.add("variant := " + variant);
         assignments.removeIf(v -> v.equals(""));
 
 	    return String.join(" || ", assignments); 
@@ -498,6 +499,11 @@ private List<String> getUnmodifiablePostConditions() {
 		return conds;
 	}
 
+	public void setVariantPost(String variant) {
+		this.variant = variant;
+		setPostFromCondition("(" + variant + ") <variant & " + variant + ">=0");
+	}
+
 	private String replaceThisWithSelf(String string) {
 		return string.replaceAll(REGEX_THIS_KEYWORD.pattern(), "self");
 	}

de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/ProveWithKey.java

@@ -616,6 +616,7 @@ public File createProveVariantWithKey(String code, Condition invariant, Conditio
 		content.addVariable("int variant");
 		content.readGlobalConditions(conds);
 		content.setPreFromCondition(invariant.getName() + " & " + guard.getName());
+		content.setVariantPost(variant.getName());
 		content.setStatement(code);
 		content.rename(renaming);
 		content.addSelf(formula);