diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index f14ac822df13bea7beb1e46fdd910e7b8932493f..8de5afd5be0067698f497808b689c7978e04f453 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -295,7 +295,7 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
       type data = code_assertions
       let name = "Wp.CfgAnnot.CodeAssertions"
       let compile (kf,stmt) =
-        let labels = NormAtLabels.labels_assert_before ~kf stmt in
+        let labels = NormAtLabels.labels_assert ~kf stmt in
         let normalize_pred p = NormAtLabels.preproc_annot labels p in
         reverse_code_assertions @@
         Annotations.fold_code_annot
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 7a52640077ea898513a7e1774385950d989e2642..0f6ebe895ab54d2ea76d543246f7bad6e1b9ca07 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -181,15 +181,10 @@ let labels_stmt_assigns_l ~kf s l_post = function
 (* --- User Assertions in Functions Code                                  --- *)
 (* -------------------------------------------------------------------------- *)
 
-let labels_assert_before ~kf s = function
+let labels_assert ~kf s = function
   | BuiltinLabel Here -> Clabels.stmt s
   | l -> labels_fct ~kf ~at:s l
 
-let labels_assert_after ~kf s l_post = function
-  | BuiltinLabel Old -> Clabels.stmt s
-  | BuiltinLabel Here as l -> option l l_post
-  | l -> labels_fct ~kf ~at:s l
-
 let labels_loop s = function
   (* In invariant preservation/establishment, LoopCurrent is Here. *)
   | BuiltinLabel (Here | LoopCurrent) -> Clabels.here
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index 2becd6c715a6c6438479c4567241e5bdc8438b31..affd569c595489fb3b8237662e69e0fb6e0d55fa 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -32,8 +32,7 @@ val labels_empty : label_mapping
 val labels_fct_pre : label_mapping
 val labels_fct_post : label_mapping
 val labels_fct_assigns : label_mapping
-val labels_assert_before : kf:kernel_function -> stmt -> label_mapping
-val labels_assert_after : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_assert : kf:kernel_function -> stmt -> label_mapping
 val labels_loop : stmt -> label_mapping
 val labels_stmt_pre : kf:kernel_function -> stmt -> label_mapping
 val labels_stmt_post : kf:kernel_function -> stmt -> label_mapping
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 420016431a7b9c76333f8c1e6c75186e81181ca6..1166868e973159697c0ccd4e3e31b0ea514f4814 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -268,7 +268,7 @@ let add_prop_call_post acc kind called_kf bhv tkind ~assumes post =
 
 let add_prop_assert acc kind kf s ca p =
   let id = WpPropId.mk_assert_id kf s ca in
-  let labels = NormAtLabels.labels_assert_before ~kf s in
+  let labels = NormAtLabels.labels_assert ~kf s in
   let p = normalize id labels p in
   add_prop acc kind id p