diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index b679aebcbff8d0a2280eb5a95afe40e6f0824ba0..382b516da8f38c7a6e99a88a0fc2632f23f32a09 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -92,7 +92,13 @@ let selected_name ~prop name =
 
 let selected_assigns ~prop = function
   | Cil_types.WritesAny -> false
-  | _ -> selected_name ~prop "@assigns"
+  | Writes _ when prop = [] -> true
+  | Writes l ->
+    let collect_names l (t, _) =
+      WpPropId.ident_names t.Cil_types.it_content.term_name @ l
+    in
+    let names = List.fold_left collect_names ["@assigns"] l in
+    WpPropId.are_selected_names prop names
 
 let selected_allocates ~prop = function
   | Cil_types.FreeAllocAny -> false
@@ -100,7 +106,7 @@ let selected_allocates ~prop = function
 
 let selected_precond ~prop ip =
   prop = [] ||
-  let tk_name = "@ensures" in
+  let tk_name = "@requires" in
   let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
   WpPropId.are_selected_names prop (tk_name :: tp_names)
 
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 45d5c45192254e7123370cbfe85cef3eae80904e..d98e533eea15680bc8d639eb5f10a5f63273a3e1 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -71,6 +71,9 @@ val select_for_behaviors : string list -> prop_id -> bool
 (** test if the prop_id has to be selected when we want to select the call. *)
 val select_call_pre : stmt -> Property.t option -> prop_id -> bool
 
+(** From a list of names (of an identified terms), returns usable names. *)
+val ident_names : string list -> string list
+
 (*----------------------------------------------------------------------------*)
 
 val prop_id_keys : prop_id -> string list * string list (* required , hints *)