diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index c2190cc487b228a0cd82d9aa6db817033c1915ed..2629c793465eccb13baf84119b38d7b63a874099 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -75,9 +75,9 @@ let normalize_pre ~goal kf bhv ?assumes ip =
     let module L = NormAtLabels in
     let labels = L.labels_fct_pre in
     let id = WpPropId.mk_pre_id kf Kglobal bhv ip in
-    let p = L.preproc_annot labels ip.ip_content.tp_statement in
+    let pre = ip.ip_content.tp_statement in
     let assumes = Option.map normalize_assumes assumes in
-    Some (id, implies ?assumes p)
+    Some (id, L.preproc_annot labels @@ implies ?assumes pre)
   else None
 
 let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =