diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 0479e18eca4a90687493c00701b085e5dfe401f9..456c225e27580a465a04408b32aba22ed6b5a9cf 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -90,7 +90,10 @@ let name_of_prover = function
   | Tactical -> "script"
 
 let title_of_prover = function
-  | Why3 s -> Why3Provers.title s
+  | Why3 s ->
+      if Wp_parameters.has_dkey dkey_success_only
+      then Why3Provers.name s
+      else Why3Provers.title s
   | NativeAltErgo -> "Alt-Ergo (native)"
   | NativeCoq -> "Coq (native)"
   | Qed -> "Qed"
@@ -142,13 +145,7 @@ let cmp_prover p q =
   | _ , NativeCoq -> 1
   | Why3 p , Why3 q -> Why3Provers.compare p q
 
-let pp_prover fmt = function
-  | NativeAltErgo -> Format.pp_print_string fmt "Alt-Ergo (Native)"
-  | NativeCoq -> Format.pp_print_string fmt "Coq (Native)"
-  | Why3 smt -> Format.pp_print_string fmt (Why3Provers.title smt)
-  | Qed -> Format.fprintf fmt "Qed"
-  | Tactical -> Format.pp_print_string fmt "Tactical"
-
+let pp_prover fmt p = Format.pp_print_string fmt (title_of_prover p)
 let pp_mode fmt m = Format.pp_print_string fmt (title_of_mode m)
 
 module P = struct type t = prover let compare = cmp_prover end
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 7c7095340b0612aab085694b4b9ac76d4295c07d..aa52b12ef953ce7df4198d0ea0ed0bf3a4e4d2c4 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -92,6 +92,7 @@ let print_wp s =
   String.concat ":" prv
 
 let title p = Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p
+let name p = p.Why3.Whyconf.prover_name
 let compare = Why3.Whyconf.Prover.compare
 
 let provers () =
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 2e53fcdbead7dda322e803f51baf998f455f4dbb..43e65783484c5e02fbdd5b2e982f139c2bfcf505 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -35,6 +35,7 @@ val find_fallback : string -> fallback
 val print_why3 : t -> string
 val print_wp : t -> string
 val title : t -> string
+val name : t -> string
 val compare : t -> t -> int
 
 val provers : unit -> t list