diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 06d9e223bd630d88959d5f81bc10340beb855627..2656757db20a71825db99709227564859382e318 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -106,9 +106,8 @@ used, it is possible to have logic identifiers with an extended lexical format:
   For instance, \verb+Foo::bar'jazz+ is a syntactically valid identifier.
 \end{itemize}
 
-There is currently no support for external specification loaders from the
-standard distribution of \FramaC, although external plug-ins might define some
-using the extension API, consult the plug-in developer manual for details.
+External module importers are defined by plug-ins \textit{via} the extension API,
+consult the plug-in manuals and the plug-in developer manual for more details.
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index bbaecca93d1a04a4108183b023200631450dc8a0..bb0ad979e6f0964774a502e1226d0cf3c2da5a8c 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
 Plugin WP <next-release>
 ###############################################################################
 
+- WP          [2024-10-08] Why3 module importer (See manual § 2.4.13)
 -  WP         [2024-09-13] -wp-par now defaults to the number of logical cores
 -! WP         [2024-08-23] Remove wp_region
 -* WP         [2024-07-02] Fixed parsing of decimal literals
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index d3fc19a0fe83999b5718ac44b73b9ed1465391a1..af8fb11afe5d4fa59ba97e560f3231f83c778c9f 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -271,6 +271,11 @@ module DT = Logic_type_info.Set
 module DR = Compinfo.Set
 module DS = Datatype.String.Set
 module DF = Set.Make(Lang.Fun)
+module DW = Set.Make
+    (struct
+      type t = string list * string
+      let compare = Stdlib.compare
+    end)
 module DC = Set.Make
     (struct
       type t = cluster
@@ -294,7 +299,8 @@ class virtual visitor main =
     val mutable dlemmas  = DS.empty
     val mutable lemmas   = DS.empty
     val mutable clusters = DC.empty
-    val mutable theories = DS.empty
+    val mutable libraries = DS.empty
+    val mutable theories = DW.empty
     val mutable locals = DC.add main DC.empty
 
     method set_local c = locals <- DC.add c locals
@@ -374,6 +380,7 @@ class virtual visitor main =
       | Comp(r, KValue) -> self#vcomp r
       | Comp(r, KInit) -> self#vicomp r
       | Atype t -> self#vtype t
+      | Wtype(p,m,_) -> self#vtheory p m
 
     method vtau = function
       | Prop | Bool | Int | Real | Tvar _ -> ()
@@ -461,6 +468,7 @@ class virtual visitor main =
         begin
           symbols <- DF.add f symbols ;
           match f with
+          | FUN { m_source = Wsymbol(p,m,_) } -> self#vtheory p m
           | FUN { m_source = Extern e  } -> self#vlibrary e.ext_library
           | FUN { m_source = Generated _ } | ACSL _ -> self#vlfun f
           | CTOR c -> self#vadt (Lang.adt c.ctor_type)
@@ -512,17 +520,24 @@ class virtual visitor main =
           self#on_cluster c ;
         end
 
-    method vlibrary thy =
-      if not (DS.mem thy theories) then
+    method vlibrary lib =
+      if not (DS.mem lib libraries) then
         begin
-          theories <- DS.add thy theories ;
+          libraries <- DS.add lib libraries ;
           try
-            let deps = LogicBuiltins.dependencies thy in
+            let deps = LogicBuiltins.dependencies lib in
             List.iter self#vlibrary deps ;
-            self#on_library thy ;
+            self#on_library lib ;
           with Not_found ->
             Wp_parameters.fatal
-              ~current:false "Unknown library '%s'" thy
+              ~current:false "Unknown library '%s'" lib
+        end
+
+    method vtheory p m =
+      if not (DW.mem (p,m) theories) then
+        begin
+          theories <- DW.add (p,m) theories ;
+          self#on_theory p m
         end
 
     method vgoal (axioms : axioms option) prop =
@@ -562,6 +577,7 @@ class virtual visitor main =
       end
 
     method virtual section : string -> unit
+    method virtual on_theory : string list -> string -> unit
     method virtual on_library : string -> unit
     method virtual on_cluster : cluster -> unit
     method virtual on_type : logic_type_info -> typedef -> unit
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index 16ce71cef4f28702dd3e6d76c80c066f0fbf4f37..1c43c871ff56e037f82fe3ab3c22df17425f9eb7 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -120,6 +120,7 @@ class virtual visitor : cluster ->
     method vlemma : logic_lemma -> unit
     method vcluster : cluster -> unit
     method vlibrary : string -> unit
+    method vtheory : string list -> string -> unit
     method vgoal : axioms option -> F.pred -> unit
 
     method vtypes : unit
@@ -142,6 +143,9 @@ class virtual visitor : cluster ->
     method virtual on_library : string -> unit
     (** External library to import *)
 
+    method virtual on_theory : string list -> string -> unit
+    (** External Why3 theory to import *)
+
     method virtual on_cluster : cluster -> unit
     (** Outer cluster to import *)
 
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index f90e9262f35bd6f38661d1d6b25211a638ecc686..ed5b259f8d0acbf023d08cb677fa787f1d7d4642 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -113,6 +113,7 @@ type adt =
   | Mrecord of mdt * fields (* Model record-type *)
   | Atype of logic_type_info (* Logic Type *)
   | Comp of compinfo * datakind (* C-code struct or union *)
+  | Wtype of string list * string * string list (** Why3 imported type *)
 
 (** name to print to the provers *)
 and mdt = string extern
@@ -197,7 +198,10 @@ let rec varpoly k x = function
   | [] -> Warning.error "Unbound type parameter <%s>" x
   | y::ys -> if x = y then k else varpoly (succ k) x ys
 
-type t_builtin = E_mdt of mdt | E_poly of (tau list -> tau)
+type t_builtin =
+  | E_mdt of mdt
+  | E_why3 of string list * string * string list
+  | E_poly of (tau list -> tau)
 let builtin_types = Context.create "Wp.Lang.builtin_types"
 
 let find_builtin name = Context.get builtin_types name
@@ -205,12 +209,14 @@ let find_builtin name = Context.get builtin_types name
 let adt lt =
   try match find_builtin lt.lt_name with
     | E_mdt m -> Mtype m
+    | E_why3(p,m,s) -> Wtype(p,m,s)
     | E_poly _ -> assert false
   with Not_found -> Atype lt
 
 let atype lt ts =
   try match find_builtin lt.lt_name with
     | E_mdt m -> Logic.Data(Mtype m,ts)
+    | E_why3(p,m,s) -> Logic.Data(Wtype(p,m,s),ts)
     | E_poly ftau -> ftau ts
   with Not_found -> Logic.Data(Atype lt,ts)
 
@@ -243,6 +249,8 @@ struct
     | Comp (c,KValue) -> basename (if c.cstruct then "S" else "U") c.corig_name
     | Comp (c,KInit) -> basename (if c.cstruct then "IS" else "IU") c.corig_name
     | Atype lt -> basename "A" lt.lt_name
+    | Wtype(_,_,s) ->
+      let rec base def = function [] -> def | w::ws -> base w ws in base "w" s
 
   let debug = function
     | Mtype a -> a.ext_debug
@@ -250,12 +258,14 @@ struct
     | Comp (c, KValue) -> comp_id c
     | Comp (c, KInit) -> comp_init_id c
     | Atype lt -> type_id lt
+    | Wtype(p,m,s) -> String.concat "." (p @ m :: s)
 
   let hash = function
     | Mtype a | Mrecord(a,_) -> FCHashtbl.hash a
     | Comp (c, KValue) -> Compinfo.hash c
     | Comp (c, KInit) -> 13 * Compinfo.hash c
     | Atype lt -> Logic_type_info.hash lt
+    | Wtype(p,m,s) -> Hashtbl.hash @@ (p @ m :: s)
 
   let compare a b =
     if a==b then 0 else
@@ -273,6 +283,9 @@ struct
       | Comp _ , _ -> (-1)
       | _ , Comp _ -> (+1)
       | Atype a , Atype b -> Logic_type_info.compare a b
+      | Atype _ , _ -> (-1)
+      | _ , Atype _ -> (+1)
+      | Wtype(p,m,s), Wtype(p',m',s') -> Stdlib.compare (p,m,s) (p',m',s')
 
   let equal a b = (compare a b = 0)
 
@@ -287,6 +300,7 @@ end
 let get_builtin_type ~name =
   match find_builtin name with
   | E_mdt m -> Mtype m
+  | E_why3(p,m,s) -> Wtype(p,m,s)
   | E_poly _ -> assert false
 
 let mem_builtin_type ~name =
@@ -303,6 +317,13 @@ let is_builtin_type ~name = function
         | _ -> false
       with Not_found -> false
     end
+  | Data(Wtype(p,m,s),_) ->
+    begin
+      try match find_builtin name with
+        | E_why3(p0,m0,s0) -> (p,m,s) = (p0,m0,s0)
+        | _ -> false
+      with Not_found -> false
+    end
   | _ -> false
 
 let datatype ~library name =
@@ -422,6 +443,7 @@ and lsymbol = {
 and source =
   | Generated of WpContext.context option * string
   | Extern of Engine.link extern
+  | Wsymbol of string list * string * string list (* package, module, name *)
 
 let lfun_observers = ref []
 let lfun_observe lf = List.iter (fun k -> k lf) !lfun_observers ; lf
@@ -563,6 +585,20 @@ let generated_p ?context ?(coloring=false) name =
 let extern_t name ~link ~library =
   new_extern ~link ~library ~debug:name
 
+let imported_t ~package ~theory ~name =
+  Wtype(package,theory,name)
+
+let imported_f ~package ~theory ~name
+    ?(params=[]) ?(result=Logic.Sprop) ?(typecheck=not_found) () =
+  lsymbol {
+    m_category = Logic.Function ;
+    m_params = params ;
+    m_result = result ;
+    m_typeof = typecheck ;
+    m_source = Wsymbol(package,theory,name) ;
+    m_coloring = false ;
+  }
+
 module Fun =
 struct
 
@@ -572,13 +608,16 @@ struct
     | ACSL f -> logic_id f
     | CTOR c -> ctor_id c
     | FUN({m_source=Generated(_,n)}) -> n
-    | FUN({m_source=Extern e})    -> e.ext_debug
+    | FUN({m_source=Extern e}) -> e.ext_debug
+    | FUN({m_source=Wsymbol(p,m,s)}) -> String.concat "." (p @ m :: s)
 
   let hash = function
     | ACSL f -> Logic_info.hash f
     | CTOR c -> Logic_ctor_info.hash c
     | FUN({m_source=Generated(_,n)}) -> Datatype.String.hash n
-    | FUN({m_source=Extern e})    -> e.ext_id
+    | FUN({m_source=Extern e}) -> e.ext_id
+    | FUN({m_source=Wsymbol(p,m,s)}) ->
+      Datatype.String.hash @@ String.concat "." (p @ m :: s)
 
   let compare_context c1 c2 =
     match c1 , c2 with
@@ -592,10 +631,14 @@ struct
     | Generated(m1,f1), Generated(m2,f2) ->
       let cmp = String.compare f1 f2 in
       if cmp<>0 then cmp else compare_context m1 m2
+    | Generated _, _ -> (-1)
+    | _, Generated _ -> (+1)
     | Extern f , Extern g ->
       ext_compare f g
-    | Generated _ , Extern _ -> (-1)
-    | Extern _ , Generated _ -> (+1)
+    | Extern _ , _ -> (-1)
+    | _ , Extern _ -> (+1)
+    | Wsymbol(p,m,s) , Wsymbol(p',m',s') ->
+      Stdlib.compare (p,m,s) (p',m',s')
 
   let compare f g =
     if f==g then 0 else
@@ -648,15 +691,20 @@ class virtual idprinting =
       | Comp(c, KValue) -> self#sanitize_type (comp_id c)
       | Comp(c, KInit) -> self#sanitize_type (comp_init_id c)
       | Atype lt -> self#sanitize_type (type_id lt)
+      | Wtype(p,m,s) -> String.concat "." (p @ m :: s)
+
     method field = function
       | Mfield(_,_,f,_) -> self#sanitize_field f
       | Cfield(f, KValue) -> self#sanitize_field (field_id f)
       | Cfield(f, KInit) -> self#sanitize_field (field_init_id f)
+
     method link = function
       | ACSL f -> Engine.F_call (self#sanitize_fun (logic_id f))
       | CTOR c -> Engine.F_call (self#sanitize_fun (ctor_id c))
       | FUN({m_source=Generated(_,n)}) -> Engine.F_call (self#sanitize_fun n)
       | FUN({m_source=Extern e}) -> e.ext_link
+      | FUN({m_source=Wsymbol(p,m,s)}) ->
+        Engine.F_call (String.concat "." (p @ m :: s))
   end
 
 let name_of_lfun = function
@@ -664,10 +712,11 @@ let name_of_lfun = function
   | CTOR c -> ctor_id c
   | FUN({m_source=Generated(_,f)}) -> f
   | FUN({m_source=Extern e}) -> e.ext_debug
+  | FUN({m_source=Wsymbol(p,m,s)}) -> String.concat "." (p @ m :: s)
 
 let context_of_lfun = function
   | ACSL _ | CTOR _
-  | FUN({m_source=Extern _}) -> None
+  | FUN({m_source=(Extern _|Wsymbol _)}) -> None
   | FUN({m_source=Generated(ctxt,_)}) -> ctxt
 
 let name_of_field = function
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index ecf24e45abda4f7f5c9b706c2d947915de152c0f..ffaef1011480e5802801f72860d2cf23da932d63 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -52,6 +52,7 @@ type adt = private
   | Mrecord of mdt * fields (** External record-type *)
   | Atype of logic_type_info (** Logic Type *)
   | Comp of compinfo * datakind (** C-code struct or union *)
+  | Wtype of string list * string * string list (** Why3 imported type *)
 
 (** name to print to the provers *)
 and mdt = string extern
@@ -68,7 +69,10 @@ and field = private
   | Cfield of fieldinfo * datakind
 and tau = (field,adt) Logic.datatype
 
-type t_builtin = E_mdt of mdt | E_poly of (tau list -> tau)
+type t_builtin =
+  | E_mdt of mdt
+  | E_why3 of string list * string * string list
+  | E_poly of (tau list -> tau)
 
 type lfun = private
   | ACSL of Cil_types.logic_info (** Registered in Definition.t,
@@ -89,6 +93,7 @@ and lsymbol = {
 and source =
   | Generated of WpContext.context option * string
   | Extern of Engine.link extern
+  | Wsymbol of string list * string * string list (** Why3 imported logic symbol *)
 
 val mem_builtin_type : name:string -> bool
 val is_builtin : logic_type_info -> bool
@@ -160,6 +165,16 @@ val generated_p : ?context:bool -> ?coloring:bool -> string -> lfun
 val extern_t:
   string -> link:string -> library:library -> mdt
 
+val imported_t:
+  package:string list -> theory:string -> name:string list -> adt
+
+val imported_f:
+  package:string list -> theory:string -> name:string list ->
+  ?params:sort list ->
+  ?result:sort ->
+  ?typecheck:(tau option list -> tau) ->
+  unit -> lfun
+
 (** {2 Sorting and Typing} *)
 
 val tau_of_object : c_object -> tau
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 1dc34ddc4a07f1d6417cd89e2801991361b549c8..04a00455df897c64bfaf69387c3efa477fb962c6 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -326,6 +326,18 @@ let add_builtin name kinds lfun =
   else
     Context.bind driver builtin_driver (register name kinds) phi
 
+let add_builtin_type name adt =
+  let bt =
+    match adt with
+    | Mtype m -> E_mdt m
+    | Wtype(p,m,s) -> E_why3(p,m,s)
+    | _ -> assert false
+  in
+  if Context.defined driver then
+    register_type name bt
+  else
+    Context.bind driver builtin_driver (register_type name) bt
+
 let add_type ?source name ~library ?link () =
   if Context.defined driver then
     add_type ?source name ~library ?link ()
diff --git a/src/plugins/wp/LogicBuiltins.mli b/src/plugins/wp/LogicBuiltins.mli
index c72bc193ea3fca22da719070643ab0d8bea9a49b..e573b4cb1b691f34b1458dfb2a577ddfbc5f604d 100644
--- a/src/plugins/wp/LogicBuiltins.mli
+++ b/src/plugins/wp/LogicBuiltins.mli
@@ -39,9 +39,14 @@ type kind =
 
 val kind_of_tau : tau -> kind
 
-(** Add a new builtin. This builtin will be shared with all created drivers *)
+(** Add a new builtin. This builtin will be shared with all created drivers. *)
 val add_builtin : string -> kind list -> lfun -> unit
 
+(** Add a new builtin type.
+    Must be an extern or imported type.
+    This builtin will be shared with all created drivers. *)
+val add_builtin_type : string -> adt -> unit
+
 type driver
 val driver: driver Context.value
 
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index de29014d0865e23b357e3572cea4879c96b58ce0..276394d7fe07b3a1c1d2dde806ac940729095717 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -22,8 +22,14 @@
 
 let dkey = Wp_parameters.register_category "prover"
 let dkey_pp_task = Wp_parameters.register_category "prover:pp_task"
-let dkey_api = Wp_parameters.register_category "why3_api"
-let dkey_model = Wp_parameters.register_category "why3_model"
+let dkey_compile =
+  Wp_parameters.register_category
+    ~help:"WP -> Why3 compilation"
+    "why3:compile"
+let dkey_model =
+  Wp_parameters.register_category
+    ~help:"Counter examples model variable"
+    "why3:model"
 
 let option_file = LogicBuiltins.create_option
     ~sanitizer:(fun ~driver_dir x -> Filename.concat driver_dir x)
@@ -56,10 +62,11 @@ let get_why3_conf = Conf.memoize
     begin fun () ->
       let config = Why3Provers.config () in
       let main = Why3.Whyconf.get_main config in
-      let ld =
-        (WpContext.directory () :> string)::
-        ((Wp_parameters.Share.get_dir "why3") :> string)::
-        (Why3.Whyconf.loadpath main) in
+      let ctx = (WpContext.directory () :> string) in
+      let wp = ((Wp_parameters.Share.get_dir "why3") :> string) in
+      let user = (Wp_parameters.Library.get () :> string list) in
+      let why3 = Why3.Whyconf.loadpath main in
+      let ld = ctx :: wp :: (user @ why3) in
       { env = Why3.Env.create_env ld ; config = main }
     end
 
@@ -141,13 +148,14 @@ let empty_cnv ?(polarity=`NoPolarity) (ctx:context) : convert = {
   convert_for_export = Lang.F.Tmap.empty;
 }
 
-
-let lfun_name (lfun:Lang.lfun) =
+let lfun_wname (lfun:Lang.lfun) =
   match lfun with
   | ACSL f -> Qed.Engine.F_call (Lang.logic_id f)
   | CTOR c -> Qed.Engine.F_call (Lang.ctor_id c)
   | FUN({m_source=Generated(_,n)}) -> Qed.Engine.F_call n
   | FUN({m_source=Extern e}) -> e.Lang.ext_link
+  | FUN({m_source=Wsymbol(p,m,s)}) ->
+    Qed.Engine.F_call (String.concat "." (p @ m :: s))
 
 let coerce ~cnv sort expected r =
   match sort, expected with
@@ -156,12 +164,13 @@ let coerce ~cnv sort expected r =
     t_app ~cnv ~f:["real"] ~l:"FromInt" ~p:["from_int"] [r]
   | _ -> r
 
-let name_of_adt = function
+let adt_wname = function
   | Lang.Mtype a -> a.Lang.ext_link
   | Mrecord(a,_) -> a.Lang.ext_link
   | Comp (c, KValue) -> Lang.comp_id c
   | Comp (c, KInit) -> Lang.comp_init_id c
   | Atype lt -> Lang.type_id lt
+  | Wtype(p,m,s) -> String.concat "." (p @ m :: s)
 
 let tvar =
   let tvar = Datatype.Int.Hashtbl.create 10 in
@@ -169,8 +178,7 @@ let tvar =
     Datatype.Int.Hashtbl.memo tvar i
       (fun i ->
          let id = Why3.Ident.id_fresh (Printf.sprintf "a%i" i) in
-         Why3.Ty.create_tvsymbol id
-      )
+         Why3.Ty.create_tvsymbol id)
 
 
 (** Sharing *)
@@ -216,6 +224,16 @@ let wp_why3_lib library =
 
 (* conversion *)
 
+let of_adt ~cnv = function
+  | Lang.Wtype(f,l,p) -> get_ts ~cnv ~f ~l ~p
+  | adt ->
+    let s = adt_wname adt in
+    try Hashtbl.find cnv.incomplete_types s
+    with Not_found ->
+    try Why3.Theory.(ns_find_ts (get_namespace cnv.th) (cut_path s))
+    with Not_found ->
+      why3_failure "Can't find type '%s' in why3 namespace" s
+
 let rec of_tau ~cnv (t:Lang.F.tau) =
   match t with
   | Prop -> None
@@ -225,18 +243,9 @@ let rec of_tau ~cnv (t:Lang.F.tau) =
   | Array(k,v) ->
     let ts = get_ts ~cnv ~f:["map"] ~l:"Map" ~p:["map"] in
     Some (Why3.Ty.ty_app ts [Option.get (of_tau ~cnv k); Option.get (of_tau ~cnv v)])
-  | Data(adt,l) -> begin
-      let s = name_of_adt adt in
-      let find s =
-        try Hashtbl.find cnv.incomplete_types s
-        with Not_found ->
-          Why3.Theory.(ns_find_ts (get_namespace cnv.th) (cut_path s))
-      in
-      match find s with
-      | ts -> Some (Why3.Ty.ty_app ts (List.map (fun e -> Option.get (of_tau ~cnv e)) l))
-      | exception Not_found ->
-        why3_failure "Can't find type '%s' in why3 namespace" s
-    end
+  | Data(adt,l) ->
+    let ts = of_adt ~cnv adt in
+    Some (Why3.Ty.ty_app ts (List.map (fun e -> Option.get (of_tau ~cnv e)) l))
   | Tvar i -> Some (Why3.Ty.ty_var (tvar i))
   | Record _ ->
     why3_failure "Type %a not (yet) convertible" Lang.F.pp_tau t
@@ -333,7 +342,7 @@ let rec of_trigger ~cnv t =
   | TgSet(m,k,v) ->
     t_app ~cnv ~f:["map"] ~l:"Map" ~p:["set"] [of_trigger ~cnv m;of_trigger ~cnv k;of_trigger ~cnv v]
   | TgFun (f,l) -> begin
-      match lfun_name f with
+      match lfun_wname f with
       | F_call s ->
         let ls = Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) in
         Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger ~cnv e) l)
@@ -341,7 +350,7 @@ let rec of_trigger ~cnv t =
     end
   | TgProp (f,l) ->
     begin
-      match lfun_name f with
+      match lfun_wname f with
       | F_call s ->
         let ls = Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) in
         Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger ~cnv e) l)
@@ -354,7 +363,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
     with Not_found ->
       why3_failure "@[<hov 2>Untyped term: %a@]" Lang.F.pp_term t
   in
-  Wp_parameters.debug ~dkey:dkey_api
+  Wp_parameters.debug ~dkey:dkey_compile
     "of_term %a:%a (expected %a)@."
     Lang.F.pp_term t Lang.F.Tau.pretty sort Lang.F.Tau.pretty expected
   ;
@@ -504,6 +513,10 @@ let rec of_term ~cnv expected t : Why3.Term.term =
       coerce ~cnv sort expected $
       t_app' ~cnv ~f:["map"] ~l:"Const" ~p:["const"] [of_term ~cnv vsort v] (of_tau ~cnv sort)
     (* Generic *)
+    | Fun (FUN({m_source=Wsymbol(f,l,p)}),ls), tau, expected ->
+      coerce ~cnv sort expected $
+      t_app' ~cnv ~f ~l ~p (List.map (of_term' cnv) ls) (of_tau ~cnv tau)
+
     | Fun (f,l), _, _ -> begin
         let t_app ls l r  =
           Why3.Term.t_app ls l r
@@ -515,18 +528,13 @@ let rec of_term ~cnv expected t : Why3.Term.term =
               Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s))
           in
           match find s, expected with
-          | ls, (Prop | Bool) ->
-            coerce ~cnv sort expected $
-            t_app ls l (of_tau ~cnv sort)
-          | ls, _ ->
-            coerce ~cnv sort expected $
-            t_app ls l (of_tau ~cnv sort)
+          | ls, _ -> coerce ~cnv sort expected $ t_app ls l (of_tau ~cnv sort)
           | exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
         in
         let apply_from_ns' s l =
           apply_from_ns s (List.map (fun e -> of_term' cnv e) l)
         in
-        match lfun_name f, expected with
+        match lfun_wname f, expected with
         | F_call s, _ -> apply_from_ns' s l sort
         | Qed.Engine.F_subst (s, _), _ -> apply_from_ns' s l sort
         | Qed.Engine.F_left s, _ | Qed.Engine.F_assoc s, _ ->
@@ -591,7 +599,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
           Why3.Term.t_app ls l (of_tau ~cnv expected)
         | exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
       end
-    | (Rdef _, Data ((Mtype _|Mrecord (_, _)|Atype _), _), _)
+    | (Rdef _, Data ((Mtype _|Mrecord (_, _)|Atype _|Wtype _), _), _)
     | (Rdef _, (Prop|Bool|Int|Real|Tvar _|Array (_, _)), _)
     | (Aset (_, _, _), (Prop|Bool|Int|Real|Tvar _|Record _|Data (_, _)), _)
     | (Neq (_, _), _, (Int|Real|Tvar _|Array (_, _)|Record _|Data (_, _)))
@@ -745,7 +753,7 @@ class visitor (ctx:context) c =
 
     method on_cluster c =
       let name = Definitions.cluster_id c in
-      Wp_parameters.debug ~dkey:dkey_api "Start on_cluster %s@." name;
+      Wp_parameters.debug ~dkey:dkey_compile "Start on_cluster %s@." name;
       let th_name = String.capitalize_ascii name in
       let thy =
         let age = try fst (CLUSTERS.find c) with Not_found -> (-1) in
@@ -773,9 +781,11 @@ class visitor (ctx:context) c =
       let th = Why3.Theory.open_scope th name in
       let th = Why3.Theory.use_export th thy in
       let th = Why3.Theory.close_scope th ~import:true in
-      Wp_parameters.debug ~dkey:dkey_api "End  on_cluster %s@." name;
+      Wp_parameters.debug ~dkey:dkey_compile "End  on_cluster %s@." name;
       ctx.th <- th
 
+    method on_theory file thy =
+      self#add_import_use ~import:false file thy ("W_" ^ thy)
 
     method section _ = ()
 
@@ -793,7 +803,7 @@ class visitor (ctx:context) c =
       self#add_import_use ~import:false file thy name
 
     method add_import_use ~import file thy name =
-      Wp_parameters.debug ~dkey:dkey_api
+      Wp_parameters.debug ~dkey:dkey_compile
         "@[use@ %s@ @[%a.%s@]@ as@ %s@]"
         (if import then "import" else "")
         Why3.Pp.(print_list (Why3.Pp.constant_string ".") string) file
@@ -972,13 +982,13 @@ class visitor (ctx:context) c =
         ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl
 
     method on_dfun d =
-      Wp_parameters.debug ~dkey:dkey_api "Define %a@." Lang.Fun.pretty d.d_lfun ;
+      Wp_parameters.debug ~dkey:dkey_compile "Define %a@." Lang.Fun.pretty d.d_lfun ;
       let cnv = empty_cnv ctx in
       List.iter (Lang.F.add_var cnv.pool) d.d_params;
       begin
         match d.d_definition with
         | Logic t ->
-          let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_name d.d_lfun)) in
+          let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_wname d.d_lfun)) in
           let map e = Option.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
           let ty_args = List.map map d.d_params in
           let id = Why3.Term.create_lsymbol id ty_args (of_tau ~cnv t) in
@@ -987,7 +997,7 @@ class visitor (ctx:context) c =
         | Function(t,mu,v) -> begin
             match mu with
             | Rec -> (* transform recursive function into an axioms *)
-              let name = Qed.Export.link_name (lfun_name d.d_lfun) in
+              let name = Qed.Export.link_name (lfun_wname d.d_lfun) in
               let id = Why3.Ident.id_fresh name in
               let map e = Option.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
               let ty_args = List.map map d.d_params in
@@ -1011,7 +1021,7 @@ class visitor (ctx:context) c =
                   t in
               ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
             | Def ->
-              let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_name d.d_lfun)) in
+              let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_wname d.d_lfun)) in
               let map e = Option.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
               let ty_args = List.map map d.d_params in
               let result = of_tau ~cnv t in
@@ -1025,7 +1035,7 @@ class visitor (ctx:context) c =
         | Predicate(mu,p) -> begin
             match mu with
             | Rec ->
-              let name = Qed.Export.link_name (lfun_name d.d_lfun) in
+              let name = Qed.Export.link_name (lfun_wname d.d_lfun) in
               let id = Why3.Ident.id_fresh name in
               let map e = Option.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
               let ty_args = List.map map d.d_params in
@@ -1048,7 +1058,7 @@ class visitor (ctx:context) c =
                   t in
               ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
             | Def ->
-              let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_name d.d_lfun)) in
+              let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_wname d.d_lfun)) in
               let map e = Option.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
               let ty_args = List.map map d.d_params in
               let id = Why3.Term.create_lsymbol id ty_args None in
@@ -1060,7 +1070,7 @@ class visitor (ctx:context) c =
           end
         | Inductive dl ->
           (* create predicate symbol *)
-          let fname = Qed.Export.link_name (lfun_name d.d_lfun) in
+          let fname = Qed.Export.link_name (lfun_wname d.d_lfun) in
           let id = Why3.Ident.id_fresh fname in
           let map e = Option.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
           let ty_args = List.map map d.d_params in
@@ -1128,7 +1138,7 @@ let prove_goal ~id ~title ~name ?axioms ?(probes=Probe.Map.empty) t =
   let goal = Definitions.cluster ~id ~title () in
   let ctx = empty_context name in
   let v = new visitor ctx goal in
-  Wp_parameters.debug ~dkey:dkey_api "%t"
+  Wp_parameters.debug ~dkey:dkey_compile "%t"
     begin fun fmt ->
       Format.fprintf fmt "---------------------------------------------@\n" ;
       Format.fprintf fmt "EXPORT GOAL %s@." id ;
@@ -1565,7 +1575,7 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ?memlimit
         automated ~config ~probes ~timeout ~steplimit ~memlimit
           wpo pconf drv prover task
   with exn ->
-    if Wp_parameters.has_dkey dkey_api then
+    if Wp_parameters.has_dkey dkey_compile then
       Wp_parameters.fatal "[Why3 Error] %a@\n%s"
         Why3.Exn_printer.exn_printer exn
         Printexc.(raw_backtrace_to_string @@ get_raw_backtrace ())
diff --git a/src/plugins/wp/TacLemma.ml b/src/plugins/wp/TacLemma.ml
index 453e9daee5b0b6f0ce044d1ec9b19dea9fc27aa1..95c80612f99197e7e176e951ad323646ffe58f67 100644
--- a/src/plugins/wp/TacLemma.ml
+++ b/src/plugins/wp/TacLemma.ml
@@ -44,6 +44,7 @@ class browser ?on_cluster f cluster =
     inherit Definitions.visitor cluster
     method section _ = ()
     method on_library _ = ()
+    method on_theory _ _ = ()
     method on_type _ _ = ()
     method on_comp _ _ = ()
     method on_icomp _ _ = ()
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index aecbcbb948e002381fda63b4ea7c5d3d508a4f25..fc5178e0d55e3cab3654112bbe2faa72dc375738 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -29,19 +29,22 @@ module T = Why3.Theory
 module F = Filepath.Normalized
 module W = Why3
 module WConf = Why3.Whyconf
+module LB = LogicBuiltins
+module LT = Logic_typing
 
-let dkey = L.register_category "why3.import"
+let dkey =
+  L.register_category
+    ~help:"Importer Why3 -> ACSL"
+    "why3:import"
 
 (* -------------------------------------------------------------------------- *)
 (* ---    Why3 Environment                                                --- *)
 (* -------------------------------------------------------------------------- *)
 
-let create_why3_env loadpath =
+let why3_env loadpath =
   let main = WConf.get_main @@ WConf.read_config None in
   W.Env.create_env @@ WConf.loadpath main @ F.to_string_list loadpath
 
-
-
 let extract_path thname =
   let segments = String.split_on_char '.' thname in
   match List.rev segments with
@@ -59,57 +62,24 @@ let of_infix s =
       else unwrap_any s others
   in unwrap_any s ["prefix ";"infix ";"mixfix "]
 
-let construct_acsl_name (id : W.Ident.ident) =
-  let (paths,name,scopes) = T.restore_path id in
-  match List.rev scopes with
+let acsl_name (id : W.Ident.ident) =
+  let (path,name,scope) = T.restore_path id in
+  match List.rev scope with
   | (t::q) ->
-    String.concat "::" (paths @ name :: List.rev_append q [of_infix t])
+    String.concat "::" (path @ name :: List.rev_append q [of_infix t])
   | [] -> ""
 
-(* For debug only*)
-let pp_id fmt (id: W.Ident.ident) =
-  Format.pp_print_string fmt id.id_string
-
-(* For debug only*)
-let pp_tys fmt (tys: W.Ty.tysymbol) =
-  W.Pretty.print_ty_decl fmt tys
-
-(* For debug only*)
-let pp_ls fmt ls =
-  W.Pretty.print_ls fmt ls
-
-(* For debug only*)
-let pp_id_loc fmt (id : W.Ident.ident) =
-  match id.id_loc with
-  | Some loc -> W.Loc.pp_position fmt loc
-  | None -> L.error "No location found"
-
-(* For debug only*)
-let pp_lti fmt (lti : C.logic_type_info) =
-  Cpp.pp_logic_type_info fmt lti
-
-(* For debug only*)
-let pp_li fmt (li : C.logic_info) =
-  Cpp.pp_logic_info fmt li
-
-(* For debug only*)
-let pp_lvs fmt (lvs : C.logic_var list) =
-  List.iter (fun (lv: C.logic_var) ->
-      Format.fprintf fmt "@ %a: %a"
-        Cpp.pp_logic_var lv Cpp.pp_logic_type lv.lv_type
-    ) lvs
+let pp_id fmt (id: W.Ident.ident) = Format.pp_print_string fmt id.id_string
 
 (* -------------------------------------------------------------------------*)
 (* ---    Types                                                           - *)
 (* -------------------------------------------------------------------------*)
 
-
 type tvars = C.logic_type W.Ty.Mtv.t
 
 type why3module = {
-  paths : string list;
-  types : C.logic_type_info list;
-  logics : C.logic_info list;
+  types : (C.logic_type_info * C.location) list;
+  logics : (C.logic_info * C.location) list;
 }
 
 type env = {
@@ -117,22 +87,24 @@ type env = {
   tenv : C.logic_type_info W.Ty.Hts.t;
   lenv : C.logic_info W.Term.Hls.t;
   lils : W.Term.lsymbol Logic_info.Hashtbl.t;
-  ltits : W.Ty.tysymbol Logic_type_info.Hashtbl.t;
-  menv : why3module Datatype.String.Hashtbl.t
+  lcts : W.Term.lsymbol Logic_ctor_info.Hashtbl.t;
+  ltts : W.Ty.tysymbol Logic_type_info.Hashtbl.t;
+  menv : why3module Datatype.String.Hashtbl.t;
 }
 
 type menv = {
-  mutable lti : C.logic_type_info list;
-  mutable li : C.logic_info list;
+  mutable lti : (C.logic_type_info * C.location) list;
+  mutable li : (C.logic_info * C.location) list;
 }
 
-let create_empty_env wenv =
+let create wenv =
   let tenv  = W.Ty.Hts.create 0 in
   let lenv  = W.Term.Hls.create 0 in
   let lils  = Logic_info.Hashtbl.create 0 in
-  let ltits  = Logic_type_info.Hashtbl.create 0 in
+  let lcts  = Logic_ctor_info.Hashtbl.create 0 in
+  let ltts  = Logic_type_info.Hashtbl.create 0 in
   let menv  = Datatype.String.Hashtbl.create 0 in
-  { wenv; tenv; lenv; lils; ltits; menv }
+  { wenv; tenv; lenv; lils; lcts; ltts; menv }
 
 (* -------------------------------------------------------------------------- *)
 (* ---    Built-in                                                        --- *)
@@ -153,11 +125,32 @@ let add_builtins env =
   begin
     let ts_list = find_ts env ["list"] "List" ["list"] in
     let ts_set = find_ts env ["set"] "Set" ["set"] in
-    add_builtin env.tenv W.Ty.ts_bool Utf8_logic.boolean [];
     add_builtin env.tenv ts_list "\\list" ["A"];
     add_builtin env.tenv ts_set "set" ["A"];
   end
 
+(* -------------------------------------------------------------------------- *)
+(* ---    Location handling                                               --- *)
+(* -------------------------------------------------------------------------- *)
+
+let convert_location (wloc : Why3.Loc.position option) : C.location =
+  match wloc with
+  | Some loc ->
+    let (file,lstart,cstart,lend,cend) = Why3.Loc.get loc in
+    let pstart = {
+      Filepath.pos_path = F.of_string file;
+      pos_lnum = lstart;
+      pos_bol = 0;
+      pos_cnum = cstart;
+    }  in
+    let pend = {
+      Filepath.pos_path = F.of_string file;
+      pos_lnum = lend;
+      pos_bol = 0;
+      pos_cnum = cend;
+    } in (pstart, pend)
+  | None ->
+    (Position.unknown, Position.unknown)
 
 (* -------------------------------------------------------------------------- *)
 (* ---    Type conversion                                                 --- *)
@@ -172,158 +165,204 @@ let tvars_of_txs (txs: W.Ty.tvsymbol list) : string list * tvars =
        x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
     ) txs ([], W.Ty.Mtv.empty)
 
-let rec lt_of_ty (env : env) (menv) (tvs : tvars)  (ty: W.Ty.ty) : C.logic_type =
+let rec lt_of_ty env menv (tvs : tvars)  (ty: W.Ty.ty) : C.logic_type =
   match ty.ty_node with
   | Tyvar x -> W.Ty.Mtv.find x tvs
   | Tyapp(s,[]) when W.Ty.(ts_equal s ts_int) -> C.Linteger
   | Tyapp(s,[]) when W.Ty.(ts_equal s ts_real) -> C.Lreal
-  | Tyapp(s,ts) -> C.Ltype( lti_of_ts env menv s ,
-                            List.map (lt_of_ty env menv tvs ) ts)
+  | Tyapp(s,[]) when W.Ty.(ts_equal s ts_bool) -> C.Lboolean
+  | Tyapp(s,ts) ->
+    C.Ltype(lt_of_ts env menv s [], List.map (lt_of_ty env menv tvs ) ts)
 
-and lti_of_ts (env : env) (menv : menv) (ts : W.Ty.tysymbol) : C.logic_type_info =
+and lt_of_ts env menv (ts : W.Ty.tysymbol) (cs: W.Decl.constructor list) : C.logic_type_info =
   try W.Ty.Hts.find env.tenv ts with Not_found ->
-    let (lt_params,tvars) = tvars_of_txs ts.ts_args in
-    let lt_def =
-      match ts.ts_def with
-      | NoDef | Range _ | Float _ -> None
-      | Alias ty -> Some (C.LTsyn (lt_of_ty env menv tvars ty))
-    in
-    let lti =
-      C.{
-        lt_name =  construct_acsl_name ts.ts_name;
-        lt_params ; lt_def ;
-        lt_attr = [];
-      }
-    in W.Ty.Hts.add env.tenv ts lti ;
-    menv.lti <- lti :: menv.lti;
-    Logic_type_info.Hashtbl.add env.ltits lti ts;
+    let lt_params,tvars = tvars_of_txs ts.ts_args in
+    let lt_name = acsl_name ts.ts_name in
+    let lti = C.{ lt_name ; lt_params ; lt_def = None ; lt_attr = []; } in
+    lti.lt_def <-
+      (match ts.ts_def with
+       | Range _ | Float _ -> None
+       | NoDef -> Some (C.LTsum (List.map (cli_of_constr env menv lti) cs))
+       | Alias ty -> Some (C.LTsyn (lt_of_ty env menv tvars ty))
+      );
+    W.Ty.Hts.add env.tenv ts lti ;
+    menv.lti <- (lti, (convert_location ts.ts_name.id_loc) ) :: menv.lti;
+    Logic_type_info.Hashtbl.add env.ltts lti ts;
     lti
 
+and cli_of_constr env menv ctor_type (ls, _: W.Decl.constructor) : C.logic_ctor_info =
+  let _,tvars =
+    tvars_of_txs @@ W.Ty.Stv.elements @@  W.Term.ls_ty_freevars ls in
+  let l_profile = List.mapi (lv_of_ty env menv tvars ) ls.ls_args in
+  let ctor_params = List.map ( fun (lv:C.logic_var) -> lv.lv_type) l_profile in
+  let ctor_name = acsl_name ls.ls_name in
+  let ctor = Cil_types.{ ctor_name ; ctor_type ; ctor_params } in
+  Logic_ctor_info.Hashtbl.add env.lcts ctor ls ;
+  ctor
+
 (* -------------------------------------------------------------------------- *)
 (* ---    Functions conversion                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
-let lv_of_ty (env:env) (menv : menv) (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
+and lv_of_ty env menv (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
   Cil_const.make_logic_var_formal (Printf.sprintf "x%d" index)
   @@ (lt_of_ty env menv tvars ty)
 
-let lt_of_ty_opt (lt_opt) =
+and lt_of_ty_opt (lt_opt) =
   match lt_opt with
   | None -> C.Ctype (C.TVoid []) (* Same as logic_typing *)
   | Some tr -> tr
 
-let li_of_ls (env:env) (menv : menv) (ls : W.Term.lsymbol)  : C.logic_info =
+let li_of_ls env menv (ls : W.Term.lsymbol) : C.logic_info =
   let l_tparams,tvars =
     tvars_of_txs @@ W.Ty.Stv.elements @@  W.Term.ls_ty_freevars ls in
   let l_type = Option.map (lt_of_ty  env menv tvars ) ls.ls_value in
   let l_profile = List.mapi (lv_of_ty env menv tvars ) ls.ls_args in
   let l_args = List.map ( fun (lv:C.logic_var) -> lv.lv_type) l_profile in
-  let signature = C.Larrow (l_args, lt_of_ty_opt l_type) in
-  let li =
-    C.{
-      l_var_info = Cil_const.make_logic_var_global
-          (construct_acsl_name ls.ls_name)
-          signature;
-      l_labels = [];
-      l_tparams;
-      l_type;
-      l_profile ;
+  let l_result = lt_of_ty_opt l_type in
+  let l_params = if l_args = [] then l_result else C.Larrow (l_args, l_result) in
+  let l_name = acsl_name ls.ls_name in
+  let lv = Cil_const.make_logic_var_global l_name l_params in
+  let li = C.{
+      l_var_info = lv ;
+      l_labels = []; l_tparams; l_type; l_profile ;
       l_body = C.LBnone;
     } in W.Term.Hls.add env.lenv ls li;
-  menv.li <- li :: menv.li;
+  menv.li <- (li, (convert_location ls.ls_name.id_loc) ):: menv.li;
   Logic_info.Hashtbl.add env.lils li ls; li
 
+let add_ts env menv (ts : W.Ty.tysymbol) (cs: W.Decl.constructor list)=
+  L.debug ~dkey "Importing type %a: %s" pp_id ts.ts_name (acsl_name ts.ts_name);
+  ignore @@ lt_of_ts env menv ts cs
+let add_ls env menv (ls : W.Term.lsymbol) =
+  L.debug ~dkey "Importing logic %a: %s" pp_id ls.ls_name (acsl_name ls.ls_name);
+  ignore @@ li_of_ls env menv ls
+
 (* -------------------------------------------------------------------------- *)
 (* ---    Theory                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let import_theory (env : env) thname =
-  let theory_name, theory_path = extract_path thname in
-  try
-    let menv : menv = {li = []; lti = []} in
-    let theory = W.Env.read_theory env.wenv theory_path theory_name in
+let get_theory env (theory_name) (theory_path) =
+  try W.Env.read_theory env.wenv theory_path theory_name
+  with W.Env.LibraryNotFound _ ->
+    L.error "Library %s not found" theory_name; W.Theory.ignore_theory
+
+let parse_theory env (theory:W.Theory.theory) (menv) =
+  begin
     List.iter (fun (tdecl : T.tdecl) ->
         match tdecl.td_node with
         | Decl decl ->
           begin
             match decl.d_node with
-            | Dtype ts ->
-              L.debug ~dkey "Decl and type %a"  pp_id ts.ts_name;
-              L.debug ~dkey "Location %a"  pp_id_loc ts.ts_name;
-              let lti =  lti_of_ts env menv ts in
-              L.debug ~dkey "Correspondign LTI %a" pp_lti lti;
-            | Ddata ddatas ->
-              List.iter
-                (fun ((ts, _) : W.Decl.data_decl) ->
-                   L.debug ~dkey "Decl and data %a" pp_id  ts.ts_name;
-                   L.debug ~dkey "Location %a"  pp_id_loc ts.ts_name;
-                   let lti =  lti_of_ts env menv ts  in
-                   L.debug ~dkey "Correspondign data LTI %a" pp_lti lti;
-                ) ddatas
-            | Dparam ls ->
-              L.debug ~dkey "Decl and dparam %a" pp_id ls.ls_name;
-              L.debug ~dkey "Location %a"  pp_id_loc ls.ls_name
-            | Dlogic dlogics ->
-              List.iter
-                (fun ((ls,_):W.Decl.logic_decl) ->
-                   L.debug ~dkey "Decl and dlogic %a" pp_id ls.ls_name;
-                   L.debug ~dkey "Location %a"  pp_id_loc ls.ls_name;
-                   let li = li_of_ls env menv ls in
-                   L.debug ~dkey "Corresponding dlogic LTI %a" pp_li li;
-                ) dlogics
-            | _ -> L.debug ~dkey "Other type of Decl"
+            | Dtype ts -> add_ts env menv ts []
+            | Dparam ls -> add_ls env menv ls
+            | Ddata ds -> List.iter (fun (ts, cs) -> add_ts env menv ts cs) ds
+            | Dlogic ds -> List.iter (fun (ls,_) -> add_ls env menv ls) ds
+            | Dind (_,ds) -> List.iter (fun (ls,_) -> add_ls env menv ls) ds
+            | Dprop _ -> ()
           end
-        | Use _| Clone _| Meta _ -> L.debug ~dkey ""
+        | Use _ | Clone _ | Meta _ -> ()
       ) theory.th_decls;
-    Datatype.String.Hashtbl.add env.menv thname
-      { logics =  List.rev menv.li;
-        types = List.rev menv.lti;
-        paths = theory_path };
-  with W.Env.LibraryNotFound _ ->
-    L.error "Library %s not found" thname
+  end
+
+let kind_of_lt (lt : C.logic_type) : LB.kind =
+  match lt with
+  | C.Linteger -> LB.Z
+  | C.Lreal -> LB.R
+  | C.Lboolean -> LB.B
+  | _ -> LB.A
+
+let sort_of_lt (lt : C.logic_type) : Qed.Logic.sort =
+  match lt with
+  | C.Linteger -> Qed.Logic.Sint
+  | C.Lreal -> Qed.Logic.Sreal
+  | _ -> Qed.Logic.Sdata
+
+let sort_of_result = function
+  | Some lt -> sort_of_lt lt
+  | None -> Qed.Logic.Sprop
+
+let register_builtin env m =
+  begin
+    let add_builtin (ls: W.Term.lsymbol) acsl_name profile result =
+      let (package, theory, name) = T.restore_path ls.ls_name in
+      let kinds = List.map kind_of_lt profile in
+      let params = List.map sort_of_lt profile in
+      LB.add_builtin acsl_name kinds @@
+      Lang.imported_f ~package ~theory ~name ~params ~result  ()
+    in
+    let add_builtin_li li =
+      let ls = Logic_info.Hashtbl.find env.lils li in
+      let profile = List.map (fun lv -> lv.C.lv_type) li.l_profile in
+      let result = sort_of_result li.l_type in
+      add_builtin ls li.l_var_info.lv_name profile result
+    in
+    let add_builtin_ctor ctor =
+      let ls = Logic_ctor_info.Hashtbl.find env.lcts ctor in
+      let profile = ctor.Cil_types.ctor_params in
+      let result = Qed.Logic.Sdata in
+      add_builtin ls ctor.ctor_name profile result
+    in
+    let add_builtin_t lti =
+      let ty = Logic_type_info.Hashtbl.find env.ltts lti in
+      let (package,theory,name) = T.restore_path ty.ts_name in
+      LB.add_builtin_type lti.lt_name @@
+      Lang.imported_t ~package ~theory ~name ;
+      begin match lti.lt_def with
+        | Some C.LTsum ctors -> List.iter add_builtin_ctor ctors
+        | _ -> ()
+      end
+    in
+    List.iter (fun (lti, _) -> add_builtin_t lti) m.types;
+    List.iter (fun (li, _) -> add_builtin_li li) m.logics;
+  end
+
+let import_theory env thname =
+  try
+    Datatype.String.Hashtbl.find env.menv thname
+  with Not_found ->
+    L.debug ~dkey "Parsing Why3 theory %s.@." thname ;
+    let theory_name, theory_path = extract_path thname in
+    let menv : menv = {li = []; lti = []} in
+    let theory = get_theory env theory_name theory_path in
+    parse_theory env theory menv;
+    let m = { types = List.rev menv.lti; logics =  List.rev menv.li } in
+    Datatype.String.Hashtbl.add env.menv thname m;
+    register_builtin env m; m
 
 (* -------------------------------------------------------------------------- *)
-(* ---    Main                                                            --- *)
+(* ---    Module registration                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
-let () =
-  Boot.Main.extend
-    begin fun () ->
-      let libs = L.Library.get() in
-      let imports = L.Import.get() in
-      if libs <> [] || imports <> [] then
-        begin
-          let wenv = create_why3_env @@ libs in
-          let env : env = create_empty_env wenv in
-          add_builtins env;
-          List.iter (import_theory env) @@ imports;
-          W.Ty.Hts.iter (fun (tys) (lti) ->
-              L.result "Why3 type symbol : %a" pp_tys tys;
-              L.result "Corresponding CIL logic type info %a" pp_lti lti;
-            ) env.tenv;
-          W.Term.Hls.iter (fun (ls) (li) ->
-              L.result "Why3 logic symbol : %a" pp_ls ls;
-              L.result "Corresponding CIL logic info : %a" pp_li li;
-              L.result "Associated parameters : @[<hov2>%a@]" pp_lvs li.l_profile;
-            ) env.lenv;
-          Datatype.String.Hashtbl.iter (fun (s) (why3mod) ->
-              L.result "@[Module %s at %s@]" s (String.concat "::" why3mod.paths);
-              List.iter (fun (li) ->
-                  L.result "Logic : @[<hov1>%a@]" pp_li li)
-                why3mod.logics;
-              List.iter (fun (lti) ->
-                  L.result "Type : @[<hov1>%a@]" pp_lti lti)
-                why3mod.types;
-            ) env.menv;
-          Logic_type_info.Hashtbl.iter ( fun (lti) (ts) ->
-              L.result "Logic type info : %a is associated to ts : %a "
-                pp_lti lti pp_tys ts )
-            env.ltits;
-          Logic_info.Hashtbl.iter ( fun (li) (ls) ->
-              L.result "Logic info %a is associated to ls : %a "
-                pp_li li pp_ls ls )
-            env.lils;
-        end
+module Env = WpContext.StaticGenerator
+    (Datatype.Unit)
+    (struct
+      type key = unit
+      type data = env
+      let name = "Wp.Why3Import.Env"
+      let compile () =
+        let env = create @@ why3_env @@ L.Library.get () in
+        add_builtins env ; env
+    end)
+
+let importer (ctxt: LT.module_builder) (_: C.location) (m: string list) =
+  begin
+    L.debug ~dkey "Importing Why3 theory %s.@." (String.concat "::" m) ;
+    let thname = String.concat "." m in
+    let m = import_theory (Env.get ()) thname in
+    List.iter (fun (lti,loc) -> ctxt.add_logic_type loc lti) m.types ;
+    List.iter (fun (li, loc) -> ctxt.add_logic_function loc li) m.logics ;
+  end
+
+let registered = ref false
+
+let register () =
+  if not !registered then
+    begin
+      registered := true ;
+      Acsl_extension.register_module_importer ~plugin:"wp" "why3" importer ;
     end
 
+let () = Cmdline.run_after_extended_stage register
+
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/doc/.gitignore b/src/plugins/wp/doc/.gitignore
index bfe2e4d25500d764b549b9e6dfd00ae71d137617..28c4dfcc0ceb3c64c16e16bd9784bf716063f224 100644
--- a/src/plugins/wp/doc/.gitignore
+++ b/src/plugins/wp/doc/.gitignore
@@ -3,3 +3,4 @@ frama-c-affiliation.tex
 cealistlogo.jpg
 feedback
 /html
+/manual/wp.synctex.gz
diff --git a/src/plugins/wp/doc/manual/wp_builtins.tex b/src/plugins/wp/doc/manual/wp_builtins.tex
index 5c04a947a4d802c007d8814f5814ba2cb43a10ad..6a98a84396319b1367bd7633dbfd8b1561ea04d7 100644
--- a/src/plugins/wp/doc/manual/wp_builtins.tex
+++ b/src/plugins/wp/doc/manual/wp_builtins.tex
@@ -247,6 +247,9 @@ $x$ and $y$ are finite, but obey IEEE semantics for infinities and NaNs
 
 \section{Custom Extensions}
 
+\paragraph{DEPRECATED.} You shall import a Why3 module instead of using custom
+drivers. See Section~\ref{importer} for details.
+
 As explained in Section~\ref{drivers}, it is possible to extend all the properties mentioned
 above. Section~\ref{wp-custom-tactics} also provides hints on how to define tactics that can be
 used in the interactive prover of \textsf{Frama-C/WP}.
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index c2a27e1a29737f1ddcf0eb77f4640726acb44c94..9ef08aa6f42d1444ebd31184d72dac4912dc1ade 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1651,6 +1651,9 @@ procedures thanks to the following option:
 \subsection{Linking \textsf{ACSL} Symbols to External Libraries}
 \label{drivers}
 
+\paragraph{DEPRECATED.} You shall now import a Why3 module
+instead of using custom drivers. See Section~\ref{importer} for details.
+
 Besides additional proof libraries, it is also possible to
 \emph{link} declared \textsf{ACSL} symbols to external or predefined
 symbols. In such case, the corresponding \textsf{ACSL} definitions,
@@ -1660,7 +1663,6 @@ External linkage is specified in \emph{driver files}. It is possible
 to load one or several drivers with the following \textsf{WP} plug-in option:
 \begin{description}
 \item[\tt -wp-driver <file,\ldots>] load specified driver files.
-
 \end{description}
 
 \newcommand{\ccc}{\texttt{,}\ldots\texttt{,}}
@@ -1782,6 +1784,48 @@ by a link (`\user{link};'). The available tags are depicted on figure~\ref{wp-dr
 \label{wp-driver-tags}
 \end{figure}
 
+\pagebreak
+\subsection{Importing Why3 Modules}
+\label{importer}
+
+The \textsf{WP} plug-in provides an \textsf{ACSL} module importer that
+can import \textsf{Why3} theories and modules into \textsf{ACSL}.
+See \textsf{Frama-C} user manual, Section § 6.3 for details.
+Here is an example of use:
+
+\begin{lstlisting}
+//@ import \wp::why3: number::Gcd;
+
+/*@
+  assigns \nothing;
+  ensures \result == Gcd::gcd(a,b);
+*/
+int euclid(int a, int b)
+{
+  int r;
+  /*@
+    loop assigns a, b, r;
+    loop invariant Gcd::gcd(a,b) == \at( Gcd::gcd(a,b), Pre );
+    loop variant \abs(b);
+  */
+  while( b != 0 ) {
+    r = b ;
+    b = a % b ;
+    a = r ;
+  }
+  return a < 0 ? -a : a;
+}
+\end{lstlisting}
+
+\noindent
+The Why3 load-path can be specified from the command-line:
+\begin{description}
+  \item[\tt -wp-library <dir,\ldots>] add the specified directory to the Why3 load-path.
+\end{description}
+
+\noindent
+Notice that the Why3 standard library is already in the load-path by default.
+
 \clearpage
 \subsection{Proof Session \& Cache}
 \label{wp-cache}
diff --git a/src/plugins/wp/tests/wp_gallery/euclid2.c b/src/plugins/wp/tests/wp_gallery/euclid2.c
new file mode 100644
index 0000000000000000000000000000000000000000..be53817f7d36463b5986ed6c78ae02deaf582822
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/euclid2.c
@@ -0,0 +1,26 @@
+#include <limits.h>
+
+//@ import why3: number::Gcd;
+
+/*@
+  requires \abs(a) <= INT_MAX ;
+  requires \abs(b) <= INT_MAX ;
+  assigns \nothing;
+  ensures \result == Gcd::gcd(a,b);
+*/
+
+int euclid_gcd(int a, int b)
+{
+  int r;
+  /*@
+    loop assigns a, b, r;
+    loop invariant Gcd::gcd(a,b) == \at( Gcd::gcd(a,b), Pre );
+    loop variant \abs(b);
+  */
+  while( b != 0 ) {
+    r = b ;
+    b = a % b ;
+    a = r ;
+  }
+  return a < 0 ? -a : a;
+}
diff --git a/src/plugins/wp/tests/wp_gallery/euclid3.c b/src/plugins/wp/tests/wp_gallery/euclid3.c
new file mode 100644
index 0000000000000000000000000000000000000000..8276d9682a602c7fa1538ca60cf842c3cceadfcf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/euclid3.c
@@ -0,0 +1,43 @@
+#include <limits.h>
+
+//@ import why3: number::Gcd;
+
+//@ import why3: int::MinMax;
+
+/*@
+  requires \abs(a) <= INT_MAX ;
+  requires \abs(b) <= INT_MAX ;
+  assigns \nothing;
+  ensures \result == Gcd::gcd(a,b);
+*/
+
+int euclid_gcd(int a, int b)
+{
+  int r;
+  /*@
+    loop assigns a, b, r;
+    loop invariant Gcd::gcd(a,b) == \at( Gcd::gcd(a,b), Pre );
+    loop variant \abs(b);
+  */
+  while( b != 0 ) {
+    r = b ;
+    b = a % b ;
+    a = r ;
+  }
+  return a < 0 ? -a : a;
+}
+
+/*@
+    requires \abs(a) <= INT_MAX;
+    requires \abs(b) <= INT_MAX;
+    requires \abs(c) <= INT_MAX;
+    requires \abs(d) <= INT_MAX;
+    assigns \nothing;
+    ensures \result == Gcd::gcd(MinMax::min(a,b), MinMax::max(c,d) );
+*/
+int minmax_gcd(int a, int b, int c, int d)
+{
+    int x = (a > b) ? b : a;
+    int y = (c > d) ? c : d;
+    return euclid_gcd(x,y);
+}
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/euclid2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/euclid2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..acf9ed3c7f25443c3a6d7688631702b55d7ab7ef
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle/euclid2.res.oracle
@@ -0,0 +1,101 @@
+# frama-c -wp [...]
+[kernel] Parsing euclid2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal euclid_gcd_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal euclid_gcd_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function euclid_gcd
+------------------------------------------------------------
+
+Goal Post-condition (file euclid2.c, line 9) in 'euclid_gcd':
+Let x = number.Gcd.gcd(a, b).
+Assume {
+  Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+      is_sint32(euclid_gcd_0).
+  (* Pre-condition *)
+  Have: IAbs.abs(a) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(b) <= 2147483647.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a_2, 0) = x.
+  If a_2 < 0
+  Then { Have: a_2 = a_1. Have: (a_1 + euclid_gcd_0) = 0. }
+  Else { Have: euclid_gcd_0 = a_2. }
+}
+Prove: x = euclid_gcd_0.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file euclid2.c, line 17):
+Let x = number.Gcd.gcd(a_2, b).
+Let x_1 = a_1 % a.
+Assume {
+  Type: is_sint32(a_2) /\ is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(b) /\
+      is_sint32(x_1).
+  (* Pre-condition *)
+  Have: IAbs.abs(a_2) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(b) <= 2147483647.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a_1, a) = x.
+  (* Then *)
+  Have: a != 0.
+}
+Prove: number.Gcd.gcd(a, x_1) = x.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file euclid2.c, line 17):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file euclid2.c, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'euclid_gcd' (1/3):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'euclid_gcd' (2/3):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'euclid_gcd' (3/3):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file euclid2.c, line 20):
+Let x = a % a_1.
+Let x_1 = number.Gcd.gcd(a_2, b).
+Assume {
+  Type: is_sint32(a_2) /\ is_sint32(a_1) /\ is_sint32(a) /\ is_sint32(b) /\
+      is_sint32(x).
+  (* Pre-condition *)
+  Have: IAbs.abs(a_2) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(b) <= 2147483647.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a, a_1) = x_1.
+  (* Then *)
+  Have: a_1 != 0.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a_1, x) = x_1.
+}
+Prove: IAbs.abs(x) < IAbs.abs(a_1).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file euclid2.c, line 20):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/euclid3.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/euclid3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ffbf3c57440a3cb44266406b858d27f4f17385e4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle/euclid3.res.oracle
@@ -0,0 +1,216 @@
+# frama-c -wp [...]
+[kernel] Parsing euclid3.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal euclid_gcd_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal euclid_gcd_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function euclid_gcd
+------------------------------------------------------------
+
+Goal Post-condition (file euclid3.c, line 11) in 'euclid_gcd':
+Let x = number.Gcd.gcd(a, b).
+Assume {
+  Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+      is_sint32(euclid_gcd_0).
+  (* Pre-condition *)
+  Have: IAbs.abs(a) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(b) <= 2147483647.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a_2, 0) = x.
+  If a_2 < 0
+  Then { Have: a_2 = a_1. Have: (a_1 + euclid_gcd_0) = 0. }
+  Else { Have: euclid_gcd_0 = a_2. }
+}
+Prove: x = euclid_gcd_0.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file euclid3.c, line 19):
+Let x = number.Gcd.gcd(a_2, b).
+Let x_1 = a_1 % a.
+Assume {
+  Type: is_sint32(a_2) /\ is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(b) /\
+      is_sint32(x_1).
+  (* Pre-condition *)
+  Have: IAbs.abs(a_2) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(b) <= 2147483647.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a_1, a) = x.
+  (* Then *)
+  Have: a != 0.
+}
+Prove: number.Gcd.gcd(a, x_1) = x.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file euclid3.c, line 19):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file euclid3.c, line 18):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'euclid_gcd' (1/3):
+Effect at line 22
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'euclid_gcd' (2/3):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'euclid_gcd' (3/3):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file euclid3.c, line 22):
+Let x = a % a_1.
+Let x_1 = number.Gcd.gcd(a_2, b).
+Assume {
+  Type: is_sint32(a_2) /\ is_sint32(a_1) /\ is_sint32(a) /\ is_sint32(b) /\
+      is_sint32(x).
+  (* Pre-condition *)
+  Have: IAbs.abs(a_2) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(b) <= 2147483647.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a, a_1) = x_1.
+  (* Then *)
+  Have: a_1 != 0.
+  (* Invariant *)
+  Have: number.Gcd.gcd(a_1, x) = x_1.
+}
+Prove: IAbs.abs(x) < IAbs.abs(a_1).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file euclid3.c, line 22):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function minmax_gcd
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'minmax_gcd':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file euclid3.c, line 36) in 'minmax_gcd':
+Let x = number.Gcd.gcd(tmp_0, tmp_0_0).
+Assume {
+  Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(d) /\
+      is_sint32(tmp_0) /\ is_sint32(tmp_0_0) /\ is_sint32(x).
+  (* Pre-condition *)
+  Have: IAbs.abs(a) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(b) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(c) <= 2147483647.
+  (* Pre-condition *)
+  Have: IAbs.abs(d) <= 2147483647.
+  If b < a
+  Then { Have: tmp_0 = b. }
+  Else { Have: tmp_0 = a. }
+  If d < c
+  Then { Have: tmp_0_0 = c. }
+  Else { Have: tmp_0_0 = d. }
+  (* Call 'euclid_gcd' *)
+  Have: (IAbs.abs(tmp_0) <= 2147483647) /\ (IAbs.abs(tmp_0_0) <= 2147483647).
+}
+Prove: number.Gcd.gcd(int.MinMax.min(a, b), int.MinMax.max(c, d)) = x.
+
+------------------------------------------------------------
+
+Goal Exit-condition (generated) in 'minmax_gcd':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (1/5):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (2/5):
+Effect at line 40
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (3/5):
+Effect at line 40
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (4/5):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (5/5):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (2/6):
+Effect at line 40
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (3/6):
+Effect at line 40
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (4/6):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (5/6):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'minmax_gcd' (6/6):
+Call Result at line 42
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file euclid3.c, line 8) in 'euclid_gcd'' in 'minmax_gcd' at call 'euclid_gcd' (file euclid3.c, line 42)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file euclid3.c, line 9) in 'euclid_gcd'' in 'minmax_gcd' at call 'euclid_gcd' (file euclid3.c, line 42)
+:
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bbeccc30fa0cbcf38acb9307f9fea2d07367d486
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid2.res.oracle
@@ -0,0 +1,25 @@
+# frama-c -wp [...]
+[kernel] Parsing euclid2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal euclid_gcd_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal euclid_gcd_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 9 goals scheduled
+[wp] [Valid] typed_euclid_gcd_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_gcd_loop_invariant_established (Qed)
+[wp] [Valid] typed_euclid_gcd_loop_assigns (Qed)
+[wp] [Valid] typed_euclid_gcd_assigns_part1 (Qed)
+[wp] [Valid] typed_euclid_gcd_assigns_part2 (Qed)
+[wp] [Valid] typed_euclid_gcd_assigns_part3 (Qed)
+[wp] [Valid] typed_euclid_gcd_loop_variant_decrease (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_gcd_loop_variant_positive (Qed)
+[wp] Proved goals:   11 / 11
+  Terminating:     1
+  Unreachable:     1
+  Qed:             6
+  Alt-Ergo:        3
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  euclid_gcd                6        3        9       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid3.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e908338719802a4c175ec5357fcf5ed86b88d618
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid3.res.oracle
@@ -0,0 +1,42 @@
+# frama-c -wp [...]
+[kernel] Parsing euclid3.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal euclid_gcd_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal euclid_gcd_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 25 goals scheduled
+[wp] [Valid] typed_euclid_gcd_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_gcd_loop_invariant_established (Qed)
+[wp] [Valid] typed_euclid_gcd_loop_assigns (Qed)
+[wp] [Valid] typed_euclid_gcd_assigns_part1 (Qed)
+[wp] [Valid] typed_euclid_gcd_assigns_part2 (Qed)
+[wp] [Valid] typed_euclid_gcd_assigns_part3 (Qed)
+[wp] [Valid] typed_euclid_gcd_loop_variant_decrease (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_gcd_loop_variant_positive (Qed)
+[wp] [Valid] typed_minmax_gcd_terminates (Qed)
+[wp] [Valid] typed_minmax_gcd_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] typed_minmax_gcd_exits (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_exit_part1 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_exit_part2 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_exit_part3 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_exit_part4 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_exit_part5 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_normal_part1 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_normal_part2 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_normal_part3 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_normal_part4 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_normal_part5 (Qed)
+[wp] [Valid] typed_minmax_gcd_assigns_normal_part6 (Qed)
+[wp] [Valid] typed_minmax_gcd_call_euclid_gcd_requires (Qed)
+[wp] [Valid] typed_minmax_gcd_call_euclid_gcd_requires_2 (Qed)
+[wp] Proved goals:   27 / 27
+  Terminating:     1
+  Unreachable:     1
+  Qed:            21
+  Alt-Ergo:        4
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  euclid_gcd                6        3        9       100%
+  minmax_gcd               15        1       16       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/import_inductive.i b/src/plugins/wp/tests/wp_plugin/import_inductive.i
new file mode 100644
index 0000000000000000000000000000000000000000..ec676ef0c289298d148b4c81879b27d44b47ed69
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_inductive.i
@@ -0,0 +1,8 @@
+//@ import why3: list::Distinct ;
+
+// WP cannot deal with a fully polymorphic value for now
+// @ lemma L1 <A> : Distinct::distinct([| |]) ;
+
+
+//@ lemma L2: Distinct::distinct([| 0 |]) ;
+//@ lemma L3: Distinct::distinct([| 1 , 2 |]) ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_int.i b/src/plugins/wp/tests/wp_plugin/import_int.i
new file mode 100644
index 0000000000000000000000000000000000000000..7a661141451a55dd506d1d54c8197411c5664593
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_int.i
@@ -0,0 +1,3 @@
+//@ import why3: int::Int \as I ;
+
+//@ lemma iso: I::zero == 0 ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_option.i b/src/plugins/wp/tests/wp_plugin/import_option.i
new file mode 100644
index 0000000000000000000000000000000000000000..ca692214f4d1e8ba201d31ae41f9aefbeb7bb8a6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_option.i
@@ -0,0 +1,27 @@
+//@ import why3: option::Option \as O ;
+
+//@ logic O::option<integer> to_opt_t(integer p) = O::Some(p);
+//@ lemma bar_1: \forall integer p ; to_opt_t(p) == O::Some(p);
+//@ lemma bar_2: \forall integer p ; to_opt_t(p) != O::None;
+
+/*@ logic O::option<integer> to_opt(int* p) =
+      p == \null ? O::None : O::Some(*p);
+*/
+
+int g ;
+
+/*@ behavior zero:
+      assumes i == 0 ;
+      ensures to_opt(\result) == O::None ;
+
+    behavior other:
+      assumes i != 0 ;
+      ensures to_opt(\result) == O::Some(42) ;
+*/
+int* f(int i){
+  if(i == 0) return (void*)0;
+  else {
+    g = 42 ;
+    return &g ;
+  }
+}
diff --git a/src/plugins/wp/tests/wp_plugin/import_real_infix.i b/src/plugins/wp/tests/wp_plugin/import_real_infix.i
new file mode 100644
index 0000000000000000000000000000000000000000..ec1dad5feb86bd9e0616142bd8c969beae5e1a3e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_real_infix.i
@@ -0,0 +1,3 @@
+//@ import why3: real::RealInfix \as RI ;
+
+//@ lemma infix: RI::(<.)((RI::(+.)(0., 1.)), 2.) ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_unexisting.i b/src/plugins/wp/tests/wp_plugin/import_unexisting.i
new file mode 100644
index 0000000000000000000000000000000000000000..cd6a13893cd7b642877ce10395a2afa91f28c9ec
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_unexisting.i
@@ -0,0 +1,9 @@
+/* run.config
+   EXIT: 1
+   OPT:
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+//@ import why3: unexisting::Module ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_unitex.i b/src/plugins/wp/tests/wp_plugin/import_unitex.i
new file mode 100644
index 0000000000000000000000000000000000000000..12ea1f3c54cfbe22bbbf17ecd388f7ce06346387
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_unitex.i
@@ -0,0 +1,68 @@
+/* run.config*
+   DEPS: @PTEST_NAME@.mlw
+   OPT: -wp-library "."
+*/
+
+// Builtin types + synonyms
+
+//@ import why3: int::Int \as I ;
+//@ import why3: real::Real \as R ;
+//@ import why3: bool::Bool \as B ;
+
+//@ import why3: import_unitex::Builtin \as BI ;
+
+/*@ predicate compat_int(integer a, BI::bint b) = a == b ;
+    lemma L_compat_int_1: compat_int(I::zero, 0) ;
+    lemma L_compat_int_2: compat_int(0, I::zero) ;
+*/
+/*@ predicate compat_real(real a, BI::breal b) = a == b ;
+    lemma L_compat_real_1: compat_real(R::zero, 0) ;
+    lemma L_compat_real_2: compat_real(0, R::zero) ;
+*/
+/*@ predicate compat_bool(boolean a, BI::bbool b) = B::andb(a, b) == \true ;
+    lemma L_compat_bool: compat_bool(\true, \true) ;
+*/
+
+// Type without definition
+
+//@ import why3: import_unitex::No_def ;
+//@ import why3: import_unitex::No_def_syn ;
+//@ lemma L_no_def: No_def::x == No_def_syn::y ;
+
+// ADT
+
+//@ import why3: import_unitex::ADT ;
+
+/*@ predicate compat_adt(ADT::t<real> a, ADT::s<real> b) = a == b ;
+    lemma L_compat_adt_1: compat_adt(ADT::A, ADT::A) ;
+    lemma L_compat_adt_2: compat_adt(ADT::B(1), ADT::B(1)) ;
+    lemma L_compat_adt_3: compat_adt(ADT::C(0.), ADT::C(0.)) ;
+*/
+
+// Range
+
+//@ import why3: import_unitex::Range \as Rg ;
+
+/*@ lemma L_rg_1:
+      \forall integer i ;
+        -42 <= i <= 42 ==> Rg::to_int (Rg::of_int (i)) == i ;
+*/
+
+//@ lemma L_rg_2: \forall Rg::r42 i ; -42 <= Rg::to_int (i) <= 42 ;
+
+// Float
+
+//@ import why3: import_unitex::Float8 \as F8 ;
+
+//@ lemma L_f8: F8::is_finite(F8::f1) ;
+
+// Symbols
+
+//@ import why3: import_unitex::Symbols \as S1 ;
+//@ import why3: import_unitex::Symbols \as S2 ;
+//@ import why3: import_unitex::Symbols ;
+//@ import why3: import_unitex::Symbols ; // should not fail
+
+//@ lemma L_sym_1: S1::(==)(S1::(!)(0), 42) ;
+//@ lemma L_sym_2: S2::pred(S2::func(0), 42) ;
+//@ lemma L_sym_3: Symbols::pos(4);
diff --git a/src/plugins/wp/tests/wp_plugin/import_unitex.mlw b/src/plugins/wp/tests/wp_plugin/import_unitex.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..8fbfd479d1abcac997969eec3a45287552dc8038
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_unitex.mlw
@@ -0,0 +1,64 @@
+module Builtin
+  use int.Int
+  use real.Real
+  use bool.Bool
+
+  type bint = int
+  type breal = real
+  type bbool = bool
+end
+
+module No_def
+  type t
+  constant x: t
+end
+
+module No_def_syn
+  use No_def
+
+  type t = No_def.t
+  constant y: t = x
+end
+
+module ADT
+  use int.Int
+  type t 'a = A | B int | C 'a
+  type s 'a = t 'a
+end
+
+module Range
+  use int.Int
+
+  type r42 = < range -42 42 >
+  function to_int (x: r42) : int = r42'int x
+
+  function of_int (x: int) : r42
+  axiom ax:
+    forall x: int.
+      -42 <= x <= 42 -> to_int(of_int(x)) = x
+end
+
+module Float8
+  use real.Real
+
+  type f8 = < float 4 3 >
+
+  constant f1: f8 = (0.5:f8)
+  predicate is_finite(f: f8) = f8'isFinite(f)
+end
+
+module Symbols
+  use int.Int
+
+  predicate pred(i j: int) = i = j
+  predicate (==) (i j: int) = pred i j
+
+  function func(i: int) : int = i + 42
+  function (!) (i : int) : int = func i
+
+  lemma x: !0 == 42
+
+  inductive pos(i: int) =
+    | Base : pos(1)
+    | Plus : forall i : int. pos (i-1) -> pos i
+end
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_inductive.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4e83e5029fb407b219a119ce23506b32e221de62
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_inductive.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp [...]
+[kernel] Parsing import_inductive.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Lemma 'L2':
+Prove: list.Distinct.distinct([ 0 ]).
+
+------------------------------------------------------------
+
+Goal Lemma 'L3':
+Assume Lemmas: 'L2'
+Prove: list.Distinct.distinct([ 1, 2 ]).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_int.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_int.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1b815532ea68a52163850c376188c4b14cf015da
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_int.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_int.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Lemma 'iso':
+Prove: int.Int.zero = 0.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_option.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_option.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d9f152360824458a7541d7d1632398a287aab358
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_option.res.oracle
@@ -0,0 +1,38 @@
+# frama-c -wp [...]
+[kernel] Parsing import_option.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Lemma 'bar_1':
+Prove: L_to_opt_t(p) = option.Option.Some(p).
+
+------------------------------------------------------------
+
+Goal Lemma 'bar_2':
+Assume Lemmas: 'bar_1'
+Prove: L_to_opt_t(p) != option.Option.None.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f with behavior other
+------------------------------------------------------------
+
+Goal Post-condition for 'other' (file import_option.i, line 19) in 'f':
+Let a = global(G_g_31).
+Assume { Type: is_sint32(i). (* Pre-condition for 'other' *) Have: i != 0. }
+Prove: L_to_opt(Mint_0[a <- 42], a) = option.Option.Some(42).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f with behavior zero
+------------------------------------------------------------
+
+Goal Post-condition for 'zero' (file import_option.i, line 15) in 'f':
+Prove: L_to_opt(Mint_0, null) = option.Option.None.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_real_infix.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_real_infix.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5b0227df806bb7bb0f9697b5bd62a09f237a0ab2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_real_infix.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_real_infix.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Lemma 'infix':
+Prove: real.RealInfix.infix <.(real.RealInfix.infix +.(.0, 1.0), 2.0).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d5852e56a1789c285c609b16d212a2cf833ced2d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
@@ -0,0 +1,7 @@
+# frama-c -wp [...]
+[kernel] Parsing import_unexisting.i (no preprocessing)
+[wp] User Error: Library Module not found
+[wp] Running WP plugin...
+[wp] No proof obligations
+[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_unitex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_unitex.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7a372ba57973701955ff13bce993b7a15c0d3900
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_unitex.res.oracle
@@ -0,0 +1,113 @@
+# frama-c -wp [...]
+[kernel] Parsing import_unitex.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_adt_1':
+Assume Lemmas: 'L_no_def' 'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1'
+  'L_compat_int_2' 'L_compat_int_1'
+Prove: P_compat_adt(import_unitex.ADT.A, import_unitex.ADT.A).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_adt_2':
+Assume Lemmas: 'L_compat_adt_1' 'L_no_def' 'L_compat_bool' 'L_compat_real_2'
+  'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Let a = import_unitex.ADT.B(1). Prove: P_compat_adt(a, a).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_adt_3':
+Assume Lemmas: 'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def' 'L_compat_bool'
+  'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Let a = import_unitex.ADT.C(.0). Prove: P_compat_adt(a, a).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_bool':
+Assume Lemmas: 'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2'
+  'L_compat_int_1'
+Prove: P_compat_bool(true, true).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_int_1':
+Prove: P_compat_int(int.Int.zero, 0).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_int_2':
+Assume Lemmas: 'L_compat_int_1'
+Prove: P_compat_int(0, int.Int.zero).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_real_1':
+Assume Lemmas: 'L_compat_int_2' 'L_compat_int_1'
+Prove: P_compat_real(real.Real.zero, .0).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_real_2':
+Assume Lemmas: 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: P_compat_real(.0, real.Real.zero).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_f8':
+Assume Lemmas: 'L_rg_2' 'L_rg_1' 'L_compat_adt_3' 'L_compat_adt_2'
+  'L_compat_adt_1' 'L_no_def' 'L_compat_bool' 'L_compat_real_2'
+  'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Float8.is_finite(import_unitex.Float8.f1).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_no_def':
+Assume Lemmas: 'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1'
+  'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.No_def_syn.y = import_unitex.No_def.x.
+
+------------------------------------------------------------
+
+Goal Lemma 'L_rg_1':
+Assume Lemmas: 'L_compat_adt_3' 'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def'
+  'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2'
+  'L_compat_int_1'
+Assume { Have: (-42) <= i. Have: i <= 42. }
+Prove: import_unitex.Range.to_int(import_unitex.Range.of_int(i)) = i.
+
+------------------------------------------------------------
+
+Goal Lemma 'L_rg_2':
+Assume Lemmas: 'L_rg_1' 'L_compat_adt_3' 'L_compat_adt_2' 'L_compat_adt_1'
+  'L_no_def' 'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1'
+  'L_compat_int_2' 'L_compat_int_1'
+Let x = import_unitex.Range.to_int(i). Prove: ((-42) <= x) /\ (x <= 42).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_sym_1':
+Assume Lemmas: 'L_f8' 'L_rg_2' 'L_rg_1' 'L_compat_adt_3' 'L_compat_adt_2'
+  'L_compat_adt_1' 'L_no_def' 'L_compat_bool' 'L_compat_real_2'
+  'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Symbols.infix ==(import_unitex.Symbols.prefix !(0), 42).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_sym_2':
+Assume Lemmas: 'L_sym_1' 'L_f8' 'L_rg_2' 'L_rg_1' 'L_compat_adt_3'
+  'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def' 'L_compat_bool'
+  'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Symbols.pred(import_unitex.Symbols.func(0), 42).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_sym_3':
+Assume Lemmas: 'L_sym_2' 'L_sym_1' 'L_f8' 'L_rg_2' 'L_rg_1' 'L_compat_adt_3'
+  'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def' 'L_compat_bool'
+  'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Symbols.pos(4).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_inductive.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0a4554a8131dbafd6e5d95ccab38a2915c268fd2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_inductive.res.oracle
@@ -0,0 +1,12 @@
+# frama-c -wp [...]
+[kernel] Parsing import_inductive.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 2 goals scheduled
+[wp] [Valid] typed_lemma_L2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L3 (Alt-Ergo) (Cached)
+[wp] Proved goals:    2 / 2
+  Alt-Ergo:        2
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        2        2       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_int.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_int.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..40e0ceaa69baa0d8e4229eeb2c89adb958454102
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_int.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_int.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Valid] typed_lemma_iso (Alt-Ergo) (Trivial)
+[wp] Proved goals:    1 / 1
+  Alt-Ergo:        1
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        1        1       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_option.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_option.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dbb2897a04f76d7789d7b8fa20e4b55e160b9bda
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_option.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp [...]
+[kernel] Parsing import_option.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Valid] typed_lemma_bar_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_bar_2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_f_zero_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] typed_f_other_ensures (Alt-Ergo) (Cached)
+[wp] Proved goals:    6 / 6
+  Terminating:     1
+  Unreachable:     1
+  Alt-Ergo:        4
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        2        2       100%
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  f                         -        2        2       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_real_infix.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_real_infix.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a4392218e7fdfca14a1fddeccfc29cd716c61307
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_real_infix.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_real_infix.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Valid] typed_lemma_infix (Alt-Ergo) (Cached)
+[wp] Proved goals:    1 / 1
+  Alt-Ergo:        1
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        1        1       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_unitex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_unitex.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..56543743d0095bdc20546f15dc56612ad0f7192a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_unitex.res.oracle
@@ -0,0 +1,25 @@
+# frama-c -wp [...]
+[kernel] Parsing import_unitex.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 15 goals scheduled
+[wp] [Valid] typed_lemma_L_compat_adt_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_adt_2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_adt_3 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_bool (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_compat_int_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_int_2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_real_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_real_2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_f8 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_no_def (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_rg_1 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_rg_2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_sym_1 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_sym_2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_sym_3 (Alt-Ergo) (Cached)
+[wp] Proved goals:   15 / 15
+  Alt-Ergo:       15
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -       15       15       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index efb064a639de06c19ba50ed0590885f962904aac..2c4c8f714efe74909d4f016b14f631da0369dfbb 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -751,17 +751,6 @@ module Tactics = String_list
 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
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 84a25a418c36a8b3ca43d84f4b195aeb76505873..1a0da8692295a6e2a8b524dd9928284ec09f13f6 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -116,7 +116,6 @@ 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