diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index da2f5d78db1ffb994455b28316fda97ad7debe28..c20fbae10bf92f26c788a3b839a34a9b3183dd0a 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -420,7 +420,8 @@ let ident_names names =
                       | _ as n -> '\"' <> (String.get n 0) ) names
 
 let code_annot_names ca = match ca.annot_content with
-  | AAssert (_, _, named_pred)  -> "@assert"::(ident_names named_pred.pred_name)
+  | AAssert (_, Check, named_pred)  -> "@check"::(ident_names named_pred.pred_name)
+  | AAssert (_, Assert, named_pred)  -> "@assert"::(ident_names named_pred.pred_name)
   | AInvariant (_,_,named_pred) -> "@invariant"::(ident_names named_pred.pred_name)
   | AVariant (term, _) -> "@variant"::(ident_names term.term_name)
   | AExtended(_,_,(_,name,_,_,_)) -> [Printf.sprintf "@%s" name]