diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
index 669139a5ea8ea941f92baa78c54e794707a355ec..db600bf51f7bba62adcd95988f5b589ddb7fa068 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
@@ -7,21 +7,11 @@
   Function main
 ------------------------------------------------------------
 
-Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
-Prove: P_P.
-
-------------------------------------------------------------
-
 Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
 Prove: P_P.
 
 ------------------------------------------------------------
 
-Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
-Prove: true.
-
-------------------------------------------------------------
-
 Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
 Prove: true.
 
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 49d002429d51a14be8015a1c892357d9a5f34194..5369d46e449d160f921822ea13e6ca1488681109 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -914,14 +914,13 @@ let get_stmt_annots config v s =
                 in (b_acc, (a_acc, e_acc))
           | TBRok | TBRpart ->
               let id = WpPropId.mk_assert_id config.kf s a in
-              let kind =
-                if kind = Check || Wp_parameters.Assert_check_only.get () then
-                  WpStrategy.Agoal
-                else
-                  WpStrategy.Aboth (goal_to_select config id)
-              in
-              let b_acc = WpStrategy.add_prop_assert b_acc kind kf s a p in
-              (b_acc, (a_acc, e_acc))
+              let check = kind = Check || Wp_parameters.Assert_check_only.get ()
+              and goal = goal_to_select config id in
+              if check && not goal then acc
+              else
+                let kind = WpStrategy.(if check then Agoal else Aboth goal) in
+                let b_acc = WpStrategy.add_prop_assert b_acc kind kf s a p in
+                (b_acc, (a_acc, e_acc))
         in acc
     | AAllocation (_b_list, _frees_allocates) ->
         (* [PB] TODO *) acc
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 9222639296b0f70ef47ae9602868db255f8271bb..bd5be9fa57d460d53a05cfbf15a933803537d46f 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -100,7 +100,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, invariant, variant, breaks, continues, returns.\n\
+                  Accepted categories are: 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