diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index b175e95b7c7a82279f0bb0e19b356d2a3a8e066b..de3d5cee53e92a51c465c7d2d5b94e48d5ee52b8 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -207,7 +207,8 @@ let pp_stats fmt s =
   List.iter
     (fun (p,pr) ->
        let success = truncate pr.success in
-       Format.fprintf fmt " (%a" VCS.pp_prover p ;
+       let title = VCS.title_of_prover ~version:false p in
+       Format.fprintf fmt " (%s" title ;
        if success > 0 && np > 1 then
          Format.fprintf fmt " %d/%d" success np ;
        if not shell && pr.time > Rformat.epsilon then
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 8ed3c20de0ecdc23edaf09ec48700af1eb537f30..a280067c96a44566108d3d12744afecf72fd8fa4 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -79,9 +79,12 @@ let name_of_prover = function
   | Qed -> "qed"
   | Tactical -> "script"
 
-let title_of_prover = function
+let title_of_prover ?version = function
   | Why3 s ->
-    if Wp_parameters.has_dkey dkey_shell
+    let v = match version with Some v -> v | None ->
+      Wp_parameters.has_dkey dkey_shell
+    in
+    if v
     then Why3Provers.name s
     else Why3Provers.title s
   | Qed -> "Qed"
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index e4dc8bac052bd33860ff546522fc087c97bdb0cf..d1b89ddddd8856887adb3ea8cffc196d4ff7031c 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -42,7 +42,7 @@ module Pset : Set.S with type elt = prover
 module Pmap : Map.S with type key = prover
 
 val name_of_prover : prover -> string
-val title_of_prover : prover -> string
+val title_of_prover : ?version:bool -> prover -> string
 val filename_for_prover : prover -> string
 val title_of_mode : mode -> string