diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index b343e24d20cc2adf85d9ac0559431dece966b38b..67e5fb613b6e9f704f69b569c74bccb31d18a7dd 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -27,6 +27,7 @@
 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_success_only = Wp_parameters.register_category "success-only"
 
 type prover =
   | Why3 of string (* Prover via WHY *)
@@ -339,8 +340,12 @@ let pp_res ~extended fmt r =
   | NoResult -> Format.pp_print_string fmt (if extended then "No Result" else "-")
   | Invalid -> Format.pp_print_string fmt "Invalid"
   | Computing _ -> Format.pp_print_string fmt "Computing"
-  | Valid -> Format.fprintf fmt "Valid%a" (pp_perf ~extended) r
   | Checked -> Format.fprintf fmt "Typechecked"
+  | Valid when Wp_parameters.has_dkey dkey_success_only ->
+      Format.pp_print_string fmt "Valid"
+  | (Timeout|Stepout|Unknown) when Wp_parameters.has_dkey dkey_success_only ->
+      Format.pp_print_string fmt "Unsuccess"
+  | Valid -> Format.fprintf fmt "Valid%a" (pp_perf ~extended) r
   | Unknown -> Format.fprintf fmt "Unknown%a" (pp_perf ~extended) r
   | Timeout -> Format.fprintf fmt "Timeout%a" (pp_perf ~extended) r
   | Stepout -> Format.fprintf fmt "Step limit%a" (pp_perf ~extended) r
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 31bf3423feb10d9348c935eec2ebb1da760a911a..68f46c4168ddf1386fdc4c4897eb888f74f18987 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -135,3 +135,4 @@ val compare : result -> result -> int (* best is minimal *)
 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_success_only: Wp_parameters.category
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index ae5dcd02429cb933efa456d8861aebe6664703c3..a21ded01520598d554c5b182a96088c017eea56a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -363,39 +363,62 @@ let do_wpo_success goal s =
           Wp_parameters.feedback ~ontty:`Silent
             "[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal)
 
+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)
+    then
+      let mean = s.a_time /. float s.n_time in
+      let epsilon = 0.05 *. mean in
+      let delta = s.u_time -. s.d_time in
+      if delta < epsilon then
+        Format.fprintf fmt " (%a)" Rformat.pp_time mean
+      else
+        let middle = (s.u_time +. s.d_time) *. 0.5 in
+        if abs_float (middle -. mean) < epsilon then
+          Format.fprintf fmt " (%a-%a)"
+            Rformat.pp_time s.d_time
+            Rformat.pp_time s.u_time
+        else
+          Format.fprintf fmt " (%a-%a-%a)"
+            Rformat.pp_time s.d_time
+            Rformat.pp_time mean
+            Rformat.pp_time s.u_time
+  end
+
+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)
+    then
+      Format.fprintf fmt " (%d)" s.steps ;
+  end
+
+let do_report_stopped fmt s =
+  if Wp_parameters.has_dkey VCS.dkey_success_only then
+    begin
+      let n = s.interrupted + s.unknown + s.failed in
+      if n > 0 then
+        Format.fprintf fmt " (unsuccess: %d)" n ;
+    end
+  else
+    begin
+      if s.interrupted > 0 then
+        Format.fprintf fmt " (interrupted: %d)" s.interrupted ;
+      if s.unknown > 0 then
+        Format.fprintf fmt " (unknown: %d)" s.unknown ;
+    end
+
 let do_report_prover_stats pp_prover fmt (p,s) =
   begin
     let name = VCS.title_of_prover p in
     Format.fprintf fmt "%a %4d " pp_prover name s.proved ;
-    begin
-      if s.n_time > 0 &&
-         s.u_time > Rformat.epsilon &&
-         not (Wp_parameters.has_dkey VCS.dkey_no_time_info)
-      then
-        let mean = s.a_time /. float s.n_time in
-        let epsilon = 0.05 *. mean in
-        let delta = s.u_time -. s.d_time in
-        if delta < epsilon then
-          Format.fprintf fmt " (%a)" Rformat.pp_time mean
-        else
-          let middle = (s.u_time +. s.d_time) *. 0.5 in
-          if abs_float (middle -. mean) < epsilon then
-            Format.fprintf fmt " (%a-%a)"
-              Rformat.pp_time s.d_time
-              Rformat.pp_time s.u_time
-          else
-            Format.fprintf fmt " (%a-%a-%a)"
-              Rformat.pp_time s.d_time
-              Rformat.pp_time mean
-              Rformat.pp_time s.u_time
-    end ;
-    if s.steps > 0  &&
-       not (Wp_parameters.has_dkey VCS.dkey_no_step_info) then
-      Format.fprintf fmt " (%d)" s.steps ;
-    if s.interrupted > 0 then
-      Format.fprintf fmt " (interrupted: %d)" s.interrupted ;
-    if s.unknown > 0 then
-      Format.fprintf fmt " (unknown: %d)" s.unknown ;
+    do_report_time fmt s ;
+    do_report_steps fmt s ;
+    do_report_stopped fmt s ;
     if s.failed > 0 then
       Format.fprintf fmt " (failed: %d)" s.failed ;
     Format.fprintf fmt "@\n" ;