diff --git a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/IcfgBacktranslator.java b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/IcfgBacktranslator.java
index 5dd7c840ca5..22eae444487 100644
--- a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/IcfgBacktranslator.java
+++ b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/IcfgBacktranslator.java
@@ -422,8 +422,9 @@ private static void createNewEdge(final Multigraph<String, BoogieASTNode> source
 	}
 
 	private static Multigraph<String, BoogieASTNode> createWitnessNode(final IcfgLocation old) {
-		final WitnessInvariant inv = WitnessInvariant.getAnnotation(old);
-		final Multigraph<String, BoogieASTNode> rtr = new Multigraph<>(inv == null ? null : inv.getInvariant());
+		final WitnessInvariant<?> inv = WitnessInvariant.getAnnotation(old);
+		final Multigraph<String, BoogieASTNode> rtr =
+				new Multigraph<>(inv == null ? null : inv.getInvariant().toString());
 		ModelUtils.copyAnnotations(old, rtr);
 		return rtr;
 	}
@@ -432,6 +433,7 @@ private static Multigraph<String, BoogieASTNode> createWitnessNode(final IcfgLoc
 	public Expression translateExpression(final Term term) {
 		return mTerm2Expression.translate(term);
 	}
+
 	// TODO maybe take getStepInfoFromCondition from BoogiePreprocessorBacktranslator
 	private StepInfo getStepInfoFromCondition(final Expression input, final Expression output) {
 		// compare the depth of UnaryExpression in the condition of the assume