diff --git a/tests/syntax/clabels_builtin_labels.c b/tests/syntax/clabels_builtin_labels.c
index 4295c77cec8efc7ebf28793330c35b2256e3172f..b7c98b2cbd0cf59dec64b00f2e235d637180ddb3 100644
--- a/tests/syntax/clabels_builtin_labels.c
+++ b/tests/syntax/clabels_builtin_labels.c
@@ -1,6 +1,6 @@
 int x;
 
-void named(void){
+void named_1(void){
   x = 4;
 Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: A:;
   x = 5;
@@ -10,27 +10,22 @@ Z: T: ;
   x = 7;
 }
 
-void post_over_old_1(void){ Old: Post: ;}
-void post_over_old_2(void){ Post: Old: ;}
-
-void post_over_loop_1(void){ LoopEntry: Post: ;}
-void post_over_loop_2(void){ Post: LoopCurrent: ;}
-
-void post_over_other_1(void){ Here: Post: ;}
-void post_over_other_2(void){ Post: Pre: ;}
-void post_over_other_3(void){ Init: Post: Pre: ;}
-
-void old_over_loop_1(void){ LoopEntry: Old: ;}
-void old_over_loop_2(void){ Old: LoopCurrent: ;}
-
-void old_over_other_1(void){ Here: Old: ;}
-void old_over_other_2(void){ Old: Pre: ;}
-void old_over_other_3(void){ Init: Old: Pre: ;}
-
-void loop_over_other_1(void){ Here: LoopEntry: ;}
-void loop_over_other_2(void){ LoopCurrent: Pre: ;}
-void loop_over_other_3(void){ Init: LoopEntry: Pre: ;}
+void named_2(void){
+  x = 4;
+A: Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: ;
+  x = 5;
+X: Y: ;
+  x = 6;
+Z: T: ;
+  x = 7;
+}
 
-void arbitray_other_1(void){ Here: Init: ;}
-void arbitray_other_2(void){ Init: Pre: ;}
-void arbitray_other_3(void){ Pre: Here: Init: ;}
+void named_3(void){
+  x = 4;
+Init: Pre: Old: Post: A: Here: LoopCurrent: LoopEntry: ;
+  x = 5;
+X: Y: ;
+  x = 6;
+Z: T: ;
+  x = 7;
+}
diff --git a/tests/syntax/oracle/clabels_builtin_labels.res.oracle b/tests/syntax/oracle/clabels_builtin_labels.res.oracle
index 3e0bd22e2d19be51f03b77e8264b1681de0fc760..822f8f7853cb2a3dcc2fcac07e9d86b76864b5e6 100644
--- a/tests/syntax/oracle/clabels_builtin_labels.res.oracle
+++ b/tests/syntax/oracle/clabels_builtin_labels.res.oracle
@@ -13,89 +13,37 @@
   LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
 [kernel] clabels_builtin_labels.c:5: Warning: 
   LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:13: Warning: 
-  Old is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:13: Warning: 
-  Post is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:14: Warning: 
-  Post is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:14: Warning: 
-  Old is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:16: Warning: 
-  LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:16: Warning: 
-  Post is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:17: Warning: 
-  Post is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:17: Warning: 
-  LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:19: Warning: 
-  Here is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:19: Warning: 
-  Post is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:20: Warning: 
-  Post is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:20: Warning: 
-  Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:21: Warning: 
+[kernel] clabels_builtin_labels.c:15: Warning: 
   Init is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:21: Warning: 
-  Post is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:21: Warning: 
+[kernel] clabels_builtin_labels.c:15: Warning: 
   Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:23: Warning: 
-  LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:23: Warning: 
-  Old is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:24: Warning: 
+[kernel] clabels_builtin_labels.c:15: Warning: 
   Old is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:24: Warning: 
-  LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:26: Warning: 
-  Here is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:26: Warning: 
-  Old is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:27: Warning: 
-  Old is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:27: Warning: 
-  Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:28: Warning: 
-  Init is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:28: Warning: 
-  Old is a builtin ACSL label, this C label is hidden in contracts
-[kernel] clabels_builtin_labels.c:28: Warning: 
-  Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:30: Warning: 
+[kernel] clabels_builtin_labels.c:15: Warning: 
+  Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:15: Warning: 
   Here is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:30: Warning: 
-  LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:31: Warning: 
+[kernel] clabels_builtin_labels.c:15: Warning: 
   LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:31: Warning: 
-  Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:32: Warning: 
-  Init is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:32: Warning: 
+[kernel] clabels_builtin_labels.c:15: Warning: 
   LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
-[kernel] clabels_builtin_labels.c:32: Warning: 
-  Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:34: Warning: 
-  Here is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:34: Warning: 
+[kernel] clabels_builtin_labels.c:25: Warning: 
   Init is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:35: Warning: 
-  Init is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:35: Warning: 
-  Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:36: Warning: 
+[kernel] clabels_builtin_labels.c:25: Warning: 
   Pre is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:36: Warning: 
+[kernel] clabels_builtin_labels.c:25: Warning: 
+  Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:25: Warning: 
+  Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:25: Warning: 
   Here is a builtin ACSL label, this C label is hidden in annotations
-[kernel] clabels_builtin_labels.c:36: Warning: 
-  Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:25: Warning: 
+  LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:25: Warning: 
+  LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
 /* Generated by Frama-C */
 int x;
-void named(void)
+void named_1(void)
 {
   x = 4;
   A: ;
@@ -107,111 +55,27 @@ void named(void)
   return;
 }
 
-void post_over_old_1(void)
-{
-  __fc_user_label_Old: ;
-  return;
-}
-
-void post_over_old_2(void)
-{
-  __fc_user_label_Post: ;
-  return;
-}
-
-void post_over_loop_1(void)
-{
-  __fc_user_label_LoopEntry: ;
-  return;
-}
-
-void post_over_loop_2(void)
-{
-  __fc_user_label_Post: ;
-  return;
-}
-
-void post_over_other_1(void)
-{
-  __fc_user_label_Here: ;
-  return;
-}
-
-void post_over_other_2(void)
-{
-  __fc_user_label_Post: ;
-  return;
-}
-
-void post_over_other_3(void)
-{
-  __fc_user_label_Init: ;
-  return;
-}
-
-void old_over_loop_1(void)
-{
-  __fc_user_label_LoopEntry: ;
-  return;
-}
-
-void old_over_loop_2(void)
-{
-  __fc_user_label_Old: ;
-  return;
-}
-
-void old_over_other_1(void)
+void named_2(void)
 {
-  __fc_user_label_Here: ;
-  return;
-}
-
-void old_over_other_2(void)
-{
-  __fc_user_label_Old: ;
-  return;
-}
-
-void old_over_other_3(void)
-{
-  __fc_user_label_Init: ;
-  return;
-}
-
-void loop_over_other_1(void)
-{
-  __fc_user_label_Here: ;
-  return;
-}
-
-void loop_over_other_2(void)
-{
-  __fc_user_label_LoopCurrent: ;
-  return;
-}
-
-void loop_over_other_3(void)
-{
-  __fc_user_label_Init: ;
-  return;
-}
-
-void arbitray_other_1(void)
-{
-  __fc_user_label_Here: ;
-  return;
-}
-
-void arbitray_other_2(void)
-{
-  __fc_user_label_Init: ;
+  x = 4;
+  A: ;
+  x = 5;
+  X: ;
+  x = 6;
+  Z: ;
+  x = 7;
   return;
 }
 
-void arbitray_other_3(void)
+void named_3(void)
 {
-  __fc_user_label_Pre: ;
+  x = 4;
+  A: ;
+  x = 5;
+  X: ;
+  x = 6;
+  Z: ;
+  x = 7;
   return;
 }