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 92a08d6ee9f..483964d98f9 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
@@ -760,7 +760,7 @@ private IIcfgElement buildCodeBlock(final Statement[] codeblock, final IIcfgElem
 					mRemovedAssumeTrueStatements++;
 					continue;
 				}
-				if (st instanceof final Label laSt && BoogieUtils.isAuxiliaryLabel(laSt)) {
+				if (st instanceof final Label laSt && canLabelBeRemoved(laSt)) {
 					final int gotoTarget = mGotoTargetCounter.getOrDefault(laSt.getName(), 0);
 					if (gotoTarget == 0) {
 						// not target of a goto
@@ -812,6 +812,11 @@ private IIcfgElement buildCodeBlock(final Statement[] codeblock, final IIcfgElem
 			return currentLocation;
 		}
 
+		private boolean canLabelBeRemoved(final Label label) {
+			return mServices.getPreferenceProvider(Activator.PLUGIN_ID).getBoolean(
+					IcfgPreferenceInitializer.LABEL_REMOVE_UNNECESSARY_LABELS) || BoogieUtils.isAuxiliaryLabel(label);
+		}
+
 		private BoogieIcfgLocation buildIf(final BoogieIcfgLocation currentLocation, final IfStatement st) {
 			mConditionalStarts.add(currentLocation);
 			final IIcfgElement thenPart = buildCodeBlock(st.getThenPart(), currentLocation, false);
diff --git a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/preferences/IcfgPreferenceInitializer.java b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/preferences/IcfgPreferenceInitializer.java
index cf7c445c70a..778c5d59f0c 100644
--- a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/preferences/IcfgPreferenceInitializer.java
+++ b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/preferences/IcfgPreferenceInitializer.java
@@ -101,6 +101,10 @@ public boolean isConcurrencySafe() {
 	public static final String LABEL_SIMPLIFY = "Simplify code blocks";
 	public static final String LABEL_CNF = "Convert code blocks to CNF";
 	public static final String LABEL_REMOVE_GOTO_EDGES = "Remove goto edges from ICFG";
+	public static final String LABEL_REMOVE_UNNECESSARY_LABELS = "Remove unnecessary labels from ICFG";
+	private static final String DESC_REMOVE_UNNECESSARY_LABELS =
+			"If this option is enabled, any label that has no corresponding goto, or whose goto appears only on the line preceding the label, is removed and not preserved in the ICFG. "
+					+ "Otherwise, this optimization is only applied for auxiliary labels.";
 	public static final String LABEL_DUMP_TO_FILE = "Dump SMT script to file";
 	public static final String LABEL_COMPRESS_SMT_DUMP_FILE = "Compress dumped SMT script";
 	public static final String DESC_COMPRESS_SMT_DUMP_FILE = "Compress the written .smt2 script with GZip";
@@ -144,6 +148,8 @@ protected UltimatePreferenceItem<?>[] initDefaultPreferences() {
 				new UltimatePreferenceItem<>(LABEL_CONTEXT_SWITCH_ONLY_AT_ATOMIC_BOUNDARIES,
 						DEF_CONTEXT_SWITCH_ONLY_AT_ATOMIC_BOUNDARIES, PreferenceType.Boolean),
 				new UltimatePreferenceItem<>(LABEL_REMOVE_GOTO_EDGES, false, PreferenceType.Boolean),
+				new UltimatePreferenceItem<>(LABEL_REMOVE_UNNECESSARY_LABELS, true, DESC_REMOVE_UNNECESSARY_LABELS,
+						PreferenceType.Boolean),
 				new UltimatePreferenceItem<>(LABEL_SIMPLIFY, false, PreferenceType.Boolean),
 				new UltimatePreferenceItem<>(LABEL_CNF, false, PreferenceType.Boolean),
 				new UltimatePreferenceItem<>(LABEL_SIMPLE_PARTIAL_SKOLEMIZATION, DEF_SIMPLE_PARTIAL_SKOLEMIZATION,