diff --git a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java
index fe18431195a..4f0c99c1c14 100644
--- a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java
+++ b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java
@@ -111,7 +111,6 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.LoopEntryDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.OrdinaryDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureEntryDebugIdentifier;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier.ProcedureErrorType;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorWithCheckDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureExitDebugIdentifier;
@@ -445,8 +444,12 @@ private void addCallTransitionAndReturnTransition(final Summary edge,
 	 *
 	 * @return
 	 */
-	private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode,
+	private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode, final Check check,
 			final Map<DebugIdentifier, BoogieIcfgLocation> procLocNodes) {
+		if (check == null) {
+			throw new IllegalArgumentException(
+					"Constructing error location without specification for the following AST node: " + boogieASTNode);
+		}
 		Set<BoogieIcfgLocation> errorNodes = mIcfg.getProcedureErrorNodes().get(procName);
 		final int locNodeNumber;
 		if (errorNodes == null) {
@@ -462,7 +465,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo
 			type = ProcedureErrorType.ASSERT_VIOLATION;
 		} else if (boogieASTNode instanceof EnsuresSpecification) {
 			type = ProcedureErrorType.ENSURES_VIOLATION;
-		} else if (boogieASTNode instanceof RequiresSpecification) {
+		} else if (boogieASTNode instanceof CallStatement) {
 			type = ProcedureErrorType.REQUIRES_VIOLATION;
 		} else if (boogieASTNode instanceof ForkStatement) {
 			type = ProcedureErrorType.INUSE_VIOLATION;
@@ -472,13 +475,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo
 			throw new IllegalArgumentException();
 		}
 
-		final ProcedureErrorDebugIdentifier errorLocLabel;
-		final Check check = Check.getAnnotation(boogieASTNode);
-		if (check == null) {
-			throw new IllegalArgumentException(
-					"Constructing error location without specification for the following AST node: " + boogieASTNode);
-		}
-		errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check);
+		final var errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check);
 		final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode);
 		check.annotate(errorLocNode);
 		procLocNodes.put(errorLocLabel, errorLocNode);
@@ -1025,7 +1022,8 @@ private BoogieIcfgLocation buildAssert(final IIcfgElement currentElement, final
 
 		private BoogieIcfgLocation buildBranchingToNewErrorLocation(final IIcfgElement currentElement,
 				final Expression formula, final BoogieASTNode origin) {
-			final BoogieIcfgLocation error = addErrorNode(mCurrentProcedureName, origin, mProcLocNodes);
+			final BoogieIcfgLocation error =
+					addErrorNode(mCurrentProcedureName, origin, Check.getAnnotation(origin), mProcLocNodes);
 			mProcLocNodes.put(error.getDebugIdentifier(), error);
 			final AssumeStatement condNotError;
 			if (mAddAssumeForEachAssert) {
@@ -1282,11 +1280,12 @@ private IIcfgElement buildCall(final IIcfgElement currentLocation, final CallSta
 					final Statement st1 = assumeSt;
 					ModelUtils.copyAnnotations(st, st1);
 					mIcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { st, spec });
-					final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes);
+					final BoogieIcfgLocation errorLocNode =
+							addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(spec), mProcLocNodes);
 					final StatementSequence errorCB =
 							mCbf.constructStatementSequence(newLocation, errorLocNode, assumeSt);
 					ModelUtils.copyAnnotations(spec, errorCB);
-					ModelUtils.copyAnnotations(spec, errorLocNode);
+					ModelUtils.copyAnnotationsExcept(spec, errorLocNode, ILocation.class);
 					mEdges.add(errorCB);
 				}
 			}
@@ -1550,7 +1549,8 @@ private void assertAndAssumeEnsures() {
 					final Statement st = assumeSt;
 					ModelUtils.copyAnnotations(spec, st);
 					mIcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { spec });
-					final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes);
+					final BoogieIcfgLocation errorLocNode =
+							addErrorNode(mCurrentProcedureName, spec, Check.getAnnotation(spec), mProcLocNodes);
 					final CodeBlock assumeEdge = mCbf.constructStatementSequence(finalNode, errorLocNode, assumeSt);
 					ModelUtils.copyAnnotations(spec, assumeEdge);
 					ModelUtils.copyAnnotations(spec, errorLocNode);
diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java
index 3f52c0be61b..015e15a5799 100644
--- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java
+++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java
@@ -101,7 +101,6 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.LoopEntryDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.OrdinaryDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureEntryDebugIdentifier;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier.ProcedureErrorType;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorWithCheckDebugIdentifier;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureExitDebugIdentifier;
@@ -420,8 +419,12 @@ private void addCallTransitionAndReturnTransition(final Summary edge,
 	 *
 	 * @return
 	 */
-	private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode,
+	private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode, final Check check,
 			final Map<DebugIdentifier, BoogieIcfgLocation> procLocNodes) {
+		if (check == null) {
+			throw new IllegalArgumentException(
+					"Constructing error location without specification for the following AST node: " + boogieASTNode);
+		}
 		Set<BoogieIcfgLocation> errorNodes = mIcfg.getProcedureErrorNodes().get(procName);
 		final int locNodeNumber;
 		if (errorNodes == null) {
@@ -437,7 +440,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo
 			type = ProcedureErrorType.ASSERT_VIOLATION;
 		} else if (boogieASTNode instanceof EnsuresSpecification) {
 			type = ProcedureErrorType.ENSURES_VIOLATION;
-		} else if (boogieASTNode instanceof RequiresSpecification) {
+		} else if (boogieASTNode instanceof CallStatement) {
 			type = ProcedureErrorType.REQUIRES_VIOLATION;
 		} else if (boogieASTNode instanceof ForkStatement) {
 			type = ProcedureErrorType.INUSE_VIOLATION;
@@ -445,13 +448,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo
 			throw new IllegalArgumentException();
 		}
 
-		final ProcedureErrorDebugIdentifier errorLocLabel;
-		final Check check = Check.getAnnotation(boogieASTNode);
-		if (check == null) {
-			throw new IllegalArgumentException(
-					"Constructing error location without specification for the following AST node: " + boogieASTNode);
-		}
-		errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check);
+		final var errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check);
 		final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode);
 		check.annotate(errorLocNode);
 		procLocNodes.put(errorLocLabel, errorLocNode);
@@ -1028,7 +1025,8 @@ private void assertAndAssumeEnsures() {
 					final Statement st = assumeSt;
 					ModelUtils.copyAnnotations(spec, st);
 					mRcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { spec });
-					final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes);
+					final BoogieIcfgLocation errorLocNode =
+							addErrorNode(mCurrentProcedureName, spec, Check.getAnnotation(spec), mProcLocNodes);
 					final CodeBlock assumeEdge = mCbf.constructStatementSequence(finalNode, errorLocNode, assumeSt);
 					ModelUtils.copyAnnotations(spec, assumeEdge);
 					ModelUtils.copyAnnotations(spec, errorLocNode);
@@ -1255,7 +1253,8 @@ private void processAssertStatement(final AssertStatement st) {
 			final AssumeStatement assumeError = new AssumeStatement(st.getLocation(), getNegation(assertion));
 			ModelUtils.copyAnnotations(st, assumeError);
 			mRcfgBacktranslator.putAux(assumeError, new BoogieASTNode[] { st });
-			final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, st, mProcLocNodes);
+			final BoogieIcfgLocation errorLocNode =
+					addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(st), mProcLocNodes);
 			final StatementSequence assumeErrorCB = mCbf.constructStatementSequence(locNode, errorLocNode, assumeError);
 			ModelUtils.copyAnnotations(st, errorLocNode);
 			ModelUtils.copyAnnotations(st, assumeErrorCB);
@@ -1401,10 +1400,11 @@ private void processCallStatement(final CallStatement st) {
 					final Statement st1 = assumeSt;
 					ModelUtils.copyAnnotations(st, st1);
 					mRcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { st, spec });
-					final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes);
+					final BoogieIcfgLocation errorLocNode =
+							addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(spec), mProcLocNodes);
 					final StatementSequence errorCB = mCbf.constructStatementSequence(locNode, errorLocNode, assumeSt);
 					ModelUtils.copyAnnotations(spec, errorCB);
-					ModelUtils.copyAnnotations(spec, errorLocNode);
+					ModelUtils.copyAnnotationsExcept(spec, errorLocNode, ILocation.class);
 					mEdges.add(errorCB);
 				}
 			}