diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 65843136872b5e143fc4ce3420645d94c8a8c47e..e949fb06f40c491653433c6187ac9063e4228382 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,7 +20,8 @@
 #   <Prover>: prover
 ###############################################################################
 
- -  Wp         [2019/01/28] New floating-point model
+ - WP          [2019/02/05] Auto filter properties with name "no_wp:"
+ - Wp          [2019/01/28] New floating-point model
  - WP          [2018/02/16] Filter out some variables from separation
  - TIP         [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
  - TIP         [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 86bdae51f57dfe3abd6becd0515a2ac2005680b5..ab349e425308f1774eb5307db76523f8912319ec 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -762,6 +762,9 @@ interface of the programmatic API.
     Properties can be prefixed with a minus sign to \emph{skip} the associated annotations.
     For example \texttt{-wp-prop="-@assigns"} removes all \texttt{assigns} 
     and \texttt{loop assigns} properties from the selection.
+    \\
+    \textbf{Remark:} properties with name \verb+no_wp:+ are always and automatically
+    filtered and never proved by WP.
 \item [\tt -wp-(no)-status-all] includes in the goal selection all properties
   regardless of their current status (default is: \texttt{no}).
 \item [\tt -wp-(no)-status-valid] includes in the goal selection those properties
diff --git a/src/plugins/wp/tests/wp_plugin/nowp.c b/src/plugins/wp/tests/wp_plugin/nowp.c
new file mode 100644
index 0000000000000000000000000000000000000000..c79a19034c767680848e94d5abcd741f6a014b2c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nowp.c
@@ -0,0 +1,7 @@
+
+int main(int a) {
+  int b;
+  if (a) b = 42 + a;
+  //@ assert no_wp: \initialized(&b);
+  return b;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json b/src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json
new file mode 100644
index 0000000000000000000000000000000000000000..19765bd501b636fce433540d9e6735f51d66151d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json
@@ -0,0 +1 @@
+null
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..134cf5cfbb8c57d81ee16894ba4537b84276e946
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
@@ -0,0 +1,6 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] No proof obligations
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a36ba39702833588de2342c76fca8306cec40df1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
@@ -0,0 +1,9 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 0 goal scheduled
+[wp] Proved goals:    0 / 0
+[wp] Report 'tests/wp_plugin/nowp.c.0.report.json'
+-------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index cffa1268c684c66beb4e9161aeb2a7aa346c7982..b3e9f7e76b926fca16b00e148b487a7e93656298 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -325,10 +325,10 @@ let filter_configstatus config pid =
 
 let filter_asked config pid =
   match config.asked_prop with
-  | AllProps -> true
   | IdProp idp -> Property.equal (WpPropId.property_of_id pid) idp
   | CallPre (s_call, asked_pre) -> WpPropId.select_call_pre s_call asked_pre pid
   | NamedProp names -> WpPropId.select_by_name names pid
+  | AllProps -> WpPropId.select_default pid
 
 let rec filter config pid = function
   | [] -> None
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7ee846ce041899d1ccc150f7655f6304006de089..43fc36f5e260ff53b4f96bbd8a6100c933dd5b76 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -693,29 +693,38 @@ let is_loop_preservation p =
       end
   | _ -> None
 
-let select_by_name asked_names pid =
+let user_prop_pid pid =
   let p_prop = match pid.p_kind with
     | PKPre (_,_,p_prop) -> p_prop
-    | _ -> property_of_id pid
-  in
-  let names = user_prop_names p_prop in
-  let is_minus s = try s.[0] = '-' with _ -> false in
-  let is_plus s = try s.[0] = '+' with _ -> false in
-  let remove_first s = String.sub s 1 ((String.length s) -1) in
-  let eval acc asked =
-    let is_minus,a = match acc with
-      | None -> if is_minus asked then true,true else false,false
-      | Some a -> (is_minus asked),a
-    in let eval () =
-         let asked = if is_minus || (is_plus asked) then remove_first asked else asked
-         in List.mem asked names
-    in Some (if is_minus
-             then a && (not (eval ()))
-             else a || (eval ()))
-  in
-  match List.fold_left eval None asked_names with
-  | Some false -> false
-  | _ -> true
+    | _ -> property_of_id pid in
+  user_prop_names p_prop
+
+let select_default pid =
+  let names = user_prop_pid pid in
+  not (List.mem "no_wp" names)
+
+let select_by_name asked_names pid =
+  let names = user_prop_pid pid in
+  if List.mem "no_wp" names then false
+  else
+    let is_minus s = try s.[0] = '-' with _ -> false in
+    let is_plus s = try s.[0] = '+' with _ -> false in
+    let remove_first s = String.sub s 1 ((String.length s) -1) in
+    let eval acc asked =
+      let is_minus,a = match acc with
+        | None -> if is_minus asked then true,true else false,false
+        | Some a -> (is_minus asked),a
+      in let eval () =
+           let asked = if is_minus || (is_plus asked)
+             then remove_first asked else asked
+           in List.mem asked names
+      in Some (if is_minus
+               then a && (not (eval ()))
+               else a || (eval ()))
+    in
+    match List.fold_left eval None asked_names with
+    | Some false -> false
+    | _ -> true
 
 let select_call_pre s_call asked_pre pid =
   match pid.p_kind with
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 16b42ff8adc916777fbc0510f968b4f8d83a58eb..5b143da74269b1e92f2923eaa1a92533c6c6f64f 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -54,8 +54,12 @@ val is_assigns : prop_id -> bool
 val is_requires : Property.t -> bool
 val is_loop_preservation : prop_id -> stmt option
 
+(** test if the prop_id does not have a [no_wp:] in its name(s). *)
+val select_default : prop_id -> bool
+
 (** test if the prop_id has to be selected for the asked name.
- * Also returns a debug message to explain then answer. *)
+    Also returns a debug message to explain then answer. Includes
+    a test for [no_wp:]. *)
 val select_by_name : string list -> prop_id -> bool
 
 (** test if the prop_id has to be selected when we want to select the call