diff --git a/framaCIRGen_src/ACSLTermOrPredicate.cpp b/framaCIRGen_src/ACSLTermOrPredicate.cpp
index c9dabbdc3f00d93d6f2b3b67765b4c0b59d72729..a6cf4d80618e82ad2e544ebd22ffedf3a4261851 100644
--- a/framaCIRGen_src/ACSLTermOrPredicate.cpp
+++ b/framaCIRGen_src/ACSLTermOrPredicate.cpp
@@ -3995,31 +3995,26 @@ TermOrPredicate::apply(Operator& operation, logic_type& ltypeResult,
             operation._startLocation, ltypeResult, context);
         operation._startLocation = NULL;
         return true;
-      case Operator::TNaming:
+      case Operator::TNaming: {
         // add naming to the local alias table;
         assert(operation._startLocation);
         free_location(operation._startLocation);
         operation._startLocation = NULL;
-        { list *endTermNames = NULL, *endPredicateNames = NULL;
-          if (targument) {
-            endTermNames = &targument->names;
-            while (*endTermNames)
-              endTermNames= &(*endTermNames)->next;
-            *endTermNames = cons_container(strdup(operation._fieldName.c_str()),
-                NULL);
-            ltypeResult = ltypeArgument;
-            expressionResult = targument;
-          };
-          if (pargument) {
-            endPredicateNames = &pargument->pred_name;
-            while (*endPredicateNames)
-              endPredicateNames= &(*endPredicateNames)->next;
-            *endPredicateNames = cons_container(strdup(
-                  operation._fieldName.c_str()), NULL);
+        if (targument) {
+          targument->names =
+            cons_container(strdup(operation._fieldName.c_str()),
+                           targument->names);
+          ltypeResult = ltypeArgument;
+          expressionResult = targument;
+        };
+        if (pargument) {
+          pargument->pred_name =
+            cons_container(strdup(operation._fieldName.c_str()),
+                           pargument->pred_name);
             predicateResult = pargument;
-          };
         };
         return true;
+      }
       case Operator::TStructAccess:
         if (!targument) {
           if (pargument) {
diff --git a/tests/basic/oracle/cxx_c_link.res.oracle b/tests/basic/oracle/cxx_c_link.res.oracle
index 7cb7c04d1ea3bbc0efaa3416541bed6a95a2ed7c..7c3e5ae806e003a0c81ca213acdd852d6abcc7b1 100644
--- a/tests/basic/oracle/cxx_c_link.res.oracle
+++ b/tests/basic/oracle/cxx_c_link.res.oracle
@@ -1,16 +1,10 @@
 [kernel] Parsing cxx_c_link.cpp (external front-end)
 Now output intermediate result
 [kernel] Parsing cxx_c_link.c (with preprocessing)
-[kernel] FRAMAC_SHARE/libc/stdlib.h:307: Warning: 
-  found two contracts. Merging them
 [kernel] FRAMAC_SHARE/libc/stdlib.h:322: Warning: 
   found two contracts. Merging them
 [kernel] FRAMAC_SHARE/libc/stdlib.h:330: Warning: 
   found two contracts. Merging them
-[kernel] FRAMAC_SHARE/libc/stdlib.h:346: Warning: 
-  found two contracts. Merging them
-[kernel] FRAMAC_SHARE/libc/stdlib.h:362: Warning: 
-  found two contracts. Merging them
 [kernel] FRAMAC_SHARE/libc/stdlib.h:724: Warning: 
   found two contracts. Merging them
 /* Generated by Frama-C */
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 5a867c54b45248cf9b808f3c975fe18db44ff34c..8e785619e41f3c46faab9b3b5e597dacf448fadb 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -701,7 +701,7 @@ unsigned short *__fc_p_random48_counter = __fc_random48_counter;
 void srand48(long seed);
 
 /*@ requires
-      initialized_seed16v: initialization: \initialized(seed16v + (0 .. 2));
+      initialization: initialized_seed16v: \initialized(seed16v + (0 .. 2));
     ensures random48_initialized: __fc_random48_init ≡ 1;
     ensures result_counter: \result ≡ __fc_p_random48_counter;
     assigns __fc_random48_counter[0 .. 2], __fc_random48_init, \result;
@@ -729,7 +729,7 @@ void lcong48(unsigned short param[7]);
 double drand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -748,7 +748,7 @@ double erand48(unsigned short xsubi[3]);
 long lrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: 0 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -767,7 +767,7 @@ long nrand48(unsigned short xsubi[3]);
 long mrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: -2147483648 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index 0381b308a216891d49dece2753e69bda7a950d52..af841f06fa63c5980ce77f2925d0adc9c8e1b3b8 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -670,7 +670,7 @@ unsigned short *__fc_p_random48_counter = __fc_random48_counter;
 void srand48(long seed);
 
 /*@ requires
-      initialized_seed16v: initialization: \initialized(seed16v + (0 .. 2));
+      initialization: initialized_seed16v: \initialized(seed16v + (0 .. 2));
     ensures random48_initialized: __fc_random48_init ≡ 1;
     ensures result_counter: \result ≡ __fc_p_random48_counter;
     assigns __fc_random48_counter[0 .. 2], __fc_random48_init, \result;
@@ -698,7 +698,7 @@ void lcong48(unsigned short param[7]);
 double drand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -717,7 +717,7 @@ double erand48(unsigned short xsubi[3]);
 long lrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: 0 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -736,7 +736,7 @@ long nrand48(unsigned short xsubi[3]);
 long mrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: -2147483648 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 7e61ad04a5442c8a7fb5e758fdf27f6fd271100d..14b3aa84e4abf55e34ea7ffabfaccceb26d16342 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -851,10 +851,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -1218,7 +1218,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1333,7 +1333,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1484,7 +1484,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
diff --git a/tests/stl/oracle/stl_bool.res.oracle b/tests/stl/oracle/stl_bool.res.oracle
index 61002813387a72e0a79d7c3fbc1d82aa5b826889..5a2dfc20ffe2fbada62b3c1985ac4a1aff258ad2 100644
--- a/tests/stl/oracle/stl_bool.res.oracle
+++ b/tests/stl/oracle/stl_bool.res.oracle
@@ -499,10 +499,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -866,7 +866,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -981,7 +981,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1132,7 +1132,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 808567140531a83f5d1ae33c359665c5a26f3668..9549fe96fbd4ea17f1dbfc551a67484af5cafe5a 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -659,10 +659,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -1026,7 +1026,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1141,7 +1141,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1292,7 +1292,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index 7ea60a5bba2aa863c36af8a8b8e0fcaf4fc703ed..1c1723c90d58e8a138784635ffdb9dfd46975c3e 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -665,10 +665,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -1032,7 +1032,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1147,7 +1147,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1298,7 +1298,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 47f02582bcf14421ea7d1ce9144b05fc47b161c5..e3995e5325a07bd0570ddacd3d4f292d0fd43c1c 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -680,10 +680,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -1047,7 +1047,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1162,7 +1162,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1313,7 +1313,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
@@ -2797,7 +2797,7 @@ unsigned short *__fc_p_random48_counter = __fc_random48_counter;
 void srand48(long seed);
 
 /*@ requires
-      initialized_seed16v: initialization: \initialized(seed16v + (0 .. 2));
+      initialization: initialized_seed16v: \initialized(seed16v + (0 .. 2));
     ensures random48_initialized: __fc_random48_init ≡ 1;
     ensures result_counter: \result ≡ __fc_p_random48_counter;
     assigns __fc_random48_counter[0 .. 2], __fc_random48_init, \result;
@@ -2825,7 +2825,7 @@ void lcong48(unsigned short param[7]);
 double drand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -2844,7 +2844,7 @@ double erand48(unsigned short xsubi[3]);
 long lrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: 0 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -2863,7 +2863,7 @@ long nrand48(unsigned short xsubi[3]);
 long mrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: -2147483648 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index aa64cb41fc115e0051733e86ebb2ef4c92d387d5..3ae6bb2e7d56a3472704bda3c8c0d331aec754e9 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -661,10 +661,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -1028,7 +1028,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1143,7 +1143,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1294,7 +1294,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
@@ -2576,7 +2576,7 @@ unsigned short *__fc_p_random48_counter = __fc_random48_counter;
 void srand48(long seed);
 
 /*@ requires
-      initialized_seed16v: initialization: \initialized(seed16v + (0 .. 2));
+      initialization: initialized_seed16v: \initialized(seed16v + (0 .. 2));
     ensures random48_initialized: __fc_random48_init ≡ 1;
     ensures result_counter: \result ≡ __fc_p_random48_counter;
     assigns __fc_random48_counter[0 .. 2], __fc_random48_init, \result;
@@ -2604,7 +2604,7 @@ void lcong48(unsigned short param[7]);
 double drand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -2623,7 +2623,7 @@ double erand48(unsigned short xsubi[3]);
 long lrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: 0 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -2642,7 +2642,7 @@ long nrand48(unsigned short xsubi[3]);
 long mrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: -2147483648 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index f49a004e298e60c5a4cac524915ed1c510515d9c..023110e6eff45e3285659dde04035016c7862895 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -662,10 +662,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -1029,7 +1029,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1144,7 +1144,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1295,7 +1295,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
@@ -2582,7 +2582,7 @@ unsigned short *__fc_p_random48_counter = __fc_random48_counter;
 void srand48(long seed);
 
 /*@ requires
-      initialized_seed16v: initialization: \initialized(seed16v + (0 .. 2));
+      initialization: initialized_seed16v: \initialized(seed16v + (0 .. 2));
     ensures random48_initialized: __fc_random48_init ≡ 1;
     ensures result_counter: \result ≡ __fc_p_random48_counter;
     assigns __fc_random48_counter[0 .. 2], __fc_random48_init, \result;
@@ -2610,7 +2610,7 @@ void lcong48(unsigned short param[7]);
 double drand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -2629,7 +2629,7 @@ double erand48(unsigned short xsubi[3]);
 long lrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: 0 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
@@ -2648,7 +2648,7 @@ long nrand48(unsigned short xsubi[3]);
 long mrand48(void);
 
 /*@ requires
-      initialized_xsubi: initialization: \initialized(xsubi + (0 .. 2));
+      initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
     ensures result_range: -2147483648 ≤ \result < 2147483648;
     assigns __fc_random48_counter[0 .. 2], \result;
     assigns __fc_random48_counter[0 .. 2]
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 254c8a96ee02890fca28d6524db1442384e28a73..27e8e63f101cc88d7d2714d1c8ca1db1f7599704 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -576,10 +576,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
  */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -943,7 +943,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1058,7 +1058,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1209,7 +1209,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
@@ -1598,7 +1598,7 @@ void (*signal(int sig, void (*func)(int )))(int );
 int raise(int sig);
 
 /*@ requires valid_set: \valid(set);
-    ensures set: initialization: \initialized(\old(set));
+    ensures initialization: set: \initialized(\old(set));
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns *set, \result;
     assigns *set \from \nothing;
@@ -1607,7 +1607,7 @@ int raise(int sig);
 int sigemptyset(sigset_t *set);
 
 /*@ requires valid_set: \valid(set);
-    ensures set: initialization: \initialized(\old(set));
+    ensures initialization: set: \initialized(\old(set));
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns *set, \result;
     assigns *set \from \nothing;
@@ -1616,7 +1616,7 @@ int sigemptyset(sigset_t *set);
 int sigfillset(sigset_t *set);
 
 /*@ requires valid_set: \valid(set);
-    requires set: initialization: \initialized(set);
+    requires initialization: set: \initialized(set);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns *set, \result;
     assigns *set \from (indirect: signum);
@@ -1625,7 +1625,7 @@ int sigfillset(sigset_t *set);
 int sigaddset(sigset_t *set, int signum);
 
 /*@ requires valid_set: \valid(set);
-    requires set: initialization: \initialized(set);
+    requires initialization: set: \initialized(set);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns *set, \result;
     assigns *set \from (indirect: signum);
@@ -1634,7 +1634,7 @@ int sigaddset(sigset_t *set, int signum);
 int sigdelset(sigset_t *set, int signum);
 
 /*@ requires valid_read_set: \valid_read(set);
-    requires set: initialization: \initialized(set);
+    requires initialization: set: \initialized(set);
     ensures
       result_found_not_found_or_error:
         \result ≡ 0 ∨ \result ≡ 1 ∨ \result ≡ -1;
@@ -1648,7 +1648,7 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
 /*@ requires valid_signal: 0 ≤ signum ≤ 64;
     requires valid_oldact_or_null: oldact ≡ \null ∨ \valid(oldact);
     requires valid_read_act_or_null: act ≡ \null ∨ \valid_read(act);
-    requires separated_acts: separation: \separated(act, oldact);
+    requires separation: separated_acts: \separated(act, oldact);
     ensures
       act_changed:
         \old(act) ≡ \null ∨
@@ -1723,7 +1723,7 @@ time_t mktime(struct tm *timeptr);
     behavior not_null:
       assumes timer_non_null: timer ≢ \null;
       requires valid_timer: \valid(timer);
-      ensures timer: initialization: \initialized(\old(timer));
+      ensures initialization: timer: \initialized(\old(timer));
       assigns *timer, \result;
       assigns *timer \from __fc_time;
       assigns \result \from __fc_time;
@@ -1736,7 +1736,7 @@ time_t time(time_t *timer);
 char __fc_ctime[26];
 char * const __fc_p_ctime = __fc_ctime;
 /*@ requires valid_timeptr: \valid_read(timeptr);
-    requires init_timeptr: initialization: \initialized(timeptr);
+    requires initialization: init_timeptr: \initialized(timeptr);
     ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
     ensures result_valid_string: valid_read_string(__fc_p_ctime);
     assigns __fc_ctime[0 .. 25], \result;
@@ -1748,7 +1748,7 @@ char * const __fc_p_ctime = __fc_ctime;
 char *asctime(struct tm const *timeptr);
 
 /*@ requires valid_timer: \valid_read(timer);
-    requires init_timer: initialization: \initialized(timer);
+    requires initialization: init_timer: \initialized(timer);
     ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
     ensures result_valid_string: valid_read_string(__fc_p_ctime);
     assigns __fc_ctime[0 .. 25], \result;
@@ -1846,7 +1846,7 @@ axiomatic nanosleep_predicates {
 /*@ ghost int volatile __fc_interrupted; */
 /*@ requires valid_request: \valid_read(rqtp);
     requires
-      initialized_request: initialization:
+      initialization: initialized_request:
         \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
     requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
     requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
@@ -1876,7 +1876,7 @@ axiomatic nanosleep_predicates {
       assumes no_einval: valid_clock_id(clock_id);
       ensures result_interrupted: \result ≡ 4;
       ensures
-        interrupted_remaining: initialization:
+        initialization: interrupted_remaining:
           \old(rmtp) ≢ \null ⇒
           \initialized(&\old(rmtp)->tv_sec) ∧
           \initialized(&\old(rmtp)->tv_nsec);
@@ -1942,7 +1942,7 @@ struct tm *gmtime_r(time_t const * restrict timer,
 /*@ requires valid_timer: \valid_read(timep);
     requires valid_result: \valid(result);
     ensures
-      initialization: result_null_or_initialized:
+      result_null_or_initialized: initialization:
         (\result ≡ \old(result) ∧ \initialized(\old(result))) ∨
         \result ≡ \null;
     ensures
@@ -1957,13 +1957,13 @@ struct tm *localtime_r(time_t const * restrict timep,
 
 /*@ requires valid_request: \valid_read(rqtp);
     requires
-      initialized_request: initialization:
+      initialization: initialized_request:
         \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
     requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
     requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
     ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1;
     ensures
-      interrupted_remaining: initialization:
+      initialization: interrupted_remaining:
         \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
         \initialized(&\old(rmtp)->tv_sec) ∧
         \initialized(&\old(rmtp)->tv_nsec);
@@ -2006,7 +2006,7 @@ wchar_t *wmemmove(wchar_t *dest, wchar_t const *src, size_t n);
 /*@ requires valid_wcs: \valid(wcs + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(wcs);
     ensures
-      wcs: initialization: \initialized(\old(wcs) + (0 .. \old(n) - 1));
+      initialization: wcs: \initialized(\old(wcs) + (0 .. \old(n) - 1));
     ensures
       contents_equal_wc: \subset(*(\old(wcs) + (0 .. \old(n) - 1)), \old(wc));
     assigns *(wcs + (0 .. n - 1)), \result;
@@ -2096,7 +2096,7 @@ size_t wcslcat(wchar_t * restrict dest, wchar_t const * restrict src,
 /*@ requires valid_wstring_src: valid_read_wstring(src);
     requires room_nwstring: \valid(dest + (0 .. n));
     requires
-      src: dest: separation:
+      separation: dest: src:
         \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     assigns *(dest + (0 .. n - 1)), \result;
     assigns *(dest + (0 .. n - 1))
@@ -2146,7 +2146,7 @@ int wcsncmp(wchar_t const *s1, wchar_t const *s2, size_t n);
 /*@ requires valid_wstring_src: valid_read_wstring(src);
     requires room_nwstring: \valid(dest + (0 .. n - 1));
     requires
-      src: dest: separation:
+      separation: dest: src:
         \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
     ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index 794d54df739ae7c8a89aa3b52f0c96a1920357bf..cb9575f6bac93915b3070303f9dcfb6ae9950c90 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -434,10 +434,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
  */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -801,7 +801,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -916,7 +916,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1067,7 +1067,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
diff --git a/tests/stl/oracle/stl_unique_ptr.res.oracle b/tests/stl/oracle/stl_unique_ptr.res.oracle
index 6a55ee95a6b63b476cf90b9338088c9b11524381..b5c6d61ca3ee000c47007bb4fdb8206fa9c6cf0b 100644
--- a/tests/stl/oracle/stl_unique_ptr.res.oracle
+++ b/tests/stl/oracle/stl_unique_ptr.res.oracle
@@ -1158,10 +1158,10 @@ predicate valid_read_or_empty{L}(void *s, size_t n) =
 */
 /*@ requires valid_s1: valid_read_or_empty(s1, n);
     requires valid_s2: valid_read_or_empty(s2, n);
-    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
-    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
-    requires s1: danglingness: non_escaping(s1, n);
-    requires s2: danglingness: non_escaping(s2, n);
+    requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+    requires danglingness: s1: non_escaping(s1, n);
+    requires danglingness: s2: non_escaping(s2, n);
     ensures
       logic_spec:
         \result ≡
@@ -1525,7 +1525,7 @@ char *strtok(char * restrict s, char const * restrict delim);
     behavior resume_str:
       assumes s_null: s ≡ \null;
       requires not_first_call: *saveptr ≢ \null;
-      requires saveptr: initialization: \initialized(saveptr);
+      requires initialization: saveptr: \initialized(saveptr);
       ensures
         result_subset:
           \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
@@ -1640,7 +1640,7 @@ char *stpcpy(char * restrict dest, char const * restrict src);
     ensures
       sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
     ensures
-      dest: initialization:
+      initialization: dest:
         \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
     ensures
       dest_null_terminated:
@@ -1791,7 +1791,7 @@ char *strsignal(int signum);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
     ensures
-      initialization: s_initialized:
+      s_initialized: initialization:
         \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});