diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index f73d8cdc1cd7a2d8ee39be2214c324b5337c7daa..5d940330603ac683267919647abc0ceb32f3e4dc 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -117,8 +117,8 @@ struct
     begin
       let prefix = Fun.debug phi in
       let sigma = Sigma.create () in
-      List.iter
-        (fun chunk ->
+      List.iteri
+        (fun i chunk ->
            List.iter
              (fun (name,triggers,conditions,m1,m2) ->
                 let mem1 = assigned sigma chunk m1 chunks in
@@ -137,8 +137,8 @@ struct
                     [ (Trigger.of_term value1 :: triggers );
                       (Trigger.of_term value2 :: triggers ) ]
                 in
-                let l_name = Pretty_utils.sfprintf "%s_%s_%a"
-                    prefix name Chunk.pretty chunk in
+                let l_name = Pretty_utils.sfprintf "%s_%s_%a%d"
+                    prefix name Chunk.pretty chunk i in
                 let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
                 Definitions.define_lemma {
                   l_assumed = true ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 233ffc233ca3311a97ada90e071d3e38ee5ac4dc..12f4230be78dc3c929fc275951e98918d101e0ab 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -157,6 +157,9 @@ struct
   let compare a b = rank a - rank b
   let equal = (=)
   let pretty fmt c = Format.pp_print_string fmt (name c)
+  let detailed_pretty fmt = function
+    | M_int i -> Format.fprintf fmt "M%a" Ctypes.pp_int i
+    | m -> Format.pp_print_string fmt (name m)
   let val_of_chunk = function
     | M_int _ | M_char -> L.Int
     | M_f32 -> Cfloat.tau_of_float Ctypes.Float32
@@ -1098,7 +1101,7 @@ and lookup_f f es =
 
 and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
 
-let mchunk c = Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c)
+let mchunk c = Sigs.Mchunk (Pretty_utils.to_string Chunk.detailed_pretty c)
 
 let lookup s e =
   try mchunk (Tmap.find e s)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..11d6b90bb121a763e572ef50afdcb7947288431b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -0,0 +1,275 @@
+# frama-c -wp -wp-rte -wp-no-let [...]
+[kernel] Parsing tests/wp_acsl/struct_fields.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function foo
+[wp] 2 goals scheduled
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'Chunk' 
+---------------------------------------------
+theory Chunk
+  (* 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 *)
+  
+  predicate is_sint8_chunk (m:addr -> int) =
+    forall a:addr. is_sint8 (get m a)
+  
+  predicate is_sint16_chunk (m:addr -> int) =
+    forall a:addr. is_sint16 (get m a)
+  
+  predicate is_sint32_chunk (m:addr -> int) =
+    forall a:addr. is_sint32 (get m a)
+end
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'S1_X' 
+---------------------------------------------
+theory S1_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 *)
+  
+  type S1_X =
+    | S1_X1 (F1_X_a:int) (F1_X_b:int) (F1_X_c:int)
+  
+  (* use frama_c_wp.cint.Cint *)
+  
+  predicate IsS1_X (s:S1_X) =
+    (is_sint8 (F1_X_a s) /\ is_sint16 (F1_X_b s)) /\ is_sint32 (F1_X_c s)
+end
+---------------------------------------------
+--- Context 'typed_foo' 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 shiftfield_F1_X_a (p:addr) : addr = shift p 0
+  
+  function shiftfield_F1_X_b (p:addr) : addr = shift p 1
+  
+  function shiftfield_F1_X_c (p:addr) : addr = shift p 2
+  
+  (* use S1_X *)
+  
+  function Load_S1_X (p:addr) (mchar:addr -> int) (mint:addr -> int) (mint1:
+    addr -> int) : S1_X =
+    S1_X1 (get mchar (shiftfield_F1_X_a p)) (get mint (shiftfield_F1_X_b p))
+    (get mint1 (shiftfield_F1_X_c p))
+  
+  Q_Load_S1_X_update_Mchar0 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
+     separated p 3 q 1 ->
+     Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_eqmem_Mchar0 :
+    forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
+     addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
+     eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
+     eqmem mchar mchar1 q n].
+     included p 3 q n ->
+     eqmem mchar mchar1 q n ->
+     Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_havoc_Mchar0 :
+    forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
+     addr -> int, n:int, p:addr, q:addr
+     [Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
+     separated p 3 q n ->
+     Load_S1_X p (havoc mchar1 mchar q n) mint mint1
+     = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_update_Mint1 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
+     separated p 3 q 1 ->
+     Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint
+  
+  Q_Load_S1_X_eqmem_Mint1 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint1 mint,
+     eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
+     eqmem mint1 mint2 q n].
+     included p 3 q n ->
+     eqmem mint1 mint2 q n ->
+     Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint
+  
+  Q_Load_S1_X_havoc_Mint1 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr
+     [Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
+     separated p 3 q n ->
+     Load_S1_X p mchar (havoc mint2 mint1 q n) mint
+     = Load_S1_X p mchar mint1 mint
+  
+  Q_Load_S1_X_update_Mint2 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
+     separated p 3 q 1 ->
+     Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_eqmem_Mint2 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
+     eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
+     eqmem mint1 mint2 q n].
+     included p 3 q n ->
+     eqmem mint1 mint2 q n ->
+     Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_havoc_Mint2 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr
+     [Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
+     separated p 3 q n ->
+     Load_S1_X p mchar mint (havoc mint2 mint1 q n)
+     = Load_S1_X p mchar mint mint1
+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 Chunk *)
+    
+    (* use S1_X *)
+    
+    (* use Compound *)
+    
+    goal wp_goal :
+      forall t:int -> int, t1:addr -> int, t2:addr -> int, t3:addr -> int, a:
+       addr.
+       region (base a) <= 0 ->
+       is_sint16_chunk t2 ->
+       is_sint32_chunk t3 ->
+       is_sint8_chunk t1 ->
+       linked t ->
+       sconst t1 ->
+       valid_rd t a 3 -> IsS1_X (Load_S1_X a t1 t2 t3) -> valid_rw t a 3
+  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 frama_c_wp.memory.Memory *)
+    
+    (* use Chunk *)
+    
+    (* use S1_X *)
+    
+    (* use Compound *)
+    
+    goal wp_goal :
+      forall t:int -> int, t1:addr -> int, t2:addr -> int, t3:addr -> int, a:
+       addr.
+       region (base a) <= 0 ->
+       is_sint16_chunk t2 ->
+       is_sint32_chunk t3 ->
+       is_sint8_chunk t1 ->
+       linked t -> sconst t1 -> IsS1_X (Load_S1_X a t1 t2 t3) -> valid_rd t a 3
+  end
+[wp] 2 goals generated
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 15):
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0) /\
+      IsS1_X(Load_S1_X(p, Mchar_0, Mint_0, Mint_1)).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+}
+Prove: valid_rd(Malloc_0, p, 3).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 16):
+Let a = Load_S1_X(p, Mchar_0, Mint_0, Mint_1).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0) /\ IsS1_X(a).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rd(Malloc_0, p, 3).
+  (* Initializer *)
+  Init: a = r.
+}
+Prove: valid_rw(Malloc_0, p, 3).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/struct_fields.i b/src/plugins/wp/tests/wp_acsl/struct_fields.i
new file mode 100644
index 0000000000000000000000000000000000000000..93b9c90858aaca1db67542015efe50acabd61703
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/struct_fields.i
@@ -0,0 +1,17 @@
+/* run.config
+   OPT:-wp-rte -wp-no-let -wp-gen -wp-prover why3 -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+struct X {
+  char a ;
+  short b ;
+  int c ;
+};
+
+void foo(struct X* p){
+  struct X r = *p ;
+  *p = r ;
+}
\ No newline at end of file
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index 2842dc0b66878ac96c03c3ff2756011a1b9d2ecf..b1af7c7da5cf23d35ee6e70c4dbfdb89fb3af036 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -60,19 +60,19 @@ theory Compound
   function Load_S2_A (p:addr) (mint:addr -> int) : S2_A =
     S2_A1 (get mint (shiftfield_F2_A_dummy p))
   
-  Q_Load_S2_A_update_Mint :
+  Q_Load_S2_A_update_Mint0 :
     forall mint:addr -> int, p:addr, q:addr, v:int
      [Load_S2_A p (set mint q v)].
      not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
   
-  Q_Load_S2_A_eqmem_Mint :
+  Q_Load_S2_A_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
      [Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
      eqmem mint mint1 q n].
      included p 1 q n ->
      eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
   
-  Q_Load_S2_A_havoc_Mint :
+  Q_Load_S2_A_havoc_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
      [Load_S2_A p (havoc mint1 mint q n)].
      separated p 1 q n ->
diff --git a/src/plugins/wp/tests/wp_tip/chunk_printing.i b/src/plugins/wp/tests/wp_tip/chunk_printing.i
new file mode 100644
index 0000000000000000000000000000000000000000..d4259c4eae03c0578c556b08fa4fa496605055e7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/chunk_printing.i
@@ -0,0 +1,33 @@
+/* run.config
+   OPT: -wp-rte -wp-msg-key state
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+struct V {
+	int* a ;
+	unsigned* b ;
+};
+
+struct V* y ;
+
+/*@
+	assigns \nothing;
+	ensures \result == v->a || \result == y->a;
+*/
+int* get_int(struct V* v);
+
+/*@
+	assigns \nothing;
+	ensures \result == v->b || \result == y->b;
+*/
+unsigned* get_uint(struct V* v);
+
+int main(void){
+	struct V x ;
+	x.a = get_int(&x);
+	x.b = get_uint(&x);
+
+	//@ assert *(x.a) == *(x.b);
+}
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e6de0501d53a2b2f1a10599ec0affcfe32491e76
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_tip/chunk_printing.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function main
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_tip/chunk_printing.i, line 32):
+Let x_1 = « *`v_1 »@L1.
+Let x_2 = « *`v »@L1.
+Assume {
+  Type: is_sint32_chunk(µ:Msint32@L1) /\ is_uint32_chunk(µ:Muint32@L1) /\
+      is_uint32(`x_1) /\ is_sint32(`x_2).
+  (* Heap *)
+  Type: framed(µ:Mptr@L1).
+  Stmt { L1:  }
+  Stmt { x.a = `v;  }
+  (* Call 'get_int' *)
+  Have: ((x@L1.F1_V_a) = `v) \/ (« y->a »@L1 = `v).
+  Stmt { x.b = `v_1;  }
+  (* Call 'get_uint' *)
+  Have: ((x@L1.F1_V_b) = `v_1) \/ (« y->b »@L1 = `v_1).
+}
+Prove: `x_2 = `x_1.
+
+------------------------------------------------------------