diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
new file mode 100644
index 0000000000000000000000000000000000000000..56879f81f0de8cb7337fe52d7f1b11ee4a110ebb
--- /dev/null
+++ b/src/plugins/wp/Why3Import.ml
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+module L = Wp_parameters
+
+(* -------------------------------------------------------------------------- *)
+
+let () =
+  Boot.Main.extend
+    begin fun () ->
+      let libs = L.Library.get () in
+      List.iter
+        (fun dir ->
+           L.debug ~level:1 " + LIB %a@." Filepath.Normalized.pretty dir
+        ) libs ;
+      let thys = L.Import.get () in
+      List.iter
+        (fun thy ->
+           L.debug ~level:1 " + THY %s@." thy
+        ) thys ;
+    end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Why3Import.mli b/src/plugins/wp/Why3Import.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0bb95bea6749b20699ff71c8163c6eef46d73f50
--- /dev/null
+++ b/src/plugins/wp/Why3Import.mli
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 88cdfd069baf8bd39d04844d7c9a4d934d747f87..45161b47bbefad2107f8ffed4a23a3a66ebfffad 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -839,6 +839,28 @@ module Tactics = String_list
     end)
 let () = on_reset Tactics.clear
 
+let () = Parameter_customize.set_group wp_prover
+let () = Parameter_customize.is_invisible ()
+module Import =
+  String_list
+    (struct
+      let option_name = "-wp-import"
+      let arg_name = "thy,..."
+      let help = "Import Why3 theories"
+    end)
+
+let () = Parameter_customize.set_group wp_prover
+let () = Parameter_customize.is_invisible ()
+module Library =
+  Filepath_list
+    (struct
+      let option_name = "-wp-library"
+      let arg_name = "dir,..."
+      let file_kind = "Why3 load path"
+      let existence = Fc_Filepath.Must_exist
+      let help = "Load path for importing why3 theories"
+    end)
+
 let () = Parameter_customize.set_group wp_prover
 module Drivers =
   Filepath_list
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 9a00ddf2b3acfb3a39ce18fcd051c43865cebb37..223b72fedb60eb8ff9cdca3f9ebd978a698e6206 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -126,6 +126,8 @@ module Cache: Parameter_sig.String
 module CacheEnv: Parameter_sig.Bool
 module CacheDir: Parameter_sig.String
 module CachePrint: Parameter_sig.Bool
+module Import: Parameter_sig.String_list
+module Library: Parameter_sig.Filepath_list
 module Drivers: Parameter_sig.Filepath_list
 module Timeout: Parameter_sig.Int
 module Memlimit: Parameter_sig.Int