diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 38a9e97129761c0fae3e4dae9a1904f9c1e6b3be..d0c6c9074638ebb1bbcf8533e6045a98b2a642d8 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -62,16 +62,24 @@ let configure =
 
 type t = Why3.Whyconf.prover
 
+(* In an ambiguous map of provers, tries to find the basic alternative, if none
+   is found, just give an arbitrary one. *)
+let resolve_ambiguity provers =
+  let open Why3.Whyconf in
+  let provers = fst @@ List.split @@ Mprover.bindings provers in
+  try List.find (fun p -> p.prover_altern = "") provers
+  with Not_found -> List.hd provers
+
 let find_opt s =
+  let open Why3.Whyconf in
   try
     let config = Lazy.force cfg in
-    let filter = Why3.Whyconf.parse_filter_prover s in
-    Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
+    let filter = parse_filter_prover s in
+    Some ((filter_one_prover config filter).prover)
   with
-  | Why3.Whyconf.ProverNotFound _
-  | Why3.Whyconf.ParseFilterProver _
-  | Why3.Whyconf.ProverAmbiguity _  ->
-    None
+  | ParseFilterProver _ -> None
+  | ProverNotFound _ -> None
+  | ProverAmbiguity (_, _, provers)  -> Some (resolve_ambiguity provers)
 
 type fallback = Exact of t | Fallback of t | NotFound
 
@@ -79,18 +87,14 @@ let find_fallback name =
   match find_opt name with
   | Some prv -> Exact prv
   | None ->
-    (* Why3 should deal with this intermediate case *)
-    match find_opt (String.lowercase_ascii name) with
-    | Some prv -> Exact prv
-    | None ->
-      match String.split_on_char ',' name with
-      | shortname :: _ :: _ ->
-        begin
-          match find_opt (String.lowercase_ascii shortname) with
-          | Some prv -> Fallback prv
-          | None -> NotFound
-        end
-      | _ -> NotFound
+    match String.split_on_char ',' name with
+    | shortname :: _ :: _ ->
+      begin
+        match find_opt (String.lowercase_ascii shortname) with
+        | Some prv -> Fallback prv
+        | None -> NotFound
+      end
+    | _ -> NotFound
 
 let ident_why3 = Why3.Whyconf.prover_parseable_format
 let ident_wp s =
diff --git a/src/plugins/wp/gui/GuiConfig.ml b/src/plugins/wp/gui/GuiConfig.ml
index a6ba232e23f2945dc795bb5c9fd3aff42c1ad2f2..f40609610d935c291e8d1bfe4e24c46efb05d3d7 100644
--- a/src/plugins/wp/gui/GuiConfig.ml
+++ b/src/plugins/wp/gui/GuiConfig.ml
@@ -36,7 +36,7 @@ class provers =
         (* select automatically the provers set on the command line *)
         let cmdline =
           match Wp_parameters.Provers.get () with
-          | [] -> [ "alt-ergo" ]
+          | [] -> [ "Alt-Ergo" ]
           | prvs -> prvs
         in
         let selection = List.fold_left
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 21f04e38923c108d5a48dd8fe9101552374f0ca5..ab5b89f86ec858f593c42e285226d676df571807 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -549,7 +549,7 @@ let spawn_wp_proofs ~script goals =
 
 let get_prover_names () =
   match Wp_parameters.Provers.get () with
-  | [] -> [ "alt-ergo" ] | pnames -> pnames
+  | [] -> [ "Alt-Ergo" ] | pnames -> pnames
 
 let compute_provers ~mode ~script =
   script.provers <- List.fold_right
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 3e167f78bf94d7e2e68dfd7ce6c25f60653a1ed1..77eab89a96c13499b5f21265426a17ce2a45d0d2 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -22,7 +22,7 @@ let run () =
          | None -> prvs
          | Some VCS.Tactical -> prvs
          | Some prv -> (VCS.Batch, prv) :: prvs)
-      ["alt-ergo"] []
+      ["Alt-Ergo"] []
   in
 
   let spawn goal =