diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 6a09fa82d14c464eee53c17d2aeb9a284880fff1..8c88a3af10b1598c786be81e67386363fd551c2a 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -317,7 +317,13 @@ struct
       let f = Context.get cframe in
       f.triggers <- tg :: f.triggers
 
-  let guards f = Lang.hypotheses f.gamma
+  let make_chunk_constraints f =
+    if not (Wp_parameters.RTE.get()) then []
+    else LabelMap.fold (fun _ s l -> M.is_well_formed s :: l) f.labels []
+
+  let guards f =
+    let constraints = in_frame f (fun () -> make_chunk_constraints f) () in
+    Lang.hypotheses f.gamma @ constraints
 
   (* -------------------------------------------------------------------------- *)
   (* --- Environments                                                       --- *)
@@ -438,6 +444,7 @@ struct
         let used = List.filter used_var sigv in
         let parp = List.map snd used in
         let sigp = List.map (fun (lv,_) -> Sig_value lv) used in
+        let domain = make_chunk_constraints frame @ domain in
         let (parm,sigm) =
           LabelMap.fold
             (fun label sigma acc ->
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index fc58ebd54acdc40d95ae067b1d845167f1311420..f10f6da7cef059c0cdeac2385976d338a97f4565 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -94,6 +94,7 @@ let loc_of_int _ _ = ()
 let int_of_loc _ () = e_zero
 
 let domain _obj _l = Sigma.Chunk.Set.empty
+let is_well_formed _s = p_true
 
 let source = "Empty Model"
 
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 18a27402314f57e34edb11a19541f494982bb18f..b717626bea998d91c4a13bdde52727de723ff4f2 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -700,6 +700,8 @@ let domain _obj = function
   | Lfld(_,_,_,ovl) -> Heap.of_overlay (map()) ovl
   | Larr(r,_,_,_,_,_) -> Heap.of_region (map()) r
 
+let is_well_formed _s = Lang.F.p_true
+
 let region_of_loc = function
   | (GarbledMix | Index _) as l -> error "Can not find region of %a" pretty l
   | Lref(r,_,_) | Lraw(r,_,_,_) | Lmem(r,_,_,_)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index e1317a92d9400d83c597a36d0e216ab934cb86a1..233ffc233ca3311a97ada90e071d3e38ee5ac4dc 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -117,7 +117,7 @@ let pointer = Context.create "MemTyped.pointer"
 (* -------------------------------------------------------------------------- *)
 
 type chunk =
-  | M_int
+  | M_int of Ctypes.c_int
   | M_char
   | M_f32
   | M_f64
@@ -128,16 +128,27 @@ module Chunk =
 struct
   type t = chunk
   let self = "typed"
+  let int_rank = function
+    | CBool -> 0
+    | UInt8 -> 1
+    | SInt8 -> 2
+    | UInt16 -> 3
+    | SInt16 -> 4
+    | UInt32 -> 5
+    | SInt32 -> 6
+    | UInt64 -> 7
+    | SInt64 -> 8
+
   let rank = function
-    | M_int -> 0
-    | M_char -> 1
-    | M_f32 -> 2
-    | M_f64 -> 3
-    | M_pointer -> 4
-    | T_alloc -> 5
+    | M_char -> -1
+    | M_int i -> int_rank i
+    | M_f32 -> 9
+    | M_f64 -> 10
+    | M_pointer -> 11
+    | T_alloc -> 12
   let hash = rank
   let name = function
-    | M_int -> "Mint"
+    | M_int _ -> "Mint"
     | M_char -> "Mchar"
     | M_f32 -> "Mf32"
     | M_f64 -> "Mf64"
@@ -147,13 +158,13 @@ struct
   let equal = (=)
   let pretty fmt c = Format.pp_print_string fmt (name c)
   let val_of_chunk = function
-    | M_int | M_char -> L.Int
+    | M_int _ | M_char -> L.Int
     | M_f32 -> Cfloat.tau_of_float Ctypes.Float32
     | M_f64 -> Cfloat.tau_of_float Ctypes.Float64
     | M_pointer -> t_addr
     | T_alloc -> L.Int
   let tau_of_chunk = function
-    | M_int | M_char -> L.Array(t_addr,L.Int)
+    | M_int _ | M_char -> L.Array(t_addr,L.Int)
     | M_pointer -> L.Array(t_addr,t_addr)
     | M_f32 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float32)
     | M_f64 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float64)
@@ -171,7 +182,7 @@ type loc = term (* of type addr *)
 (* --- Utilities on locations                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
-let m_int i = if Ctypes.is_char i then M_char else M_int
+let m_int i = if Ctypes.is_char i then M_char else M_int i
 let m_float = function Float32 -> M_f32 | Float64 -> M_f64
 
 let rec footprint = function
@@ -871,6 +882,51 @@ let frames obj addr = function
       let basename = Chunk.basename_of_chunk m in
       MemMemory.frames ~addr ~offset ~sizeof ~basename tau
 
+(* -------------------------------------------------------------------------- *)
+(* --- Chunk element type                                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+module ChunkContent = WpContext.Generator(Chunk)
+    (struct
+      let name = "MemTyped.ChunkContent"
+      type key = Chunk.t
+      type data = lfun
+
+      let int_kind = function
+        | M_char -> Ctypes.c_char ()
+        | M_int k -> k
+        | _ -> failwith "MemTyped asked constraint for non int type"
+
+      let generate c =
+        let k = int_kind c in
+        let p = Lang.freshvar ~basename:"m" (Chunk.tau_of_chunk c) in
+        let m = e_var p in
+        let name = Format.asprintf "is_%a_chunk" Ctypes.pp_int k in
+        let lfun = Lang.generated_p name in
+        let l = Lang.freshvar ~basename:"l" (Lang.t_addr()) in
+        let is_int = Cint.range k in
+        let def = p_forall [l] (is_int (F.e_get m (e_var l))) in
+        Definitions.define_symbol {
+          d_lfun = lfun ; d_types = 0 ;
+          d_params = [p] ;
+          d_definition = Predicate(Def, def) ;
+          d_cluster = cluster ~id:"Chunk" ~title:"Chunk type constraint" () ;
+        } ;
+        lfun
+
+      let compile = Lang.local generate
+    end)
+
+let is_chunk sigma = function
+  | M_int _ | M_char as m ->
+      F.p_call (ChunkContent.get m) [ Sigma.value sigma m ]
+  | _ ->
+      p_true
+
+let is_well_formed sigma =
+  let open Sigma in
+  p_conj (Chunk.Set.fold (fun c l -> is_chunk sigma c :: l) (domain sigma) [])
+
 (* -------------------------------------------------------------------------- *)
 (* --- Loader                                                             --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index fd09f824c2c909084efb61b68f5abcd6ab51956e..e07a9ad259adcc5d0bf587c98ba2fc57ddb48caf 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1267,6 +1267,9 @@ struct
           (fun m s -> Heap.Set.add (Mem m) s)
           (M.domain obj (mloc_of_loc l)) Heap.Set.empty
 
+  let is_well_formed sigma =
+    M.is_well_formed sigma.mem
+
   (* -------------------------------------------------------------------------- *)
 
 end
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 19f271238f13ffc3b9049c6f4b2695e8488b2f78..c734daed7a612645c844dd3351f711eb9328bfcf 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -183,6 +183,8 @@ let domain _obj l =
   try Heap.Set.singleton (fst (access l))
   with _ -> Heap.Set.empty
 
+let is_well_formed _s = p_true
+
 let value sigma l =
   let m,ks = access l in
   let x = Sigma.get sigma m in
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 72d1972ac59d46b817f11284ffa445c843d75af7..6f8f2636caefcc70f64d661a1c46e85e6f56c81a 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -412,6 +412,10 @@ sig
       the given C-type. It is safe to retun an over-approximation of the
       chunks involved. *)
 
+  val is_well_formed : sigma -> pred
+  (** Provides the constraint corresponding to the kind of data stored by all
+      chunks in sigma. *)
+
   val load : sigma -> c_object -> loc -> loc value
   (** Return the value of the object of the given type at the given location in
       the given memory state. *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 6108632979a7df27f72538793ef5881df0f49d37..b8389519cc2b552a62d28100f2ae7c1b8b7ecab1 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -207,11 +207,15 @@ struct
   let intersect_vc vc p =
     Vars.intersect (F.varsp p) vc.vars || Conditions.intersect p vc.hyps
 
-  let state_vc ?descr ?stmt state vc =
+  let state_vc ?descr ?stmt sigma state vc =
     let path = match stmt with
       | None -> vc.path
       | Some s -> S.add s vc.path in
-    let hyps = Conditions.state ?stmt ?descr state vc.hyps in
+    let hyps =
+      if not (Wp_parameters.RTE.get()) then vc.hyps
+      else Conditions.domain [M.is_well_formed sigma] vc.hyps
+    in
+    let hyps = Conditions.state ?stmt ?descr state hyps in
     { vc with path ; hyps }
 
   let assume_vc ?descr ?hpid ?stmt ?warn
@@ -640,7 +644,7 @@ struct
         | Some { labels = lbl::_ } ->
             Some (Pretty_utils.to_string Printer.pp_label lbl) in
       let state = Mstate.state state sigma in
-      gmap (state_vc ?descr ?stmt state) vcs
+      gmap (state_vc ?descr ?stmt sigma state) vcs
     with Not_found -> vcs
 
   let label wenv stmt label wp =
diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing.i b/src/plugins/wp/tests/wp_acsl/chunk_typing.i
new file mode 100644
index 0000000000000000000000000000000000000000..5a7f30a3950cd024d3738e03553708bb7c472423
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/chunk_typing.i
@@ -0,0 +1,54 @@
+/* run.config
+   OPT: -wp-rte
+*/
+/* run.config_qualif
+   OPT: -wp-rte
+*/
+
+const char x[10];
+
+/*@
+  requires \valid(&i8[0..9])  && \valid(&u8[0..9])  && \valid(&i16[0..9])
+        && \valid(&u16[0..9]) && \valid(&i32[0..9]) && \valid(&u32[0..9])
+        && \valid(&i64[0..9]) && \valid(&u64[0..9]);
+  ensures
+    \forall integer k ; 0 <= k < 10 ==> x[k]+8
+                                     == i8[k]+7  == u8[k]+6
+                                     == i16[k]+5 == u16[k]+4
+                                     == i32[k]+3 == u32[k]+2
+                                     == i64[k]+1 == u64[k];
+*/
+void function(signed char i8[10],
+              unsigned char u8[10],
+              signed short i16[10],
+              unsigned short u16[10],
+              signed int i32[10],
+              unsigned int u32[10],
+              signed long long int i64[10],
+              unsigned long long int u64[10])
+{
+  /*@
+    loop invariant 0 <= i <= 10;
+    loop invariant \forall integer k ; 0 <= k < i ==> i8[k] == 1 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u8[k] == 2 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> i16[k] == 3 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u16[k] == 4 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> i32[k] == 5 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u32[k] == 6 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> i64[k] == 7 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u64[k] == 8 ;
+    loop assigns i, i8[0..9], u8[0..9], i16[0..9], u16[0..9],
+                    i32[0..9], u32[0..9], i64[0..9], u64[0..9] ;
+    loop variant 10-i;
+  */
+  for (int i = 0; i < 10; ++i) {
+    i8[i] = 1;
+    u8[i] = 2;
+    i16[i] = 3;
+    u16[i] = 4;
+    i32[i] = 5;
+    u32[i] = 6;
+    i64[i] = 7;
+    u64[i] = 8;
+  }
+}
diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
new file mode 100644
index 0000000000000000000000000000000000000000..28ffabaec02d2fef6f2b767e8cf9320b5e0c77a7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
@@ -0,0 +1,47 @@
+/* run.config
+   OPT: -wp-gen -wp-rte -wp-prover why3 -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   OPT: -wp-rte -wp-coq-script tests/wp_acsl/chunk_typing_usable.script -wp-prover alt-ergo,native:coq
+*/
+
+/*@
+  axiomatic Occ{
+    logic integer occ{L}(int value, int* p, integer f, integer t)
+      reads p[f .. t-1];
+
+    axiom empty{L}:
+      \forall int v, int* p, integer f, t;
+        f >= t ==> occ{L}(v, p, f, t) == 0;
+
+    axiom is{L}:
+      \forall int v, int* p, integer f, t;
+        (f < t && p[t-1] == v) ==> occ(v,p,f,t) == 1+occ(v,p,f,t-1);
+
+    axiom isnt{L}:
+      \forall int v, int* p, integer f, t;
+        (f < t && p[t-1] != v) ==> occ(v,p,f,t) == occ(v,p,f,t-1);
+  }
+*/
+
+/*@
+  requires b < e <= 1000 ;
+  ensures \forall int v ; v != a[e-1] ==> occ(v,a,b,e) == occ(v,a,b,e-1);
+*/
+void usable_axiom(int* a, unsigned b, unsigned e){
+
+}
+
+/*@
+  lemma provable_lemma:
+    \forall int v, int* p, integer f, s, t;
+    f <= s <= t ==> occ(v,p,f,t) == occ(v,p,f,s) + occ(v,p,s,t) ;
+*/
+
+/*@
+  requires b < s <= e;
+  ensures \forall int v ; occ(v,a,b,e) == occ(v,a,b,s) + occ(v,a,s,e) ;
+*/
+void usable_lemma(int* a, unsigned b, unsigned s, unsigned e){
+
+}
diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script
new file mode 100644
index 0000000000000000000000000000000000000000..7e86db5b5e787c3126afb74e22e641ba12b9c35c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script
@@ -0,0 +1,37 @@
+(* Generated by Frama-C WP *)
+
+Goal typed_lemma_provable_lemma.
+Hint property,provable_lemma.
+Proof.
+  Import Compound.
+
+  Ltac norm := repeat(match goal with
+  | [ _ : _ |- context [ (?i + 1 - 1)%Z ]] => replace (i + 1 - 1)%Z with i by omega
+  | [ _ : _ |- context [ (0 + ?i)%Z ]] => replace (0 + i)%Z with i by omega
+  | [ _ : _ |- context [ (?i + 0)%Z ]] => replace (i + 0)%Z with i by omega
+  end).
+  intros e from cut to.
+  generalize dependent cut.
+  induction to using Z_induction with (m := from) ; intros cut mem page Hct Hfc Hm He.
+  * repeat(rewrite A_Occ.Q_empty ; auto ; try omega).
+  * assert(EqNeq: { mem.[ (shift_sint32 page to) ] = e } + { mem.[ (shift_sint32 page to) ] <> e }) by
+      repeat(decide equality).
+    assert(Cut: (cut < to + 1 \/ cut = to + 1)%Z ) by omega ; inversion Cut as [ Inf | Eq ].
+    + inversion_clear EqNeq as [ Eq | Neq ].
+      - rewrite <- Eq.
+        replace (mem .[ shift_sint32 page to]) with (mem .[ shift_sint32 page (to + 1 - 1)]) by (norm ; auto).
+        rewrite <- A_Occ.Q_is with (i := (to+1)%Z) ;
+        [ rewrite <- A_Occ.Q_is with (i := (to+1)%Z) | | | | |] ;
+          norm ; try rewrite Eq ; auto ; try omega.
+        assert(Simpl: forall x y z : Z, (x + y = z)%Z -> (1 + x + y = 1 + z)%Z) by (intros ; omega).
+        apply Simpl.
+        apply IHto ; auto ; omega.
+      - rewrite <- A_Occ.Q_isnt with (i := (to+1)%Z) ;
+        [ rewrite <- A_Occ.Q_isnt with (i := (to+1)%Z) | | | | |] ;
+          norm ; auto ; try omega.
+        apply IHto ; auto ; omega.
+    + rewrite Eq.
+      rewrite A_Occ.Q_empty ; auto ; try omega.
+Qed.
+
+
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8f21ca532c0fe39f1713a5a780ff7e2cb2fa5f56
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -0,0 +1,1889 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function function
+------------------------------------------------------------
+  Function function
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/chunk_typing.i, line 15) in 'function':
+Let a = shift_sint8(i8_0, 0).
+Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, 10).
+Let a_2 = shift_uint8(u8_0, 0).
+Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 10).
+Let a_4 = shift_sint16(i16_0, 0).
+Let a_5 = havoc(Mint_undef_1, Mint_1, a_4, 10).
+Let a_6 = shift_uint16(u16_0, 0).
+Let a_7 = havoc(Mint_undef_2, Mint_2, a_6, 10).
+Let a_8 = shift_sint32(i32_0, 0).
+Let a_9 = havoc(Mint_undef_3, Mint_3, a_8, 10).
+Let a_10 = shift_uint32(u32_0, 0).
+Let a_11 = havoc(Mint_undef_4, Mint_4, a_10, 10).
+Let a_12 = shift_sint64(i64_0, 0).
+Let a_13 = havoc(Mint_undef_5, Mint_5, a_12, 10).
+Let a_14 = shift_uint64(u64_0, 0).
+Let a_15 = havoc(Mint_undef_6, Mint_6, a_14, 10).
+Let a_16 = a_1[shift_sint8(i8_0, i)].
+Let a_17 = a_3[shift_uint8(u8_0, i)].
+Let a_18 = a_5[shift_sint16(i16_0, i)].
+Let a_19 = a_7[shift_uint16(u16_0, i)].
+Let a_20 = a_9[shift_sint32(i32_0, i)].
+Let a_21 = a_11[shift_uint32(u32_0, i)].
+Let a_22 = a_13[shift_sint64(i64_0, i)].
+Assume {
+  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_3) /\
+      is_sint64_chunk(Mint_5) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_2) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_6) /\ is_uint8_chunk(Mint_0) /\ is_sint32(i_1) /\
+      is_sint16_chunk(a_5) /\ is_sint32_chunk(a_9) /\
+      is_sint64_chunk(a_13) /\ is_sint8_chunk(a_1) /\ is_uint16_chunk(a_7) /\
+      is_uint32_chunk(a_11) /\ is_uint64_chunk(a_15) /\ is_uint8_chunk(a_3).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      IsArray1_sint8(x) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 9).
+  (* Initializer *)
+  Init: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (x[i_2] = 0))).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_4, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a, 10) /\
+      valid_rw(Malloc_0, a_6, 10) /\ valid_rw(Malloc_0, a_10, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_2, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_15[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_13[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_11[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_9[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_7[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_5[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_3[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+      (a_1[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i_1) /\ (i_1 <= 10).
+  (* Else *)
+  Have: 10 <= i_1.
+}
+Prove: (a_16 = (1 + x[i])) /\ (a_17 = (1 + a_16)) /\ (a_18 = (1 + a_17)) /\
+    (a_19 = (1 + a_18)) /\ (a_20 = (1 + a_19)) /\ (a_21 = (1 + a_20)) /\
+    (a_22 = (1 + a_21)) /\ (a_15[shift_uint64(u64_0, i)] = (1 + a_22)).
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 31):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_1, Mint_1, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_23[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_21[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_19[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_17[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_15[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_13[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_11[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_9[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: (-1) <= i.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 31):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 32):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_1, Mint_1, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Let a_24 = a_9[a_7 <- 1].
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_24) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_sint8(i8_0, i_1)] = 1.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 32):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 33):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_0, Mint_0, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_4, Mint_4, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_5, Mint_5, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_6, Mint_6, a_22, 10).
+Let a_24 = a_11[a_6 <- 2].
+Assume {
+  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
+      is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_4) /\ is_uint32_chunk(Mint_5) /\
+      is_uint64_chunk(Mint_6) /\ is_uint8_chunk(Mint_0) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_24).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_uint8(u8_0, i_1)] = 2.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 33):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 34):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_1, Mint_1, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Let a_24 = a_13[a_5 <- 3].
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_24) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_sint16(i16_0, i_1)] = 3.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 34):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 35):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_0, Mint_0, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Let a_24 = a_15[a_4 <- 4].
+Assume {
+  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
+      is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_0) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_24) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_uint16(u16_0, i_1)] = 4.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 35):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 36):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_0, Mint_0, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Let a_24 = a_17[a_3 <- 5].
+Assume {
+  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_0) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_24) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_sint32(i32_0, i_1)] = 5.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 36):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 37):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_4, Mint_4, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_0, Mint_0, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Let a_24 = a_19[a_2 <- 6].
+Assume {
+  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
+      is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_4) /\ is_uint32_chunk(Mint_0) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_24) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_uint32(u32_0, i_1)] = 6.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 37):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 38):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_0, Mint_0, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Let a_24 = a_21[a_1 <- 7].
+Assume {
+  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
+      is_sint64_chunk(Mint_0) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_24) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_sint64(i64_0, i_1)] = 7.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 39):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_4, Mint_4, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_5, Mint_5, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_0, Mint_0, a_22, 10).
+Let a_24 = a_23[a <- 8].
+Assume {
+  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
+      is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_4) /\ is_uint32_chunk(Mint_5) /\
+      is_uint64_chunk(Mint_0) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint32(1 + i) /\ is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_24) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Goal *)
+  When: (0 <= i_1) /\ (i_1 <= i).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_23[shift_uint64(u64_0, i_2)] = 8))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_21[shift_sint64(i64_0, i_2)] = 7))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_19[shift_uint32(u32_0, i_2)] = 6))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_17[shift_sint32(i32_0, i_2)] = 5))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_15[shift_uint16(u16_0, i_2)] = 4))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_13[shift_sint16(i16_0, i_2)] = 3))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_11[shift_uint8(u8_0, i_2)] = 2))).
+  (* Invariant *)
+  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+      (a_9[shift_sint8(i8_0, i_2)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= 2147483646.
+}
+Prove: a_24[shift_uint64(u64_0, i_1)] = 8.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 39):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 45):
+Let a = shift_sint8(i8_0, 0).
+Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, 10).
+Let a_2 = shift_uint8(u8_0, 0).
+Let a_3 = havoc(Mint_undef_6, Mint_6, a_2, 10).
+Let a_4 = shift_sint16(i16_0, 0).
+Let a_5 = havoc(Mint_undef_0, Mint_0, a_4, 10).
+Let a_6 = shift_uint16(u16_0, 0).
+Let a_7 = havoc(Mint_undef_3, Mint_3, a_6, 10).
+Let a_8 = shift_sint32(i32_0, 0).
+Let a_9 = havoc(Mint_undef_1, Mint_1, a_8, 10).
+Let a_10 = shift_uint32(u32_0, 0).
+Let a_11 = havoc(Mint_undef_4, Mint_4, a_10, 10).
+Let a_12 = shift_sint64(i64_0, 0).
+Let a_13 = havoc(Mint_undef_2, Mint_2, a_12, 10).
+Let a_14 = shift_uint64(u64_0, 0).
+Let a_15 = havoc(Mint_undef_5, Mint_5, a_14, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_5) /\ is_sint32_chunk(a_9) /\
+      is_sint64_chunk(a_13) /\ is_sint8_chunk(a_1) /\ is_uint16_chunk(a_7) /\
+      is_uint32_chunk(a_11) /\ is_uint64_chunk(a_15) /\ is_uint8_chunk(a_3).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_4, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a, 10) /\
+      valid_rw(Malloc_0, a_6, 10) /\ valid_rw(Malloc_0, a_10, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_2, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_15[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_13[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_11[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_9[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_7[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_5[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_3[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_1[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+}
+Prove: valid_rw(Malloc_0, shift_sint8(i8_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 46):
+Let a = shift_sint8(i8_0, i).
+Let a_1 = shift_sint8(i8_0, 0).
+Let a_2 = havoc(Mchar_undef_0, Mchar_0, a_1, 10).
+Let a_3 = shift_uint8(u8_0, 0).
+Let a_4 = havoc(Mint_undef_6, Mint_6, a_3, 10).
+Let a_5 = shift_sint16(i16_0, 0).
+Let a_6 = havoc(Mint_undef_0, Mint_0, a_5, 10).
+Let a_7 = shift_uint16(u16_0, 0).
+Let a_8 = havoc(Mint_undef_3, Mint_3, a_7, 10).
+Let a_9 = shift_sint32(i32_0, 0).
+Let a_10 = havoc(Mint_undef_1, Mint_1, a_9, 10).
+Let a_11 = shift_uint32(u32_0, 0).
+Let a_12 = havoc(Mint_undef_4, Mint_4, a_11, 10).
+Let a_13 = shift_sint64(i64_0, 0).
+Let a_14 = havoc(Mint_undef_2, Mint_2, a_13, 10).
+Let a_15 = shift_uint64(u64_0, 0).
+Let a_16 = havoc(Mint_undef_5, Mint_5, a_15, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_6) /\ is_sint32_chunk(a_10) /\
+      is_sint64_chunk(a_14) /\ is_sint8_chunk(a_2) /\ is_uint16_chunk(a_8) /\
+      is_uint32_chunk(a_12) /\ is_uint64_chunk(a_16) /\
+      is_uint8_chunk(a_4) /\ is_sint8_chunk(a_2[a <- 1]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_5, 10) /\ valid_rw(Malloc_0, a_9, 10) /\
+      valid_rw(Malloc_0, a_13, 10) /\ valid_rw(Malloc_0, a_1, 10) /\
+      valid_rw(Malloc_0, a_7, 10) /\ valid_rw(Malloc_0, a_11, 10) /\
+      valid_rw(Malloc_0, a_15, 10) /\ valid_rw(Malloc_0, a_3, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_16[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_14[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_12[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_10[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_8[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_6[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_4[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_2[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: valid_rw(Malloc_0, shift_uint8(u8_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 47):
+Let a = shift_uint8(u8_0, i).
+Let a_1 = shift_sint8(i8_0, i).
+Let a_2 = shift_sint8(i8_0, 0).
+Let a_3 = havoc(Mchar_undef_0, Mchar_0, a_2, 10).
+Let a_4 = shift_uint8(u8_0, 0).
+Let a_5 = havoc(Mint_undef_6, Mint_6, a_4, 10).
+Let a_6 = shift_sint16(i16_0, 0).
+Let a_7 = havoc(Mint_undef_0, Mint_0, a_6, 10).
+Let a_8 = shift_uint16(u16_0, 0).
+Let a_9 = havoc(Mint_undef_3, Mint_3, a_8, 10).
+Let a_10 = shift_sint32(i32_0, 0).
+Let a_11 = havoc(Mint_undef_1, Mint_1, a_10, 10).
+Let a_12 = shift_uint32(u32_0, 0).
+Let a_13 = havoc(Mint_undef_4, Mint_4, a_12, 10).
+Let a_14 = shift_sint64(i64_0, 0).
+Let a_15 = havoc(Mint_undef_2, Mint_2, a_14, 10).
+Let a_16 = shift_uint64(u64_0, 0).
+Let a_17 = havoc(Mint_undef_5, Mint_5, a_16, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_7) /\ is_sint32_chunk(a_11) /\
+      is_sint64_chunk(a_15) /\ is_sint8_chunk(a_3) /\ is_uint16_chunk(a_9) /\
+      is_uint32_chunk(a_13) /\ is_uint64_chunk(a_17) /\
+      is_uint8_chunk(a_5) /\ is_sint8_chunk(a_3[a_1 <- 1]) /\
+      is_uint8_chunk(a_5[a <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_6, 10) /\ valid_rw(Malloc_0, a_10, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_2, 10) /\
+      valid_rw(Malloc_0, a_8, 10) /\ valid_rw(Malloc_0, a_12, 10) /\
+      valid_rw(Malloc_0, a_16, 10) /\ valid_rw(Malloc_0, a_4, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_17[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_15[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_13[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_11[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_9[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_7[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_5[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_3[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: valid_rw(Malloc_0, shift_sint16(i16_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 48):
+Let a = shift_sint16(i16_0, i).
+Let a_1 = shift_uint8(u8_0, i).
+Let a_2 = shift_sint8(i8_0, i).
+Let a_3 = shift_sint8(i8_0, 0).
+Let a_4 = havoc(Mchar_undef_0, Mchar_0, a_3, 10).
+Let a_5 = shift_uint8(u8_0, 0).
+Let a_6 = havoc(Mint_undef_6, Mint_6, a_5, 10).
+Let a_7 = shift_sint16(i16_0, 0).
+Let a_8 = havoc(Mint_undef_0, Mint_0, a_7, 10).
+Let a_9 = shift_uint16(u16_0, 0).
+Let a_10 = havoc(Mint_undef_3, Mint_3, a_9, 10).
+Let a_11 = shift_sint32(i32_0, 0).
+Let a_12 = havoc(Mint_undef_1, Mint_1, a_11, 10).
+Let a_13 = shift_uint32(u32_0, 0).
+Let a_14 = havoc(Mint_undef_4, Mint_4, a_13, 10).
+Let a_15 = shift_sint64(i64_0, 0).
+Let a_16 = havoc(Mint_undef_2, Mint_2, a_15, 10).
+Let a_17 = shift_uint64(u64_0, 0).
+Let a_18 = havoc(Mint_undef_5, Mint_5, a_17, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_8) /\ is_sint32_chunk(a_12) /\
+      is_sint64_chunk(a_16) /\ is_sint8_chunk(a_4) /\
+      is_uint16_chunk(a_10) /\ is_uint32_chunk(a_14) /\
+      is_uint64_chunk(a_18) /\ is_uint8_chunk(a_6) /\
+      is_sint16_chunk(a_8[a <- 3]) /\ is_sint8_chunk(a_4[a_2 <- 1]) /\
+      is_uint8_chunk(a_6[a_1 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_7, 10) /\ valid_rw(Malloc_0, a_11, 10) /\
+      valid_rw(Malloc_0, a_15, 10) /\ valid_rw(Malloc_0, a_3, 10) /\
+      valid_rw(Malloc_0, a_9, 10) /\ valid_rw(Malloc_0, a_13, 10) /\
+      valid_rw(Malloc_0, a_17, 10) /\ valid_rw(Malloc_0, a_5, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_18[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_16[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_14[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_12[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_10[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_8[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_6[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_4[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: valid_rw(Malloc_0, shift_uint16(u16_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 49):
+Let a = shift_uint16(u16_0, i).
+Let a_1 = shift_sint16(i16_0, i).
+Let a_2 = shift_uint8(u8_0, i).
+Let a_3 = shift_sint8(i8_0, i).
+Let a_4 = shift_sint8(i8_0, 0).
+Let a_5 = havoc(Mchar_undef_0, Mchar_0, a_4, 10).
+Let a_6 = shift_uint8(u8_0, 0).
+Let a_7 = havoc(Mint_undef_6, Mint_6, a_6, 10).
+Let a_8 = shift_sint16(i16_0, 0).
+Let a_9 = havoc(Mint_undef_0, Mint_0, a_8, 10).
+Let a_10 = shift_uint16(u16_0, 0).
+Let a_11 = havoc(Mint_undef_3, Mint_3, a_10, 10).
+Let a_12 = shift_sint32(i32_0, 0).
+Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
+Let a_14 = shift_uint32(u32_0, 0).
+Let a_15 = havoc(Mint_undef_4, Mint_4, a_14, 10).
+Let a_16 = shift_sint64(i64_0, 0).
+Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
+Let a_18 = shift_uint64(u64_0, 0).
+Let a_19 = havoc(Mint_undef_5, Mint_5, a_18, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_9) /\ is_sint32_chunk(a_13) /\
+      is_sint64_chunk(a_17) /\ is_sint8_chunk(a_5) /\
+      is_uint16_chunk(a_11) /\ is_uint32_chunk(a_15) /\
+      is_uint64_chunk(a_19) /\ is_uint8_chunk(a_7) /\
+      is_sint16_chunk(a_9[a_1 <- 3]) /\ is_sint8_chunk(a_5[a_3 <- 1]) /\
+      is_uint16_chunk(a_11[a <- 4]) /\ is_uint8_chunk(a_7[a_2 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_8, 10) /\ valid_rw(Malloc_0, a_12, 10) /\
+      valid_rw(Malloc_0, a_16, 10) /\ valid_rw(Malloc_0, a_4, 10) /\
+      valid_rw(Malloc_0, a_10, 10) /\ valid_rw(Malloc_0, a_14, 10) /\
+      valid_rw(Malloc_0, a_18, 10) /\ valid_rw(Malloc_0, a_6, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_19[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_17[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_15[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_13[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_11[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_9[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_7[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_5[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: valid_rw(Malloc_0, shift_sint32(i32_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 50):
+Let a = shift_sint32(i32_0, i).
+Let a_1 = shift_uint16(u16_0, i).
+Let a_2 = shift_sint16(i16_0, i).
+Let a_3 = shift_uint8(u8_0, i).
+Let a_4 = shift_sint8(i8_0, i).
+Let a_5 = shift_sint8(i8_0, 0).
+Let a_6 = havoc(Mchar_undef_0, Mchar_0, a_5, 10).
+Let a_7 = shift_uint8(u8_0, 0).
+Let a_8 = havoc(Mint_undef_6, Mint_6, a_7, 10).
+Let a_9 = shift_sint16(i16_0, 0).
+Let a_10 = havoc(Mint_undef_0, Mint_0, a_9, 10).
+Let a_11 = shift_uint16(u16_0, 0).
+Let a_12 = havoc(Mint_undef_3, Mint_3, a_11, 10).
+Let a_13 = shift_sint32(i32_0, 0).
+Let a_14 = havoc(Mint_undef_1, Mint_1, a_13, 10).
+Let a_15 = shift_uint32(u32_0, 0).
+Let a_16 = havoc(Mint_undef_4, Mint_4, a_15, 10).
+Let a_17 = shift_sint64(i64_0, 0).
+Let a_18 = havoc(Mint_undef_2, Mint_2, a_17, 10).
+Let a_19 = shift_uint64(u64_0, 0).
+Let a_20 = havoc(Mint_undef_5, Mint_5, a_19, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_10) /\ is_sint32_chunk(a_14) /\
+      is_sint64_chunk(a_18) /\ is_sint8_chunk(a_6) /\
+      is_uint16_chunk(a_12) /\ is_uint32_chunk(a_16) /\
+      is_uint64_chunk(a_20) /\ is_uint8_chunk(a_8) /\
+      is_sint16_chunk(a_10[a_2 <- 3]) /\ is_sint32_chunk(a_14[a <- 5]) /\
+      is_sint8_chunk(a_6[a_4 <- 1]) /\ is_uint16_chunk(a_12[a_1 <- 4]) /\
+      is_uint8_chunk(a_8[a_3 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_9, 10) /\ valid_rw(Malloc_0, a_13, 10) /\
+      valid_rw(Malloc_0, a_17, 10) /\ valid_rw(Malloc_0, a_5, 10) /\
+      valid_rw(Malloc_0, a_11, 10) /\ valid_rw(Malloc_0, a_15, 10) /\
+      valid_rw(Malloc_0, a_19, 10) /\ valid_rw(Malloc_0, a_7, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_20[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_18[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_16[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_14[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_12[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_10[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_8[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_6[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: valid_rw(Malloc_0, shift_uint32(u32_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 51):
+Let a = shift_uint32(u32_0, i).
+Let a_1 = shift_sint32(i32_0, i).
+Let a_2 = shift_uint16(u16_0, i).
+Let a_3 = shift_sint16(i16_0, i).
+Let a_4 = shift_uint8(u8_0, i).
+Let a_5 = shift_sint8(i8_0, i).
+Let a_6 = shift_sint8(i8_0, 0).
+Let a_7 = havoc(Mchar_undef_0, Mchar_0, a_6, 10).
+Let a_8 = shift_uint8(u8_0, 0).
+Let a_9 = havoc(Mint_undef_6, Mint_6, a_8, 10).
+Let a_10 = shift_sint16(i16_0, 0).
+Let a_11 = havoc(Mint_undef_0, Mint_0, a_10, 10).
+Let a_12 = shift_uint16(u16_0, 0).
+Let a_13 = havoc(Mint_undef_3, Mint_3, a_12, 10).
+Let a_14 = shift_sint32(i32_0, 0).
+Let a_15 = havoc(Mint_undef_1, Mint_1, a_14, 10).
+Let a_16 = shift_uint32(u32_0, 0).
+Let a_17 = havoc(Mint_undef_4, Mint_4, a_16, 10).
+Let a_18 = shift_sint64(i64_0, 0).
+Let a_19 = havoc(Mint_undef_2, Mint_2, a_18, 10).
+Let a_20 = shift_uint64(u64_0, 0).
+Let a_21 = havoc(Mint_undef_5, Mint_5, a_20, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_11) /\ is_sint32_chunk(a_15) /\
+      is_sint64_chunk(a_19) /\ is_sint8_chunk(a_7) /\
+      is_uint16_chunk(a_13) /\ is_uint32_chunk(a_17) /\
+      is_uint64_chunk(a_21) /\ is_uint8_chunk(a_9) /\
+      is_sint16_chunk(a_11[a_3 <- 3]) /\ is_sint32_chunk(a_15[a_1 <- 5]) /\
+      is_sint8_chunk(a_7[a_5 <- 1]) /\ is_uint16_chunk(a_13[a_2 <- 4]) /\
+      is_uint32_chunk(a_17[a <- 6]) /\ is_uint8_chunk(a_9[a_4 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_10, 10) /\ valid_rw(Malloc_0, a_14, 10) /\
+      valid_rw(Malloc_0, a_18, 10) /\ valid_rw(Malloc_0, a_6, 10) /\
+      valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_21[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_19[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_17[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_15[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_13[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_11[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_9[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_7[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: valid_rw(Malloc_0, shift_sint64(i64_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/chunk_typing.i, line 52):
+Let a = shift_sint64(i64_0, i).
+Let a_1 = shift_uint32(u32_0, i).
+Let a_2 = shift_sint32(i32_0, i).
+Let a_3 = shift_uint16(u16_0, i).
+Let a_4 = shift_sint16(i16_0, i).
+Let a_5 = shift_uint8(u8_0, i).
+Let a_6 = shift_sint8(i8_0, i).
+Let a_7 = shift_sint8(i8_0, 0).
+Let a_8 = havoc(Mchar_undef_0, Mchar_0, a_7, 10).
+Let a_9 = shift_uint8(u8_0, 0).
+Let a_10 = havoc(Mint_undef_6, Mint_6, a_9, 10).
+Let a_11 = shift_sint16(i16_0, 0).
+Let a_12 = havoc(Mint_undef_0, Mint_0, a_11, 10).
+Let a_13 = shift_uint16(u16_0, 0).
+Let a_14 = havoc(Mint_undef_3, Mint_3, a_13, 10).
+Let a_15 = shift_sint32(i32_0, 0).
+Let a_16 = havoc(Mint_undef_1, Mint_1, a_15, 10).
+Let a_17 = shift_uint32(u32_0, 0).
+Let a_18 = havoc(Mint_undef_4, Mint_4, a_17, 10).
+Let a_19 = shift_sint64(i64_0, 0).
+Let a_20 = havoc(Mint_undef_2, Mint_2, a_19, 10).
+Let a_21 = shift_uint64(u64_0, 0).
+Let a_22 = havoc(Mint_undef_5, Mint_5, a_21, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_12) /\ is_sint32_chunk(a_16) /\
+      is_sint64_chunk(a_20) /\ is_sint8_chunk(a_8) /\
+      is_uint16_chunk(a_14) /\ is_uint32_chunk(a_18) /\
+      is_uint64_chunk(a_22) /\ is_uint8_chunk(a_10) /\
+      is_sint16_chunk(a_12[a_4 <- 3]) /\ is_sint32_chunk(a_16[a_2 <- 5]) /\
+      is_sint64_chunk(a_20[a <- 7]) /\ is_sint8_chunk(a_8[a_6 <- 1]) /\
+      is_uint16_chunk(a_14[a_3 <- 4]) /\ is_uint32_chunk(a_18[a_1 <- 6]) /\
+      is_uint8_chunk(a_10[a_5 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_11, 10) /\ valid_rw(Malloc_0, a_15, 10) /\
+      valid_rw(Malloc_0, a_19, 10) /\ valid_rw(Malloc_0, a_7, 10) /\
+      valid_rw(Malloc_0, a_13, 10) /\ valid_rw(Malloc_0, a_17, 10) /\
+      valid_rw(Malloc_0, a_21, 10) /\ valid_rw(Malloc_0, a_9, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_22[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_20[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_18[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_16[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_14[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_12[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_10[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_8[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: valid_rw(Malloc_0, shift_uint64(u64_0, i), 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,signed_overflow' (file tests/wp_acsl/chunk_typing.i, line 44):
+Let a = shift_uint64(u64_0, i).
+Let a_1 = shift_sint64(i64_0, i).
+Let a_2 = shift_uint32(u32_0, i).
+Let a_3 = shift_sint32(i32_0, i).
+Let a_4 = shift_uint16(u16_0, i).
+Let a_5 = shift_sint16(i16_0, i).
+Let a_6 = shift_uint8(u8_0, i).
+Let a_7 = shift_sint8(i8_0, i).
+Let a_8 = shift_sint8(i8_0, 0).
+Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
+Let a_10 = shift_uint8(u8_0, 0).
+Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
+Let a_12 = shift_sint16(i16_0, 0).
+Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
+Let a_14 = shift_uint16(u16_0, 0).
+Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
+Let a_16 = shift_sint32(i32_0, 0).
+Let a_17 = havoc(Mint_undef_1, Mint_1, a_16, 10).
+Let a_18 = shift_uint32(u32_0, 0).
+Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
+Let a_20 = shift_sint64(i64_0, 0).
+Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
+Let a_22 = shift_uint64(u64_0, 0).
+Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
+      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
+      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
+      is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
+      is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
+      is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
+      is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
+      is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
+      is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
+      is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
+      is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
+  (* Heap *)
+  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
+      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
+      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
+      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
+      linked(Malloc_0) /\ sconst(Mchar_0).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
+      valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
+      valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
+      valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_23[shift_uint64(u64_0, i_1)] = 8))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_21[shift_sint64(i64_0, i_1)] = 7))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_19[shift_uint32(u32_0, i_1)] = 6))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_17[shift_sint32(i32_0, i_1)] = 5))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_15[shift_uint16(u16_0, i_1)] = 4))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_13[shift_sint16(i16_0, i_1)] = 3))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_11[shift_uint8(u8_0, i_1)] = 2))).
+  (* Invariant *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_9[shift_sint8(i8_0, i_1)] = 1))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_7, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_6, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_5, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_4, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_3, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_2, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a_1, 1).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rw(Malloc_0, a, 1).
+}
+Prove: i <= 2147483646.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (1/9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (2/9):
+Effect at line 45
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (3/9):
+Effect at line 46
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (4/9):
+Effect at line 47
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (5/9):
+Effect at line 48
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (6/9):
+Effect at line 49
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (7/9):
+Effect at line 50
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (8/9):
+Effect at line 51
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/chunk_typing.i, line 40) (9/9):
+Effect at line 52
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/chunk_typing.i, line 44):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/chunk_typing.i, line 44):
+Prove: true.
+
+------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'function':
+  /*@
+     behavior typed:
+     requires \separated(x+(..),
+                \union(i8+(..),u8+(..),i16+(..),u16+(..),i32+(..),u32+(..),
+                  i64+(..),u64+(..)));
+     */
+  void function(signed char * /*[10]*/ i8, unsigned char * /*[10]*/ u8,
+                short * /*[10]*/ i16, unsigned short * /*[10]*/ u16,
+                int * /*[10]*/ i32, unsigned int * /*[10]*/ u32,
+                long long * /*[10]*/ i64, unsigned long long * /*[10]*/ u64);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f066a94e1eb05f0ceb3f905405e624205a997b7a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -0,0 +1,501 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function usable_axiom
+[rte] annotating function usable_lemma
+[wp] 3 goals scheduled
+---------------------------------------------
+--- Context 'typed_usable_lemma' 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_sint32_chunk (m:addr -> int) =
+    forall a:addr. is_sint32 (get m a)
+end
+---------------------------------------------
+--- Context 'typed_usable_lemma' 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
+---------------------------------------------
+--- Context 'typed_usable_lemma' Cluster 'A_Occ' 
+---------------------------------------------
+theory A_Occ
+  (* 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 L_occ (addr -> int) int addr int int : int
+  
+  (* use Chunk *)
+  
+  Q_empty :
+    forall mint:addr -> int, v:int, p:addr, f:int, t:int.
+     t <= f -> is_sint32_chunk mint -> is_sint32 v -> L_occ mint v p f t = 0
+  
+  (* use Compound *)
+  
+  Q_is :
+    forall mint:addr -> int, v:int, p:addr, f:int, t:int.
+     let x = (- 1) + t in
+     let x1 = get mint (shift_sint32 p x) in
+     x1 = v ->
+     f < t ->
+     is_sint32_chunk mint ->
+     is_sint32 v ->
+     is_sint32 x1 -> (1 + L_occ mint v p f x) = L_occ mint v p f t
+  
+  Q_isnt :
+    forall mint:addr -> int, v:int, p:addr, f:int, t:int.
+     let x = (- 1) + t in
+     let x1 = get mint (shift_sint32 p x) in
+     not x1 = v ->
+     f < t ->
+     is_sint32_chunk mint ->
+     is_sint32 v -> is_sint32 x1 -> L_occ mint v p f x = L_occ mint v p f t
+end
+---------------------------------------------
+--- Context 'typed_usable_lemma' 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 *)
+  
+  (* use frama_c_wp.memory.Memory *)
+  
+  (* use Chunk *)
+  
+  (* use A_Occ *)
+  
+  lemma Q_provable_lemma :
+    forall mint:addr -> int, v:int, p:addr, f:int, s:int, t:int.
+     f <= s ->
+     s <= t ->
+     is_sint32_chunk mint ->
+     is_sint32 v ->
+     (L_occ mint v p f s + L_occ mint v p s t) = L_occ mint v p f t
+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 Axiomatic1 *)
+    
+    goal wp_goal :
+      forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int.
+       i3 <= i1 ->
+       i < i3 ->
+       region (base a) <= 0 ->
+       is_sint32_chunk t ->
+       is_uint32 i3 ->
+       is_uint32 i1 ->
+       is_uint32 i ->
+       is_sint32 i2 ->
+       (L_occ t i2 a i i3 + L_occ t i2 a i3 i1) = L_occ t i2 a i i1
+  end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'Chunk' 
+---------------------------------------------
+theory Chunk1
+  (* 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 *)
+  
+  predicate is_sint32_chunk1 (m:addr1 -> int) =
+    forall a:addr1. is_sint321 (get1 m a)
+end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'Compound' 
+---------------------------------------------
+theory Compound1
+  (* 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 *)
+  
+  function shift_sint321 (p:addr1) (k:int) : addr1 = shift1 p k
+end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'A_Occ' 
+---------------------------------------------
+theory A_Occ1
+  (* 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 *)
+  
+  function L_occ1 (addr1 -> int) int addr1 int int : int
+  
+  (* use Chunk1 *)
+  
+  Q_empty1 :
+    forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
+     t <=' f ->
+     is_sint32_chunk1 mint -> is_sint321 v -> L_occ1 mint v p f t = 0
+  
+  (* use Compound1 *)
+  
+  Q_is1 :
+    forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
+     let x = (- 1) +' t in
+     let x1 = get1 mint (shift_sint321 p x) in
+     x1 = v ->
+     f <' t ->
+     is_sint32_chunk1 mint ->
+     is_sint321 v ->
+     is_sint321 x1 -> (1 +' L_occ1 mint v p f x) = L_occ1 mint v p f t
+  
+  Q_isnt1 :
+    forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
+     let x = (- 1) +' t in
+     let x1 = get1 mint (shift_sint321 p x) in
+     not x1 = v ->
+     f <' t ->
+     is_sint32_chunk1 mint ->
+     is_sint321 v ->
+     is_sint321 x1 -> L_occ1 mint v p f x = L_occ1 mint v p f t
+end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'Axiomatic1' 
+---------------------------------------------
+theory Axiomatic11
+  (* 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 Chunk1 *)
+  
+  (* use A_Occ1 *)
+  
+  lemma Q_provable_lemma1 :
+    forall mint:addr1 -> int, v:int, p:addr1, f:int, s:int, t:int.
+     f <=' s ->
+     s <=' t ->
+     is_sint32_chunk1 mint ->
+     is_sint321 v ->
+     (L_occ1 mint v p f s +' L_occ1 mint v p s t) = L_occ1 mint v p f t
+end
+[wp:print-generated] 
+  theory WP1
+    (* 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 Axiomatic11 *)
+    
+    goal wp_goal :
+      forall t:addr1 -> int, a:addr1, i:int, i1:int, i2:int.
+       let x = (- 1) +' i1 in
+       not get1 t (shift_sint321 a x) = i2 ->
+       i <' i1 ->
+       region1 (base1 a) <=' 0 ->
+       i1 <=' 1000 ->
+       is_sint32_chunk1 t ->
+       is_uint321 i1 ->
+       is_uint321 i -> is_sint321 i2 -> L_occ1 t i2 a i x = L_occ1 t i2 a i i1
+  end
+---------------------------------------------
+--- Context 'typed' Cluster 'Chunk' 
+---------------------------------------------
+theory Chunk2
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool2 *)
+  
+  (* use int.Int2 *)
+  
+  (* use int.ComputerDivision2 *)
+  
+  (* use real.RealInfix2 *)
+  
+  (* use frama_c_wp.qed.Qed2 *)
+  
+  (* use map.Map2 *)
+  
+  (* use frama_c_wp.memory.Memory2 *)
+  
+  (* use frama_c_wp.cint.Cint2 *)
+  
+  predicate is_sint32_chunk2 (m:addr2 -> int) =
+    forall a:addr2. is_sint322 (get2 m a)
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'Compound' 
+---------------------------------------------
+theory Compound2
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool2 *)
+  
+  (* use int.Int2 *)
+  
+  (* use int.ComputerDivision2 *)
+  
+  (* use real.RealInfix2 *)
+  
+  (* use frama_c_wp.qed.Qed2 *)
+  
+  (* use map.Map2 *)
+  
+  (* use frama_c_wp.memory.Memory2 *)
+  
+  function shift_sint322 (p:addr2) (k:int) : addr2 = shift2 p k
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'A_Occ' 
+---------------------------------------------
+theory A_Occ2
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool2 *)
+  
+  (* use int.Int2 *)
+  
+  (* use int.ComputerDivision2 *)
+  
+  (* use real.RealInfix2 *)
+  
+  (* use frama_c_wp.qed.Qed2 *)
+  
+  (* use map.Map2 *)
+  
+  (* use frama_c_wp.memory.Memory2 *)
+  
+  function L_occ2 (addr2 -> int) int addr2 int int : int
+  
+  (* use Chunk2 *)
+  
+  Q_empty2 :
+    forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
+     t <='' f ->
+     is_sint32_chunk2 mint -> is_sint322 v -> L_occ2 mint v p f t = 0
+  
+  (* use Compound2 *)
+  
+  Q_is2 :
+    forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
+     let x = (- 1) +'' t in
+     let x1 = get2 mint (shift_sint322 p x) in
+     x1 = v ->
+     f <'' t ->
+     is_sint32_chunk2 mint ->
+     is_sint322 v ->
+     is_sint322 x1 -> (1 +'' L_occ2 mint v p f x) = L_occ2 mint v p f t
+  
+  Q_isnt2 :
+    forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
+     let x = (- 1) +'' t in
+     let x1 = get2 mint (shift_sint322 p x) in
+     not x1 = v ->
+     f <'' t ->
+     is_sint32_chunk2 mint ->
+     is_sint322 v ->
+     is_sint322 x1 -> L_occ2 mint v p f x = L_occ2 mint v p f t
+end
+[wp:print-generated] 
+  theory WP2
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool2 *)
+    
+    (* use int.Int2 *)
+    
+    (* use int.ComputerDivision2 *)
+    
+    (* use real.RealInfix2 *)
+    
+    (* use frama_c_wp.qed.Qed2 *)
+    
+    (* use map.Map2 *)
+    
+    (* use frama_c_wp.memory.Memory2 *)
+    
+    (* use Chunk2 *)
+    
+    (* use A_Occ2 *)
+    
+    goal wp_goal :
+      forall t:addr2 -> int, i:int, a:addr2, i1:int, i2:int, i3:int.
+       i2 <='' i3 ->
+       i1 <='' i2 ->
+       is_sint32_chunk2 t ->
+       is_sint322 i ->
+       (L_occ2 t i a i1 i2 +'' L_occ2 t i a i2 i3) = L_occ2 t i a i1 i3
+  end
+[wp] 3 goals generated
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma provable_lemma:
+Prove: (f_0<=s_0) -> (s_0<=t_0) -> (is_sint32_chunk Mint_0)
+       -> (is_sint32 v_0)
+       -> (((L_occ Mint_0 v_0 p_0 f_0 s_0)+(L_occ Mint_0 v_0 p_0 s_0 t_0))=
+           (L_occ Mint_0 v_0 p_0 f_0 t_0))
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function usable_axiom
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/chunk_typing_usable.i, line 29) in 'usable_axiom':
+Let x = e - 1.
+Assume {
+  Type: is_sint32_chunk(Mint_0) /\ is_uint32(b) /\ is_uint32(e).
+  (* Heap *)
+  Type: region(a.base) <= 0.
+  (* Goal *)
+  When: (Mint_0[shift_sint32(a, x)] != i) /\ is_sint32(i).
+  (* Pre-condition *)
+  Have: (b < e) /\ (e <= 1000).
+}
+Prove: L_occ(Mint_0, i, a, b, x) = L_occ(Mint_0, i, a, b, e).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function usable_lemma
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/chunk_typing_usable.i, line 43) in 'usable_lemma':
+Assume {
+  Type: is_sint32_chunk(Mint_0) /\ is_uint32(b) /\ is_uint32(e) /\
+      is_uint32(s).
+  (* Heap *)
+  Type: region(a.base) <= 0.
+  (* Goal *)
+  When: is_sint32(i).
+  (* Pre-condition *)
+  Have: (b < s) /\ (s <= e).
+}
+Prove: (L_occ(Mint_0, i, a, b, s) + L_occ(Mint_0, i, a, s, e))
+         = L_occ(Mint_0, i, a, b, e).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index e519f55833a656ae85bc1acda6610c6ee0f85398..85d318865a1934c7bb5c8f657a5ea7317cb64852 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -71,19 +71,10 @@ Let a = global(G_tr_35).
 Let a_1 = shift___anonstruct_Point_1(a, 2).
 Let a_2 = shift___anonstruct_Point_1(a, 1).
 Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
 Let m = Array1_S1(a, 3, Mint_0).
 Assume {
   Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
   (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 3)] = 8.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -105,19 +96,10 @@ Let a = global(G_tr_35).
 Let a_1 = shift___anonstruct_Point_1(a, 2).
 Let a_2 = shift___anonstruct_Point_1(a, 1).
 Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
 Let m = Array1_S1(a, 3, Mint_0).
 Assume {
   Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
   (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 3)] = 8.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -139,19 +121,10 @@ Let a = global(G_tr_35).
 Let a_1 = shift___anonstruct_Point_1(a, 2).
 Let a_2 = shift___anonstruct_Point_1(a, 1).
 Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
 Let m = Array1_S1(a_3, 3, Mint_0).
 Assume {
   Type: IsArray1S1(Array1_S1(a, 3, Mint_0)) /\ IsArray1S1(m).
   (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 3)] = 8.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -220,37 +193,21 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:55: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast to struct (Buint) from (unsigned int) not implemented yet
-Let a = global(G_tr_35).
-Let a_1 = shift___anonstruct_Point_1(a, 2).
-Let a_2 = shift___anonstruct_Point_1(a, 1).
-Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_41).
-Let a_5 = shiftfield_F4_bytes(a_4).
-Let a_6 = Load_S4(a_4, Mint_0).
+Let a = global(G_buint_41).
+Let a_1 = shiftfield_F4_bytes(a).
+Let a_2 = Load_S4(a, Mint_0).
 Assume {
-  Type: IsS4(a_6).
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 3)] = 8.
-  (* Initializer *)
-  Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
+  Type: IsS4(a_2).
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
+  Init: Mint_0[shift_uint8(a_1, 0)] = 1.
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_x(a_2)] = 20.
+  Init: Mint_0[shift_uint8(a_1, 1)] = 2.
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_y(a_2)] = 21.
+  Init: Mint_0[shift_uint8(a_1, 2)] = 4.
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_x(a_1)] = 30.
-  (* Initializer *)
-  Init: Mint_0[shiftfield_F1_y(a_1)] = 31.
+  Init: Mint_0[shift_uint8(a_1, 3)] = 8.
 }
-Prove: EqS4(a_6, w).
+Prove: EqS4(a_2, w).
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..89b1b1b5b973e603935151a80fee6115eeaa1b79
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -0,0 +1,63 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function function
+[wp] 39 goals scheduled
+[wp] [Alt-Ergo] Goal typed_function_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_2_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_2_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_3_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_3_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_4_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_4_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_5_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_5_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_6_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_6_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_7_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_7_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_8_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_8_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_loop_invariant_9_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_9_established : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_2 : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_3 : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_4 : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_5 : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_6 : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_7 : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_8 : Valid
+[wp] [Alt-Ergo] Goal typed_function_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part4 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part5 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part6 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part7 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part8 : Valid
+[wp] [Qed] Goal typed_function_loop_assigns_part9 : Valid
+[wp] [Qed] Goal typed_function_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_function_loop_variant_positive : Valid
+[wp] Proved goals:   39 / 39
+  Qed:            20 
+  Alt-Ergo:       19
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  function                 20       19       39       100%
+------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'function':
+  /*@
+     behavior typed:
+     requires \separated(x+(..),
+                \union(i8+(..),u8+(..),i16+(..),u16+(..),i32+(..),u32+(..),
+                  i64+(..),u64+(..)));
+     */
+  void function(signed char * /*[10]*/ i8, unsigned char * /*[10]*/ u8,
+                short * /*[10]*/ i16, unsigned short * /*[10]*/ u16,
+                int * /*[10]*/ i32, unsigned int * /*[10]*/ u32,
+                long long * /*[10]*/ i64, unsigned long long * /*[10]*/ u64);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c503421c8a958092c2d9bd7e08643dac8c075331
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
@@ -0,0 +1,24 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function usable_axiom
+[rte] annotating function usable_lemma
+[wp] Warning: native support for coq is deprecated, use tip instead
+[wp] 3 goals scheduled
+[wp] [Coq] Goal typed_lemma_provable_lemma : Saved script
+[wp] [Coq (native)] Goal typed_lemma_provable_lemma : Valid
+[wp] [Alt-Ergo] Goal typed_usable_axiom_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_usable_lemma_ensures : Valid
+[wp] Proved goals:    3 / 3
+  Qed:             0 
+  Coq (native):    1 
+  Alt-Ergo:        2  (unsuccess: 1)
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        -        1       100%
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  usable_axiom              -        1        1       100%
+  usable_lemma              -        1        1       100%
+------------------------------------------------------------