diff --git a/trunk/examples/programs/regression/bpl/toolDirectives/LabelsWithAttributes.bpl b/trunk/examples/programs/regression/bpl/toolDirectives/LabelsWithAttributes.bpl
new file mode 100644
index 00000000000..4efcbd269df
--- /dev/null
+++ b/trunk/examples/programs/regression/bpl/toolDirectives/LabelsWithAttributes.bpl
@@ -0,0 +1,18 @@
+//#Safe
+// Author: 	matthias.heizmann@iste.uni-stuttgart.de
+// Date: 2025-01-03
+//
+// Test for our Boogie extension that allows labels to have attributes.
+
+procedure proc() returns ()
+modifies;
+{
+  var x : int;
+  assume x == 0;
+  MyLabel  { :keyA "valueA1", "valueA2"} { :auxiliary_label true} { :keyB "valueB"} :
+  assert(x == 0);
+
+}
+
+
+
diff --git a/trunk/source/BoogiePLParser/src/de/uni_freiburg/informatik/ultimate/boogie/parser/Boogie.cup b/trunk/source/BoogiePLParser/src/de/uni_freiburg/informatik/ultimate/boogie/parser/Boogie.cup
index 9e7707e233d..21c01da49b1 100644
--- a/trunk/source/BoogiePLParser/src/de/uni_freiburg/informatik/ultimate/boogie/parser/Boogie.cup
+++ b/trunk/source/BoogiePLParser/src/de/uni_freiburg/informatik/ultimate/boogie/parser/Boogie.cup
@@ -701,8 +701,8 @@ stmtList ::=
     //| stmtList:l error {: RESULT = l; :}
 	;
 stmt ::=
-	  ID:i COLON
-	  {: RESULT = new Label(getLocation(i$,i$), i); :}
+	  ID:i attributes:attr COLON
+	  {: RESULT = new Label(getLocation(i$,i$), i, attr); :}
 	| ASSERT:x attributes:attr expr:e SEMI
 	  {: RESULT = new AssertStatement(getLocation(x$,e$), attr, e); Check check = createCheck(RESULT); check.annotate(RESULT); :}
 	| ASSUME:x attributes:attr expr:e SEMI
diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/Boogie.ast b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/Boogie.ast
index eff5bfa821c..d23c703b8b4 100644
--- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/Boogie.ast
+++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/ast/Boogie.ast
@@ -388,6 +388,7 @@ Statement ::=
 	   */
 	  Label }
 		name    : String
+	    attributes : ?NamedAttribute[]
 	| { /**
 	     * Assert that a boolean formula holds.  Program will terminate
 	     * with an error if it does not.