diff --git a/opam/opam b/opam/opam
index f60fee39900551bb31fa7b8f19d69106431bc618..d20af2f6f82340c4314295461fe5a7fc29c61abd 100644
--- a/opam/opam
+++ b/opam/opam
@@ -135,3 +135,7 @@ messages: [
   "The Frama-C/Wp native support for Coq is now deprecated (use TIP or Why-3 instead)."
   {coq:installed}
 ]
+
+post-messages: [
+  "Why3 provers setup: rm -r ~/.why3.conf ; why3 config --detect"
+]
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 3c9a5f797a62fa1879dab6209297e3bda177d835..19e8070cf06d110febdbf0a04f7c5aa471445f94 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -64,7 +64,6 @@ let find_opt s =
   try
     let config = Lazy.force cfg in
     let filter = Why3.Whyconf.parse_filter_prover s in
-    let filter = Why3.Whyconf.filter_prover_with_shortcut config filter in
     Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
   with
   | Why3.Whyconf.ProverNotFound _
@@ -78,14 +77,18 @@ let find_fallback name =
   match find_opt 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
+      (* 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
 
 let print_why3 = Why3.Whyconf.prover_parseable_format
 let print_wp s =