diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 7cf2a73dd9a1616da302af686a11a21ad0d485b4..7ccb3f4c493234e7eacdf4b8c7922ab3e22e3f23 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -23,6 +23,8 @@
 -  Wp         [2019/28/01] Now -wp-dynamic is set by default (annotation @calls)
 
  -  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 40d9d63d4dbbbe2a2b8d52cdd48e586e158b999a..478983a60bd6a1333dc9277ff6a8aba7587e828a 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 5369d46e449d160f921822ea13e6ca1488681109..b0203265ab29603de764b54e26f512e2a3f6826e 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -329,10 +329,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 c20fbae10bf92f26c788a3b839a34a9b3183dd0a..2cde75506a5960e32eb8a2e6493738a24241bedb 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -694,29 +694,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