diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index e47be993a8a5a428b4bcb8f1a37874ac0289fc56..174873b3019c281b3d86afbe536c5f6687d7da80 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,9 @@
 Plugin WP <next-release>
 ########################
 
+- WP          [2023-02-03] new option -wp-why3-extra-config for providing
+                           additional Why3 configuration files
+
 #####################
 Plugin WP 26.0 (Iron)
 #####################
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index a30b2e536ec3ba6e2997f0f2907a8569dce11099..38a9e97129761c0fae3e4dae9a1904f9c1e6b3be 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -26,7 +26,8 @@
 
 let cfg = lazy
   begin
-    try Why3.Whyconf.init_config None
+    let extra_config = Wp_parameters.Why3ExtraConfig.get () in
+    try Why3.Whyconf.init_config ~extra_config None
     with exn ->
       Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
   end
@@ -41,8 +42,12 @@ let configure =
   begin fun () ->
     if !todo then
       begin
-        let args = Array.of_list ("why3"::Wp_parameters.Why3Flags.get ()) in
+        let commands = "why3"::Wp_parameters.Why3Flags.get () in
+        let args = Array.of_list commands in
         begin try
+            (* Ensure that an error message generating directly by why3 is
+               reported as coming from Why3, not from Frama-C. *)
+            Why3.Getopt.commands := commands;
             Why3.Getopt.parse_all
               (Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list])
               (fun opt -> raise (Arg.Bad ("unknown option: " ^ opt)))
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index b891cf1c4c41f52f30f129764c8719be7f9bb454..ce7ead626d04c77fef0413a8e88771037b5e1fae 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1346,6 +1346,8 @@ See \texttt{-wp-interactive <mode>} option for details.
   steps. This can be used as a machine-independent alternative to timeout.
 \item[\tt -wp-why3-opt='options,...'] provides additional options to the
   \verb+why3+ command.
+\item[\tt -wp-why3-extra-config='files,...'] provides additional configuration
+  files for \verb+why3+.
 \item[\tt -wp-prepare-scripts] initialize a script tracking directory in the
   session directory.
 \item[\tt -wp-finalize-scripts] remove untracked scripts according to the
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 5a63447c8844bb2ea82f7bdb07887248f54d53e8..23ff0dda57c622e47b57170e242faee62c225069 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -983,6 +983,16 @@ module Why3Flags =
       let help = "Additional options for Why3"
     end)
 
+let () = Parameter_customize.set_group wp_prover_options
+let () = Parameter_customize.no_category ()
+module Why3ExtraConfig =
+  String_list
+    (struct
+      let option_name = "-wp-why3-extra-config"
+      let arg_name = "file,..."
+      let help = "Additional config files for Why3"
+    end)
+
 (* ------------------------------------------------------------------------ *)
 (* --- PO Management                                                    --- *)
 (* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 74e6e0376c6e09feb6272c801f8ad3d73d887be1..786bf2d170668267ba39a507a078806ac18793de 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -136,6 +136,7 @@ module Steps: Parameter_sig.Int
 module Procs: Parameter_sig.Int
 module ProofTrace: Parameter_sig.Bool
 module Why3Flags: Parameter_sig.String_list
+module Why3ExtraConfig: Parameter_sig.String_list
 
 module Auto: Parameter_sig.String_list
 module AutoDepth: Parameter_sig.Int