diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 3535467b5136d9c797a4b0236b18bd54bd202a00..49d002429d51a14be8015a1c892357d9a5f34194 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -902,18 +902,20 @@ let get_stmt_annots config v s =
               Printer.pp_code_annotation a;
             acc
           end
-    | AAssert (b_list,_,p) ->
+    | AAssert (b_list, kind, p) ->
         let kf = config.kf in
         let acc = match is_annot_for_config config v s b_list with
           | TBRno -> acc
           | TBRhyp ->
-              let b_acc =
-                WpStrategy.add_prop_assert b_acc WpStrategy.Ahyp kf s a p
-              in (b_acc, (a_acc, e_acc))
+              if kind = Check then acc
+              else
+                let b_acc =
+                  WpStrategy.add_prop_assert b_acc WpStrategy.Ahyp kf s a p
+                in (b_acc, (a_acc, e_acc))
           | TBRok | TBRpart ->
               let id = WpPropId.mk_assert_id config.kf s a in
               let kind =
-                if Wp_parameters.Assert_check_only.get () then
+                if kind = Check || Wp_parameters.Assert_check_only.get () then
                   WpStrategy.Agoal
                 else
                   WpStrategy.Aboth (goal_to_select config id)