diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 7f362c7148689ecbbdda1696585c2a3fd53b0e65..536b85c8130af21403546343899c6cef9c6febc9 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
 #   <Prover>: prover
 ###############################################################################
 
+- Wp          [2020-09-09] Support for generalized @check ACSL annotations
+
 #########################
 Plugin WP <next-release>
 #########################
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
index 1a1174504f7e46923c594d5f5d11049ad5fdd1f0..f3fdcbfcab8f623e1c5393ae7e7b4b977300a6c2 100644
--- a/src/plugins/wp/tests/wp_acsl/checks.i
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -1,7 +1,7 @@
 /* run.config
    OPT: -eva -load-module scope,eva,report -then -report
    OPT: -wp-prop=@check
-   OPT: -wp-prop=@assert
+   OPT: -wp-prop=-@check
 */
 /* run.config_qualif
    OPT: -load-module report -wp-steps 5 -then -report
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 77400497f4deca5243047a1f6d89a0ada9dbc593..4858d59ff064165d03b16879580ad7d93f8cc400 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -465,12 +465,13 @@ let ident_names names =
   List.filter (function "" -> true
                       | _ as n -> '\"' <> (String.get n 0) ) names
 
+let pred_names p =
+  let p_names = ident_names p.tp_statement.pred_name in
+  if p.tp_only_check then "@check"::p_names else p_names
+
 let code_annot_names ca = match ca.annot_content with
-  | AAssert (_, pred)  ->
-      let cat = if pred.tp_only_check then "@check" else "@assert" in
-      cat::(ident_names pred.tp_statement.pred_name)
-  | AInvariant (_,_,named_pred) ->
-      "@invariant"::(ident_names named_pred.tp_statement.pred_name)
+  | AAssert (_, pred)  -> "@assert" :: pred_names pred
+  | AInvariant (_,_,pred) -> "@invariant":: pred_names pred
   | AVariant (term, _) -> "@variant"::(ident_names term.term_name)
   | AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
   | _ -> [] (* TODO : add some more names ? *)
@@ -481,7 +482,7 @@ let user_prop_names p =
   let open Property in match p with
   | IPPredicate {ip_kind; ip_pred} ->
       Format.asprintf  "@@%a" Property.pretty_predicate_kind ip_kind ::
-      ip_pred.ip_content.tp_statement.pred_name
+      pred_names ip_pred.ip_content
   | IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
   | IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
   | IPComplete {ic_bhvs} ->
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 448ff335f59df0604294f560f9f87b957e69a5ae..c37830d4ebbeb1a452a31fcb5caba4890efd98b9 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -98,7 +98,7 @@ module Properties =
       let arg_name = "p,..."
       let help = "Select properties having the one of the given tagnames (defaults to all properties).\n\
                   You may also replace the tagname by '@category' for the selection of all properties of the given category.\n\
-                  Accepted categories are: lemmas, requires, assigns, ensures, exits, complete_behaviors, disjoint_behaviors, assert, check, invariant, variant, breaks, continues, returns.\n\
+                  Accepted categories are: checks, lemmas, requires, assigns, ensures, exits, complete_behaviors, disjoint_behaviors, assert, check, invariant, variant, breaks, continues, returns.\n\
                   Starts by a minus character to remove properties from the selection."
     end)
 let () = on_reset Properties.clear