diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index ea121cb9b8cedcff35a8a6114e312eca1d205ab0..fdf07763cf86afae3cb2e498efc33435fa7a5829 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -199,11 +199,6 @@ module TYPE = STRUCTURAL
 
 let has_ctype = TYPE.is_typ
 
-let has_ltype ltype e =
-  match Logic_utils.unroll_type ~unroll_typedef:false ltype with
-  | Ctype typ -> has_ctype typ e
-  | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _ -> p_true
-
 let is_object obj = function
   | Loc _ -> p_true
   | Val e -> TYPE.is_obj obj e
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index 102255f1c0465fe84322dc84d93da68a522eb475..e5e4f0d60885a61dff351964cf718cbd967b0b9c 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -69,7 +69,6 @@ val startof : shift:('a -> c_object -> term -> 'a) -> 'a -> typ -> 'a
 
 val is_object : c_object -> 'a value -> pred
 val has_ctype : typ -> term -> pred
-val has_ltype : logic_type -> term -> pred
 
 val cdomain : c_object -> (term -> pred) option
 val ldomain : logic_type -> (term -> pred) option
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 27f13b6965a9a6129207f2f2d07d0533af2e2f95..5652757329553f29c2bbe8aa6125376a797411d4 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -61,6 +61,29 @@ struct
     | Sig_value of logic_var (* to be replaced by the value *)
     | Sig_chunk of chunk * c_label (* to be replaced by the chunk variable *)
 
+  (* -------------------------------------------------------------------------- *)
+  (* --- Registering User-Defined Signatures                                --- *)
+  (* -------------------------------------------------------------------------- *)
+
+  module Typedefs = WpContext.Index
+      (struct
+        type key = logic_type_info
+        type data = lfun option
+        let name = "LogicCompiler." ^ M.datatype ^ ".Typedefs"
+        let compare = Logic_type_info.compare
+        let pretty = Logic_type_info.pretty
+      end)
+  let compile_logic_type = ref (fun _ -> assert false)
+
+  module Signature = WpContext.Index
+      (struct
+        type key = logic_info
+        type data = signature
+        let name = "LogicCompiler." ^ M.datatype ^ ".Signature"
+        let compare = Logic_info.compare
+        let pretty fmt l = Logic_var.pretty fmt l.l_var_info
+      end)
+
   (* -------------------------------------------------------------------------- *)
   (* --- Utilities                                                          --- *)
   (* -------------------------------------------------------------------------- *)
@@ -79,10 +102,21 @@ struct
     | (label,mem) :: m -> LabelMap.add label mem (wrap_mem m)
     | [] -> LabelMap.empty
 
+  let has_ltype ltype t =
+    match Logic_utils.unroll_type ~unroll_typedef:false ltype with
+    | Ltype (lt, _) ->
+        if not (Typedefs.mem lt) then !compile_logic_type ltype ;
+        begin match Typedefs.find lt with
+          | Some lfun -> F.p_call lfun [t]
+          | None -> p_true
+        end
+    | Ctype typ -> Cvalues.has_ctype typ t
+    | _ -> p_true
+
   let fresh_lvar ?basename ltyp =
     let tau = Lang.tau_of_ltype ltyp in
     let x = Lang.freshvar ?basename tau in
-    let p = Cvalues.has_ltype ltyp (e_var x) in
+    let p = has_ltype ltyp (e_var x) in
     Lang.assume p ; x
 
   let fresh_cvar ?basename typ =
@@ -363,7 +397,7 @@ struct
     | [] -> { vars=vars ; lhere=None ; current=None } , domain , List.rev sigv
     | lv :: profile ->
         let x = param_of_lv lv in
-        let h = Cvalues.has_ltype lv.lv_type (e_var x) in
+        let h = has_ltype lv.lv_type (e_var x) in
         let v = Cvalues.plain lv.lv_type (e_var x) in
         profile_env
           (Logic_var.Map.add lv v vars)
@@ -448,28 +482,6 @@ struct
   let is_recursive l =
     if LogicUsage.is_recursive l then Rec else Def
 
-  (* -------------------------------------------------------------------------- *)
-  (* --- Registering User-Defined Signatures                                --- *)
-  (* -------------------------------------------------------------------------- *)
-
-  module Typedefs = WpContext.Index
-      (struct
-        type key = logic_type_info
-        type data = unit
-        let name = "LogicCompiler." ^ M.datatype ^ ".Typedefs"
-        let compare = Logic_type_info.compare
-        let pretty = Logic_type_info.pretty
-      end)
-
-  module Signature = WpContext.Index
-      (struct
-        type key = logic_info
-        type data = signature
-        let name = "LogicCompiler." ^ M.datatype ^ ".Signature"
-        let compare = Logic_info.compare
-        let pretty fmt l = Logic_var.pretty fmt l.l_var_info
-      end)
-
   (* -------------------------------------------------------------------------- *)
   (* --- Compiling Lemmas                                                   --- *)
   (* -------------------------------------------------------------------------- *)
@@ -509,7 +521,7 @@ struct
             let rec conditions vs sigp =
               match vs , sigp with
               | v::vs , Sig_value lv :: sigp ->
-                  let cond = Cvalues.has_ltype lv.lv_type v in
+                  let cond = has_ltype lv.lv_type v in
                   cond :: conditions vs sigp
               | _ -> [] in
             let result = F.e_fun ldef.d_lfun vs in
@@ -726,9 +738,51 @@ struct
   (* --- Retrieving Signature                                               --- *)
   (* -------------------------------------------------------------------------- *)
 
-  let define_type c t =
-    Typedefs.update t () ;
-    Definitions.define_type c t
+  let define_type cluster lt =
+    let constrainer = match lt with
+      | { lt_def = Some(LTsum(ctors)) ; lt_name ; lt_params=[] } ->
+          let frame = logic_frame lt_name [] in
+          in_frame frame
+            begin fun () ->
+              let lfun = Lang.generated_p ("is_" ^ lt_name) in
+              let tau_lt = Lang.tau_of_ltype (Ltype(lt, [])) in
+              Typedefs.update lt (Some lfun) ;
+              let term_constraint ltyp =
+                let v = Lang.freshvar ~basename:"p" (Lang.tau_of_ltype ltyp) in
+                v, (has_ltype ltyp (Lang.F.e_var v))
+              in
+              let ctor_to_prop = function
+                | { ctor_name = l_name ; ctor_params = ts } as const ->
+                    let vs, cs = List.split (List.map term_constraint ts) in
+                    let ts = List.map Lang.F.e_var vs in
+                    let const = F.e_fun ~result:tau_lt (CTOR const) ts in
+                    let is_lt = F.p_call lfun [const] in
+                    {
+                      l_name ;
+                      l_types = 0 ;
+                      l_assumed = true ;
+                      l_triggers = [frame.triggers] ;
+                      l_forall = vs ;
+                      l_cluster = cluster ;
+                      l_lemma = p_hyps cs is_lt ;
+                    }
+              in
+              let cases = List.map ctor_to_prop ctors in
+              Definitions.define_symbol {
+                d_lfun = lfun ;
+                d_types = 0 ;
+                d_params = [ Lang.freshvar ~basename:"v" tau_lt ] ;
+                d_cluster = cluster ;
+                d_definition = Inductive cases
+              } ;
+              Some lfun
+            end ()
+      | { lt_def = Some(LTsum(_)) ; lt_params=_ } ->
+          Wp_parameters.not_yet_implemented "Type parameters for sum types"
+      | _ -> None
+    in
+    Typedefs.update lt constrainer ;
+    Definitions.define_type cluster lt
 
   let define_logic c a = Signature.compile (compile_logic c a)
 
@@ -785,7 +839,7 @@ struct
         List.iter logic_type ps ;
         if not (Typedefs.mem lt) then
           begin
-            Typedefs.update lt () ;
+            Typedefs.update lt None ;
             if not (Lang.is_builtin lt) &&
                not (Logic_const.is_boolean_type t)
             then
@@ -798,6 +852,7 @@ struct
                   (* force compilation of entire axiomatics *)
                   define_axiomatic cluster ax
           end
+  let () = compile_logic_type := logic_type
 
   let logic_profile phi =
     begin
diff --git a/src/plugins/wp/LogicCompiler.mli b/src/plugins/wp/LogicCompiler.mli
index 6f818870f67f5de55d733cf86722e415d099db5a..aaf8cd8f3245afa82500073abd9224e65b8d07d7 100644
--- a/src/plugins/wp/LogicCompiler.mli
+++ b/src/plugins/wp/LogicCompiler.mli
@@ -126,6 +126,8 @@ sig
   val logic_var : env -> logic_var -> logic
   val logic_info : env -> logic_info -> pred option
 
+  val has_ltype : logic_type -> term -> pred
+
   (** {3 Logic Lemmas} *)
 
   val lemma : logic_lemma -> dlemma
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 1a84dcf2d3c491674e8b9d914c48f277182d5de3..1b0f23d8c3fbda099ca9c02f06e1e8943cf1f9cb 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -623,7 +623,7 @@ struct
           let h =
             if Wp_parameters.SimplifyForall.get ()
             then F.p_true
-            else Cvalues.has_ltype v.lv_type (e_var x)
+            else C.has_ltype v.lv_type (e_var x)
           in
           let e = C.env_let env v (Vexp (e_var x)) in
           acc (x::xs) e (h::hs) vs in
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index d0d05905e1eccea824ddad15a7e1efc1bad52977..f225a3cb684399e3b2bbab5eee7cc9b7534047bd 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -68,6 +68,8 @@ type convert = {
   pool: Lang.F.pool;
   polarity: Cvalues.polarity;
   in_goal: bool;
+  incomplete_types: (string, Why3.Ty.tysymbol) Hashtbl.t;
+  incomplete_symbols: (string, Why3.Term.lsymbol) Hashtbl.t;
   mutable convert_for_export: Lang.F.term Lang.F.Tmap.t;
 }
 
@@ -163,6 +165,8 @@ let empty_cnv ?(polarity=`NoPolarity) ?(in_goal=false) (ctx:context) : convert =
   env = ctx.env;
   polarity;
   in_goal;
+  incomplete_symbols = Hashtbl.create 3;
+  incomplete_types = Hashtbl.create 3;
   convert_for_export = Lang.F.Tmap.empty;
 }
 
@@ -252,7 +256,12 @@ let rec of_tau ~cnv (t:Lang.F.tau) =
       Some (Why3.Ty.ty_app ts [Why3.Opt.get (of_tau ~cnv k); Why3.Opt.get (of_tau ~cnv v)])
   | Data(adt,l) -> begin
       let s = name_of_adt adt in
-      match Why3.Theory.(ns_find_ts (get_namespace cnv.th) (cut_path s)) with
+      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 -> Why3.Opt.get (of_tau ~cnv e)) l))
       | exception Not_found ->
           why3_failure "Can't find type '%s' in why3 namespace" s
@@ -457,7 +466,12 @@ let rec of_term ~cnv expected t : Why3.Term.term =
           Why3.Term.t_app ls l r
         in
         let apply_from_ns s l sort =
-          match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)), expected with
+          let find s =
+            try Hashtbl.find cnv.incomplete_symbols s
+            with Not_found ->
+              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)
@@ -670,7 +684,7 @@ class visitor (ctx:context) c =
           v#add_builtin_lib;
           v#vself;
           let th = Why3.Theory.close_theory ctx.th in
-          if Wp_parameters.has_dkey ProverErgo.dkey_cluster then
+          if Wp_parameters.has_print_generated () then
             Log.print_on_output
               begin fun fmt ->
                 Format.fprintf fmt "---------------------------------------------@\n" ;
@@ -784,13 +798,15 @@ class visitor (ctx:context) c =
           let decl = Why3.Decl.create_ty_decl id in
           ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
       | Tsum cases ->
-          let id = Why3.Ident.id_fresh (Lang.type_id lt) in
+          let name = Lang.type_id lt in
+          let id = Why3.Ident.id_fresh name in
           let map i _ = tvar i in
           let tv_args = List.mapi map lt.lt_params in
           let tys = Why3.Ty.create_tysymbol id tv_args NoDef in
+          let cnv = empty_cnv ctx in
+          Hashtbl.add cnv.incomplete_types name tys ;
           let tv_args = List.map Why3.Ty.ty_var tv_args in
           let return_ty = Why3.Ty.ty_app tys tv_args in
-          let cnv = empty_cnv ctx in
           let constr = List.length cases in
           let cases = List.map (fun (c,targs) ->
               let name = match c with | Lang.CTOR c -> Lang.ctor_id c | _ -> assert false in
@@ -803,13 +819,15 @@ class visitor (ctx:context) c =
           let decl = Why3.Decl.create_data_decl [tys,cases] in
           ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
       | Trec fields ->
-          let id = Why3.Ident.id_fresh (Lang.type_id lt) in
+          let name = Lang.type_id lt in
+          let id = Why3.Ident.id_fresh name in
           let map i _ = tvar i in
           let tv_args = List.mapi map lt.lt_params in
           let tys = Why3.Ty.create_tysymbol id tv_args NoDef in
+          let cnv = empty_cnv ctx in
+          Hashtbl.add cnv.incomplete_types name tys ;
           let tv_args = List.map Why3.Ty.ty_var tv_args in
           let return_ty = Why3.Ty.ty_app tys tv_args in
-          let cnv = empty_cnv ctx in
           let fields,args = List.split @@ List.map (fun (f,ty) ->
               let name = Lang.name_of_field f in
               let id = Why3.Ident.id_fresh name in
@@ -847,21 +865,23 @@ class visitor (ctx:context) c =
         ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
       end
 
+    method private make_lemma cnv (l: Definitions.dlemma) =
+      let id = Why3.Ident.id_fresh (Lang.lemma_id l.l_name) in
+      let id = Why3.Decl.create_prsymbol id in
+      List.iter (Lang.F.add_var cnv.pool) l.l_forall;
+      let cnv, vars = Lang.For_export.in_state (mk_binders cnv) l.l_forall in
+      let t = convert cnv Prop (Lang.F.e_prop l.l_lemma) in
+      let triggers = full_triggers l.l_triggers in
+      let triggers = Lang.For_export.in_state (List.map (List.map (of_trigger ~cnv))) triggers in
+      let t = Why3.Term.t_forall_close vars triggers t in
+      id, t
+
     method on_dlemma l =
-      begin
-        let kind = Why3.Decl.(if l.l_assumed then Paxiom else Plemma) in
-        let id = Why3.Ident.id_fresh (Lang.lemma_id l.l_name) in
-        let id = Why3.Decl.create_prsymbol id in
-        let cnv = empty_cnv ctx in
-        List.iter (Lang.F.add_var cnv.pool) l.l_forall;
-        let cnv, vars = Lang.For_export.in_state (mk_binders cnv) l.l_forall in
-        let t = convert cnv Prop (Lang.F.e_prop l.l_lemma) in
-        let triggers = full_triggers l.l_triggers in
-        let triggers = Lang.For_export.in_state (List.map (List.map (of_trigger ~cnv))) triggers in
-        let t = Why3.Term.t_forall_close vars triggers t in
-        let decl = Why3.Decl.create_prop_decl kind id t in
-        ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
-      end
+      let kind = Why3.Decl.(if l.l_assumed then Paxiom else Plemma) in
+      let cnv = empty_cnv ctx in
+      let id, t = self#make_lemma cnv l in
+      let decl = Why3.Decl.create_prop_decl kind id t in
+      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 ;
@@ -952,14 +972,18 @@ class visitor (ctx:context) c =
           end
         | Inductive dl ->
             (* create predicate symbol *)
-            let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_name d.d_lfun)) in
+            let fname = Qed.Export.link_name (lfun_name d.d_lfun) in
+            let id = Why3.Ident.id_fresh fname in
             let map e = Why3.Opt.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
-            let decl = Why3.Decl.create_param_decl id in
-            ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl ;
-            (* register axioms *)
-            List.iter (self#on_dlemma) dl
+            let fid = Why3.Term.create_lsymbol id ty_args None in
+            let make_case (l:Definitions.dlemma) =
+              let cnv = empty_cnv ctx in
+              Hashtbl.add cnv.incomplete_symbols fname fid ;
+              self#make_lemma cnv l
+            in
+            let ind_decl = (fid, List.map make_case dl) in
+            ctx.th <- Why3.Theory.add_ind_decl ctx.th Why3.Decl.Ind [ind_decl]
       end
 
   end
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index d0bde7870b7a8cade014142226f5f026c223bd3b..ea52c7dcb27540192bf438772975bf952af017e5 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -4,6 +4,28 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
+---------------------------------------------
+--- Context 'typed_f' Cluster 'Compound' 
+---------------------------------------------
+theory Compound
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  (* use frama_c_wp.memory.Memory *)
+  
+  function shift_sint32 (p:addr) (k:int) : addr = shift p k
+end
 [wp:print-generated] 
   theory WP
     (* use why3.BuiltIn.BuiltIn *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index d8cb3e9a8d05e830be50775f2197d99d3aaa12af..a1016679f96bf1124f0d163eec275e1e005514b5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -3,6 +3,30 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] 3 goals scheduled
+---------------------------------------------
+--- Context 'typed' Cluster 'Compound' 
+---------------------------------------------
+theory Compound
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  (* use frama_c_wp.memory.Memory *)
+  
+  function shift_sint32 (p:addr) (k:int) : addr = shift p k
+  
+  function shiftfield_F1__list_next (p:addr) : addr = shift p 1
+end
 [wp:print-generated] 
   theory WP
     (* use why3.BuiltIn.BuiltIn *)
@@ -19,12 +43,10 @@
     
     (* use map.Map *)
     
-    predicate P_is_gcd int int int
-    
-    axiom Q_gcd_zero : forall n:int. P_is_gcd n 0 n
-    
-    axiom Q_gcd_succ :
-      forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
+    inductive P_is_gcd int int int =
+      | Q_gcd_zero : forall n:int. P_is_gcd n 0 n
+      | Q_gcd_succ :
+          forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
     
     lemma Q_test_no_label :
       forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
@@ -33,17 +55,15 @@
     
     (* use Compound *)
     
-    predicate P_reachable (int -> int) (addr -> addr) addr addr
-    
-    axiom Q_root_reachable :
-      forall malloc:int -> int, mptr:addr -> addr, root:addr.
-       P_reachable malloc mptr root root
-    
-    axiom Q_next_reachable :
-      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
-       valid_rw malloc root 2 ->
-       P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
-       P_reachable malloc mptr root node
+    inductive P_reachable (int -> int) (addr -> addr) addr addr =
+      | Q_root_reachable :
+          forall malloc:int -> int, mptr:addr -> addr, root:addr.
+           P_reachable malloc mptr root root
+      | Q_next_reachable :
+          forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+           valid_rw malloc root 2 ->
+           P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root))
+           node -> P_reachable malloc mptr root node
     
     goal wp_goal :
       forall t:int -> int, t1:addr -> addr, t2:int -> int, t3:addr -> addr, a:
@@ -65,12 +85,11 @@
     
     (* use map.Map *)
     
-    predicate P_is_gcd1 int int int
-    
-    axiom Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
-    
-    axiom Q_gcd_succ1 :
-      forall a:int, b:int, d:int. P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
+    inductive P_is_gcd1 int int int =
+      | Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
+      | Q_gcd_succ1 :
+          forall a:int, b:int, d:int.
+           P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
     
     goal wp_goal :
       forall i:int, i1:int, i2:int. P_is_gcd1 i i1 i2 -> not P_is_gcd1 i1 i2 i
@@ -95,29 +114,26 @@
     
     (* use Compound *)
     
-    predicate P_reachable1 (int -> int) (addr -> addr) addr addr
-    
-    axiom Q_root_reachable1 :
-      forall malloc:int -> int, mptr:addr -> addr, root:addr.
-       P_reachable1 malloc mptr root root
-    
-    axiom Q_next_reachable1 :
-      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
-       valid_rw malloc root 2 ->
-       P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
-       P_reachable1 malloc mptr root node
+    inductive P_reachable1 (int -> int) (addr -> addr) addr addr =
+      | Q_root_reachable1 :
+          forall malloc:int -> int, mptr:addr -> addr, root:addr.
+           P_reachable1 malloc mptr root root
+      | Q_next_reachable1 :
+          forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+           valid_rw malloc root 2 ->
+           P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root))
+           node -> P_reachable1 malloc mptr root node
     
     lemma Q_test_one_label :
       forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
        addr -> addr, l1:addr, l2:addr.
        P_reachable1 malloc1 mptr1 l1 l2 -> not P_reachable1 malloc mptr l1 l2
     
-    predicate P_is_gcd2 int int int
-    
-    axiom Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
-    
-    axiom Q_gcd_succ2 :
-      forall a:int, b:int, d:int. P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
+    inductive P_is_gcd2 int int int =
+      | Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
+      | Q_gcd_succ2 :
+          forall a:int, b:int, d:int.
+           P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
     
     lemma Q_test_no_label1 :
       forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
@@ -142,26 +158,23 @@
         i1 < end1 ->
         get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
     
-    predicate P_same_elements (addr -> int) (addr -> int) addr addr int int
-    
-    axiom Q_refl :
-      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int,
-       end1:int.
-       P_same_array mint mint1 a b begin end1 ->
-       P_same_elements mint mint1 a b begin end1
-    
-    axiom Q_swap :
-      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int, i:
-       int, j:int, end1:int.
-       P_swap mint mint1 a b begin i j end1 ->
-       P_same_elements mint mint1 a b begin end1
-    
-    axiom Q_trans :
-      forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:addr, b:
-       addr, c:addr, begin:int, end1:int.
-       P_same_elements mint mint1 b c begin end1 ->
-       P_same_elements mint1 mint2 a b begin end1 ->
-       P_same_elements mint mint2 a c begin end1
+    inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
+      | Q_refl :
+          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+           int, end1:int.
+           P_same_array mint mint1 a b begin end1 ->
+           P_same_elements mint mint1 a b begin end1
+      | Q_swap :
+          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+           int, i:int, j:int, end1:int.
+           P_swap mint mint1 a b begin i j end1 ->
+           P_same_elements mint mint1 a b begin end1
+      | Q_trans :
+          forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
+           addr, b:addr, c:addr, begin:int, end1:int.
+           P_same_elements mint mint1 b c begin end1 ->
+           P_same_elements mint1 mint2 a b begin end1 ->
+           P_same_elements mint mint2 a c begin end1
     
     goal wp_goal :
       forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..41bb0db407147d61133f3a2d16373ed8ce45e1a8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
@@ -0,0 +1,235 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/sum_types.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 3 goals scheduled
+---------------------------------------------
+--- Context 'typed' Cluster 'A_A' 
+---------------------------------------------
+theory A_A
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  type A_InAxiomatic =
+    | C_IAu int
+    | C_IAc int
+    | C_IAi int
+  
+  (* use frama_c_wp.cint.Cint *)
+  
+  inductive is_InAxiomatic A_InAxiomatic =
+    | Q_IAu : forall p:int. is_uint32 p -> is_InAxiomatic (C_IAu p)
+    | Q_IAc : forall p:int. is_sint8 p -> is_InAxiomatic (C_IAc p)
+    | Q_IAi : forall p:int. is_InAxiomatic (C_IAi p)
+  
+  predicate P_P A_InAxiomatic
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'Axiomatic1' 
+---------------------------------------------
+theory Axiomatic1
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  type A_AtTopLevel =
+    | C_TLu int
+    | C_TLc int
+    | C_TLi int
+  
+  (* use frama_c_wp.cint.Cint *)
+  
+  inductive is_AtTopLevel A_AtTopLevel =
+    | Q_TLu : forall p:int. is_uint32 p -> is_AtTopLevel (C_TLu p)
+    | Q_TLc : forall p:int. is_sint8 p -> is_AtTopLevel (C_TLc p)
+    | Q_TLi : forall p:int. is_AtTopLevel (C_TLi p)
+  
+  (* use A_A *)
+  
+  lemma Q_LA : forall a:A_InAxiomatic. is_InAxiomatic a -> P_P a
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'A_X' 
+---------------------------------------------
+theory A_X
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  (* use Axiomatic1 *)
+  
+  predicate P_Q A_AtTopLevel
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'Axiomatic2' 
+---------------------------------------------
+theory Axiomatic2
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  type A_Rec =
+    | C_Nil
+    | C_C int A_Rec
+  
+  (* use frama_c_wp.cint.Cint *)
+  
+  inductive is_Rec A_Rec =
+    | Q_Nil : is_Rec C_Nil
+    | Q_C :
+        forall p:int, p1:A_Rec. is_Rec p1 -> is_sint32 p -> is_Rec (C_C p p1)
+  
+  (* use Axiomatic1 *)
+  
+  (* use A_X *)
+  
+  lemma Q_LB : forall a:A_AtTopLevel. is_AtTopLevel a -> P_Q a
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'A_Y' 
+---------------------------------------------
+theory A_Y
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  (* use Axiomatic2 *)
+  
+  predicate P_R A_Rec
+end
+[wp:print-generated] 
+  theory WP
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use Axiomatic2 *)
+    
+    (* use A_Y *)
+    
+    goal wp_goal : forall r:A_Rec. is_Rec r -> P_R r
+  end
+[wp:print-generated] 
+  theory WP1
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use Axiomatic1 *)
+    
+    (* use A_X *)
+    
+    goal wp_goal : forall a:A_AtTopLevel. is_AtTopLevel a -> P_Q a
+  end
+[wp:print-generated] 
+  theory WP2
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use A_A *)
+    
+    goal wp_goal : forall i:A_InAxiomatic. is_InAxiomatic i -> P_P i
+  end
+[wp] 3 goals generated
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma LA:
+Prove: (is_InAxiomatic a_0) -> (P_P a_0)
+
+------------------------------------------------------------
+
+Lemma LB:
+Assume: 'LA'
+Prove: (is_AtTopLevel a_0) -> (P_Q a_0)
+
+------------------------------------------------------------
+
+Lemma LC:
+Assume: 'LB' 'LA'
+Prove: (is_Rec a_0) -> (P_R a_0)
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/sum_types.i b/src/plugins/wp/tests/wp_acsl/sum_types.i
new file mode 100644
index 0000000000000000000000000000000000000000..bd95a51825eb451514d665dea6dbabd4ed9b8407
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/sum_types.i
@@ -0,0 +1,35 @@
+/* run.config
+   OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+/*@
+  axiomatic A {
+    type InAxiomatic = IAu(unsigned)
+                     | IAc(char)
+                     | IAi(integer) ;
+
+    predicate P(InAxiomatic a) reads \nothing ;
+  }
+  lemma LA: \forall InAxiomatic a ; P(a) ;
+*/
+/*@
+  type AtTopLevel = TLu(unsigned)
+                  | TLc(char)
+                  | TLi(integer) ;
+
+  axiomatic X {
+    predicate Q(AtTopLevel a) reads \nothing ;
+  }
+  lemma LB: \forall AtTopLevel a ; Q(a) ;
+*/
+/*@
+  type Rec = Nil | C(int, Rec) ;
+
+  axiomatic Y {
+    predicate R(Rec a) reads \nothing ;
+  }
+  lemma LC: \forall Rec a ; R(a) ;
+*/
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 0f90c5deb366647d57c2b869aaeac6de026b9c5d..4b57d2f03e09e31030018d51fd55a39abec3216b 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -4,7 +4,7 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-msg-key cluster -wp-model Typed -wp-check -then -wp -wp-model Typed+ref -wp-check
+   OPT: -wp-msg-key print-generated -wp-model Typed -wp-check -then -wp -wp-model Typed+ref -wp-check
 */
 
 //@ predicate P(integer a);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index 2c3c0c68a6b2d2f44462e42d1922b22197ac2052..99814117676139196e030fd7b41ecfbbc7790509 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
@@ -48,6 +48,35 @@ theory Axiomatic
   
   predicate P_P int
 end
+[wp:print-generated] 
+  theory WP
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use frama_c_wp.cint.Cint *)
+    
+    (* use Compound *)
+    
+    (* use Axiomatic *)
+    
+    goal wp_goal :
+      forall t:addr -> int, i:int, a:addr.
+       let x = get t (shift_sint32 a i) in
+       region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+  end
 [wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures : Typechecked
 [wp] Proved goals:    0 / 1
   Alt-Ergo 2.0.0:    0  (unsuccess: 1)
@@ -57,6 +86,35 @@ end
 ------------------------------------------------------------
 [wp] Running WP plugin...
 [wp] 2 goals scheduled
+[wp:print-generated] 
+  theory WP1
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use frama_c_wp.cint.Cint *)
+    
+    (* use Compound *)
+    
+    (* use Axiomatic *)
+    
+    goal wp_goal :
+      forall t:addr -> int, i:int, a:addr.
+       let x = get t (shift_sint32 a i) in
+       region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+  end
 [wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures : Typechecked
 ---------------------------------------------
 --- Context 'typed_ref_f' Cluster 'Compound' 
@@ -100,6 +158,35 @@ theory Axiomatic1
   
   predicate P_P1 int
 end
+[wp:print-generated] 
+  theory WP2
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool1 *)
+    
+    (* use int.Int1 *)
+    
+    (* use int.ComputerDivision1 *)
+    
+    (* use real.RealInfix1 *)
+    
+    (* use frama_c_wp.qed.Qed1 *)
+    
+    (* use map.Map1 *)
+    
+    (* use frama_c_wp.memory.Memory1 *)
+    
+    (* use frama_c_wp.cint.Cint1 *)
+    
+    (* use Compound1 *)
+    
+    (* use Axiomatic1 *)
+    
+    goal wp_goal :
+      forall t:addr1 -> int, i:int, a:addr1.
+       let x = get1 t (shift_sint321 a i) in
+       region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
+  end
 [wp] [Alt-Ergo 2.0.0] Goal typed_ref_f_ensures : Typechecked
 [wp] Proved goals:    0 / 2
   Alt-Ergo 2.0.0:    0  (unsuccess: 2)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
index fb6e3336de647eebe03fb9c24e275611ec4c23d9..82901ded836c14ba3f2ba30ec3e14fc6463f440b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
@@ -4,6 +4,27 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
+---------------------------------------------
+--- Context 'typed_f' Cluster 'S1_s' 
+---------------------------------------------
+theory S1_s
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  type S1_s =
+    | S1_s1 (F1_s_a:int -> int) (F1_s_b:int -> int)
+end
 [wp:print-generated] 
   theory WP
     (* use why3.BuiltIn.BuiltIn *)