diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 0cf379c647a9396abb574b71bc20948c82b01619..c92b0ca59fb985c1a5b76353ce52de64594e1ba7 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -25,11 +25,6 @@
 (* -------------------------------------------------------------------------- *)
 
 let dkey_shell = Wp_parameters.register_category "shell"
-let dkey_no_time_info = Wp_parameters.register_category "no-time-info"
-let dkey_no_step_info = Wp_parameters.register_category "no-step-info"
-let dkey_no_goals_info = Wp_parameters.register_category "no-goals-info"
-let dkey_no_cache_info = Wp_parameters.register_category "no-cache-info"
-let dkey_success_only = Wp_parameters.register_category "success-only"
 
 type prover =
   | Why3 of Why3Provers.t (* Prover via WHY *)
@@ -92,7 +87,7 @@ let name_of_prover = function
 
 let title_of_prover = function
   | Why3 s ->
-      if Wp_parameters.has_dkey dkey_success_only
+      if Wp_parameters.has_dkey dkey_shell
       then Why3Provers.name s
       else Why3Provers.title s
   | NativeAltErgo -> "Alt-Ergo (native)"
@@ -299,15 +294,15 @@ let perfo dkey = not (Wp_parameters.has_dkey dkey)
 let pp_perf fmt r =
   begin
     let t = r.solver_time in
-    if t > Rformat.epsilon && perfo dkey_no_time_info
+    if t > Rformat.epsilon && perfo dkey_shell
     then Format.fprintf fmt " (Qed:%a)" Rformat.pp_time t ;
     let t = r.prover_time in
-    if t > Rformat.epsilon && perfo dkey_no_time_info
+    if t > Rformat.epsilon && perfo dkey_shell
     then Format.fprintf fmt " (%a)" Rformat.pp_time t ;
     let s = r.prover_steps in
-    if s > 0 && perfo dkey_no_step_info
+    if s > 0 && perfo dkey_shell
     then Format.fprintf fmt " (%d)" s ;
-    if r.cached && perfo dkey_no_cache_info
+    if r.cached && perfo dkey_shell
     then Format.fprintf fmt " (cached)" ;
   end
 
@@ -335,7 +330,7 @@ let pp_cache_miss fmt st prover r =
     Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
 
 let pp_result_qualif prover fmt r =
-  if Wp_parameters.has_dkey dkey_success_only then
+  if Wp_parameters.has_dkey dkey_shell then
     match r.verdict with
     | NoResult -> Format.pp_print_string fmt "No Result"
     | Computing _ -> Format.pp_print_string fmt "Computing"
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 3e1acbf04bbbf09e247ea8bdf4935577ce5e4497..0e869ebea1458ef899c8e8ea6ff4b563cf224644 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -127,8 +127,3 @@ val choose : result -> result -> result
 val best : result list -> result
 
 val dkey_shell: Wp_parameters.category
-val dkey_no_time_info: Wp_parameters.category
-val dkey_no_step_info: Wp_parameters.category
-val dkey_no_goals_info: Wp_parameters.category
-val dkey_no_cache_info: Wp_parameters.category
-val dkey_success_only: Wp_parameters.category
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 2a0acd067fafb3f6f422a2493cda6812878c0ea6..c350f0f5779d5de2272bee29683161bf140e4290 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -263,20 +263,17 @@ let add_time s t =
     end
 
 let do_list_scheduled iter_on_goals =
-  if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
-    begin
-      clear_scheduled () ;
-      iter_on_goals
-        (fun goal ->
-           begin
-             incr scheduled ;
-             if !spy then session := GOALS.add goal !session ;
-           end) ;
-      match !scheduled with
-      | 0 -> Wp_parameters.warning ~current:false "No goal generated"
-      | 1 -> Wp_parameters.feedback "1 goal scheduled"
-      | n -> Wp_parameters.feedback "%d goals scheduled" n
-    end
+  clear_scheduled () ;
+  iter_on_goals
+    (fun goal ->
+       begin
+         incr scheduled ;
+         if !spy then session := GOALS.add goal !session ;
+       end) ;
+  match !scheduled with
+  | 0 -> Wp_parameters.warning ~current:false "No goal generated"
+  | 1 -> Wp_parameters.feedback "1 goal scheduled"
+  | n -> Wp_parameters.feedback "%d goals scheduled" n
 
 let dkey_prover = Wp_parameters.register_category "prover"
 
@@ -305,8 +302,7 @@ let do_progress goal msg =
 
 let do_report_cache_usage mode =
   if !exercised > 0 &&
-     not (Wp_parameters.has_dkey VCS.dkey_shell) &&
-     not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
+     not (Wp_parameters.has_dkey VCS.dkey_shell)
   then
     let hits = Cache.get_hits () in
     let miss = Cache.get_miss () in
@@ -450,8 +446,7 @@ let do_report_time fmt s =
   begin
     if s.n_time > 0 &&
        s.u_time > Rformat.epsilon &&
-       not (Wp_parameters.has_dkey VCS.dkey_no_time_info) &&
-       not (Wp_parameters.has_dkey VCS.dkey_success_only)
+       not (Wp_parameters.has_dkey VCS.dkey_shell)
     then
       let mean = s.a_time /. float s.n_time in
       let epsilon = 0.05 *. mean in
@@ -474,14 +469,13 @@ let do_report_time fmt s =
 let do_report_steps fmt s =
   begin
     if s.steps > 0 &&
-       not (Wp_parameters.has_dkey VCS.dkey_no_step_info) &&
-       not (Wp_parameters.has_dkey VCS.dkey_success_only)
+       not (Wp_parameters.has_dkey VCS.dkey_shell)
     then
       Format.fprintf fmt " (%d)" s.steps ;
   end
 
 let do_report_stopped fmt s =
-  if Wp_parameters.has_dkey VCS.dkey_success_only then
+  if Wp_parameters.has_dkey VCS.dkey_shell then
     begin
       let n = s.interrupted + s.unknown in
       if n > 0 then
@@ -510,27 +504,26 @@ let do_report_prover_stats pp_prover fmt (p,s) =
   end
 
 let do_report_scheduled () =
-  if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
-    if Wp_parameters.Generate.get () then
-      let plural = if !exercised > 1 then "s" else "" in
-      Wp_parameters.result "%d goal%s generated" !exercised plural
-    else
-    if !scheduled > 0 then
-      begin
-        let proved = GOALS.cardinal !proved in
-        let mode = Cache.get_mode () in
-        if mode <> Cache.NoCache then do_report_cache_usage mode ;
-        Wp_parameters.result "%t"
-          begin fun fmt ->
-            Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
-            Pretty_utils.pp_items
-              ~min:12 ~align:`Left
-              ~title:(fun (prover,_) -> VCS.title_of_prover prover)
-              ~iter:(fun f -> PM.iter (fun p s -> f (p,s)) !provers)
-              ~pp_title:(fun fmt a -> Format.fprintf fmt "%s:" a)
-              ~pp_item:do_report_prover_stats fmt ;
-          end ;
-      end
+  if Wp_parameters.Generate.get () then
+    let plural = if !exercised > 1 then "s" else "" in
+    Wp_parameters.result "%d goal%s generated" !exercised plural
+  else
+  if !scheduled > 0 then
+    begin
+      let proved = GOALS.cardinal !proved in
+      let mode = Cache.get_mode () in
+      if mode <> Cache.NoCache then do_report_cache_usage mode ;
+      Wp_parameters.result "%t"
+        begin fun fmt ->
+          Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
+          Pretty_utils.pp_items
+            ~min:12 ~align:`Left
+            ~title:(fun (prover,_) -> VCS.title_of_prover prover)
+            ~iter:(fun f -> PM.iter (fun p s -> f (p,s)) !provers)
+            ~pp_title:(fun fmt a -> Format.fprintf fmt "%s:" a)
+            ~pp_item:do_report_prover_stats fmt ;
+        end ;
+    end
 
 let do_list_scheduled_result () =
   begin
@@ -738,8 +731,7 @@ let do_cache_cleanup () =
     Cache.cleanup_cache () ;
     let removed = Cache.get_removed () in
     if removed > 0 &&
-       not (Wp_parameters.has_dkey VCS.dkey_shell) &&
-       not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
+       not (Wp_parameters.has_dkey VCS.dkey_shell)
     then
       Wp_parameters.result "[Cache] removed:%d" removed
   end
@@ -905,7 +897,10 @@ let pp_wp_parameters fmt =
     if Wp_parameters.RTE.get () then Format.pp_print_string fmt " -wp-rte" ;
     let spec = Wp_parameters.Model.get () in
     if spec <> [] && spec <> ["Typed"] then
-      ( let descr = Factory.descr (Factory.parse spec) in
+      ( let descr =
+          if spec = ["Dump"] then "Dump"
+          else Factory.descr (Factory.parse spec)
+        in
         Format.fprintf fmt " -wp-model '%s'" descr ) ;
     if not (Wp_parameters.Let.get ()) then Format.pp_print_string fmt
         " -wp-no-let" ;
diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index 2eb7d3d587b555af4b14c9f791c20376a97d2b5c..181dab0d59b9b32b46d5f730f963fbbdd298448e 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -63,7 +63,7 @@ below for details.
 
 To be accepted by Frama-CI, tests in « qualif » configuration must be easily
 reproducible on any platform. This is checked by running WP with flag
-`-wp-msg-key success-only` which is set by the default in the qualif test
+`-wp-msg-key shell` which is set by the default in the qualif test
 configuration. Hence, a qualified test result only contains proof status that
 are either:
 - failed
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 29195ff38b165f48d638ff1c1ef4c558669da718..82ac23797226aae576338c46106f95e16f40b717 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
 OPT:
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.i b/src/plugins/wp/tests/wp/stmtcompiler_test.i
index 264b9e58d48e6401b1c73564a7755720598f2b97..c610d54549272ce23c3610a5e58846880fcd5b00 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.i
@@ -1,5 +1,5 @@
 /* run.config
-   OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key success-only
+   OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key shell
 */
 
 int empty (int c){
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
index 4dafe25db11100c8549fc7f6291914f0a31f9df0..b206efad0519db1f347ae4a6b79e5221ff611f9d 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
@@ -1,5 +1,5 @@
 /* run.config_qualif
-   OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key success-only
+   OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key shell
 */
 
 int empty (int c){
diff --git a/src/plugins/wp/tests/wp/wp_strategy.c b/src/plugins/wp/tests/wp/wp_strategy.c
index 0afd35c132005b5dc32d047c4d9847b410013b91..c514347a72a233922e656c26095d63647feea376 100644
--- a/src/plugins/wp/tests/wp/wp_strategy.c
+++ b/src/plugins/wp/tests/wp/wp_strategy.c
@@ -4,7 +4,7 @@ OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
 */
 
 /* run.config_qualif
-OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key "success-only"
+OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
 */
 /*----------------------------------------------------------------------------*/
 
@@ -89,7 +89,7 @@ int default_behaviors (int c, int x) {
   int y;
 
   //@ ensures qed_ok: stmt_p: x > 0; assigns qed_ok: x;
-  if (c) x = 1; 
+  if (c) x = 1;
   else {
     //@ assert qed_ok: x >= 0;
     x++;
diff --git a/src/plugins/wp/tests/wp_acsl/boolean.i b/src/plugins/wp/tests/wp_acsl/boolean.i
index f8e7f458b4f55d82f878bfed3a4a83f71dd3352e..79f94c24a8a358a23922d03fee6157f4d6f03ad1 100644
--- a/src/plugins/wp/tests/wp_acsl/boolean.i
+++ b/src/plugins/wp/tests/wp_acsl/boolean.i
@@ -1,5 +1,5 @@
 /* run.config
-OPT: -wp-gen -wp-prover why3 -wp-msg-key success-only
+OPT: -wp-gen -wp-prover why3 -wp-msg-key shell
 */
 
  /*@
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 40c0c6de692e62b8846b7a62e3bc02b1dcfb564c..979b8b88f24de686b3269c1c829b0bf3c69cf033 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -305,4 +305,4 @@
  Functions                 WP     Alt-Ergo  Total   Success
   f                        12       31       43       100%
 ------------------------------------------------------------
-[wp] Logging keys: success-only,shell,cnf.
+[wp] Logging keys: shell,cnf.
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
index 00a8df49e163c00104c97b7203e10f9e6f4accfa..064dce264b9e7e20ae5c3d9799927e9b346ed87c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
@@ -8,7 +8,6 @@
 [rte] annotating function init
 [rte] annotating function mem_binding
 [rte] annotating function size
-[wp] Computing [100 goals...]
 [wp] Goal typed_add_complete_full_nominal : not tried
 [wp] Goal typed_add_disjoint_full_nominal : not tried
 [wp] Goal typed_add_assert_rte_index_bound : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 6e3fc54c35c0210277228789814f49736f648f08..8e5320587c9157e2971dc28f9078d3d860dbfd28 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -3,7 +3,6 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
 [wp] 102 goals scheduled
 [wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
 [wp] [Alt-Ergo] Goal typed_add_disjoint_full_nominal : Valid
diff --git a/src/plugins/wp/tests/wp_manual/manual.i b/src/plugins/wp/tests/wp_manual/manual.i
index 7cd72107d4ca6d53372e573288e68d42ab88786c..11a04e0783ab7854b9dcb873766eaa739de19bfa 100644
--- a/src/plugins/wp/tests/wp_manual/manual.i
+++ b/src/plugins/wp/tests/wp_manual/manual.i
@@ -2,8 +2,8 @@
    DONTRUN:
 */
 /* run.config_qualif
-   OPT: -wp-msg-key no-time-info @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
-   OPT: -wp-msg-key no-time-info -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
-   OPT: -load-module report -kernel-verbose 0 -wp-msg-key no-time-info -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report  
+   OPT: -wp-msg-key shell @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
+   OPT: -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
+   OPT: -load-module report -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
 */
 void look_at_working_dir(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index 98b421111a0747310342b30ae27213ef61a1adc8..0e98bda081db384a322195823f214794edf217e0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -1,10 +1,11 @@
+# frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/removed.i (no preprocessing)
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  
-[eva:alarm] tests/wp_plugin/removed.i:10: Warning: 
+
+[eva:alarm] tests/wp_plugin/removed.i:10: Warning:
   signed overflow. assert 1 + i ≤ 2147483647;
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
index efc57b6183b5975f7b8605af6ecacb8409e2fa88..583f4d36f0886bdb9e400a01be8bc0d7723ec389 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
@@ -1,3 +1,4 @@
+# frama-c -wp -wp-model 'Dump' [...]
 [kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] [CFG] Goal f_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index f27fb0df1d6386f8b02e3954f7cf1cab1d922897..a0e4b8e3fef874b15f67e384203eca37fd0fa091 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,5 +1,5 @@
 /* run.config_qualif
-   CMD: @frama-c@ -wp-share ./share -wp-msg-key no-cache-info,success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay -wp-cache-dir ./cache
+   CMD: @frama-c@ -wp-share ./share -wp-msg-key shell -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay -wp-cache-dir ./cache
    OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
  */
 
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
index 02e1eddff383cc8b84a70ba560c0f62f60cd4d4d..58e04b9d85fccbba9f6eb09c1738dffc0c98768c 100644
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ b/src/plugins/wp/tests/wp_plugin/stmt.c
@@ -4,7 +4,7 @@
 
 /* run.config_qualif
    OPT: -load-module report -then -report
-   EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key no-cache-info @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
+   EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
 */
 
 /*@ ensures a > 0 ==> \result == a + b;
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 999fd9b742431831e08595ee7463dfe6d0469cd4..e8e6e13bc582dde43cd57df852ee32ea1fc163ed 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -8,7 +8,6 @@
 [wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
 [wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
 ------------------------------------------------------------
   Function init
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index e6996907f9367101bc6353be0b7ae906cb568ba9..aa1fcfbc2ff78b19adb1a83efb7a8576a3e8bf19 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -8,7 +8,6 @@
 [wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
 [wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
 ------------------------------------------------------------
   Function init
 ------------------------------------------------------------
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 4f85fe8851bc0fa7025f2cffd3fb2d1ca71b67bc..1d6649a3de7511c3c8a26c798fa5d9a90c25877d 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -659,7 +659,7 @@ let add g =
         Gmap.iter
           (fun _ ws -> WPOset.iter (fun _ -> incr added) ws)
           system.wpo_idx ;
-        if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
+        if not (Wp_parameters.has_dkey VCS.dkey_shell) then
           Wp_parameters.feedback ~ontty:`Feedback "Computing [%d goals...]" !added ;
         added := 0 ;
       end ;