diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index ecb9b6a606fd0a6d4d6bca9af09be4b5f8057e6d..46942381492b89e23c8e684a97e9003fd9e9790c 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -815,250 +815,360 @@ let c_int_bounds_ival f  =
 
 let max_reduce_quantifiers = 1000
 
-(** We know that t is a predicate which is the opened body of a forall *)
-let reduce_bound v tv dom t : term =
-  let module Exc = struct
-    exception True
-    exception False
-    exception Unknown of Integer.t
-  end in
-  try
-    let red i () =
-      match repr (QED.e_subst_var v (e_zint i) t) with
-      | True -> ()
-      | False -> raise Exc.False
-      | _ -> raise (Exc.Unknown i) in
-    let min_bound = try
-        Ival.fold_int red dom (); raise Exc.True
-      with Exc.Unknown i -> i in
-    let max_bound = try
-        Ival.fold_int_decrease red dom (); raise Exc.True
-      with Exc.Unknown i -> i in
-    (** we try to reduce the bounds of the domains, when trivially false *)
-    let dom_red = Ival.inject_range (Some min_bound) (Some max_bound) in
-    assert ( Ival.is_included dom_red dom);
-    if Ival.equal dom_red dom
-    then t
-    else
-      (e_imply [e_leq (e_zint min_bound) tv;
-                e_leq tv (e_zint max_bound)]
-         t)
-  with
-  | Exc.True -> e_true
-  | Exc.False -> e_false
-
-module Polarity = struct
-  type t = Pos | Neg | Both
-  let flip = function | Pos -> Neg | Neg -> Pos | Both -> Both
-  let from_bool = function | false -> Neg | true -> Pos
-end
-
-let is_cint_simplifier = object (self)
+module Dom = struct
+  type t = Ival.t Tmap.t
+  let is_top_ival = Ival.equal Ival.top
 
-  val mutable domain : Ival.t Tmap.t = Tmap.empty
+  let top = Tmap.empty
 
-  method private print fmt =
+  let print fmt dom =
     Tmap.iter (fun k v ->
         Format.fprintf fmt "%a: %a,@ " Lang.F.pp_term k Ival.pretty v)
-      domain
-
-  method name = "Remove redundant is_cint"
-  method copy = {< domain = domain >}
-
-  method private narrow_dom t v =
-    domain <-
-      Tmap.change (fun _ p ->
-          function
-          | None -> Some p
-          | Some old -> Some (Ival.narrow p old))
-        t v domain
-
-  method assume p =
-    let rec aux t =
-      match Lang.F.repr t with
-      | _ when not (is_prop t) -> ()
-      | Fun(g,[a]) ->
-          begin try
-              let ubound = c_int_bounds_ival (is_cint g) in
-              self#narrow_dom a ubound
-            with Not_found -> ()
+      dom
+
+  let find t dom = Tmap.find t dom
+
+  let get t dom = try find t dom with Not_found -> Ival.top
+
+  let narrow t v dom =
+    if Ival.is_bottom v then raise Lang.Contradiction
+    else if is_top_ival v then dom
+    else Tmap.change (fun _ v old ->
+        match old with | None -> Some v
+                       | (Some old) as old' ->
+                           let v = Ival.narrow v old in
+                           if Ival.is_bottom v then raise Lang.Contradiction;
+                           if Ival.equal v old then old'
+                           else Some v) t v dom
+
+  let add t v dom =
+    if Ival.is_bottom v then raise Lang.Contradiction;
+    if is_top_ival v then dom else Tmap.add t v dom
+
+  let remove t dom = Tmap.remove t dom
+
+  let assume_cmp =
+    let module Local = struct
+      type t = Integer of Ival.t | Term of Ival.t option
+    end in fun cmp t1 t2 dom ->
+      let encode t = match Lang.F.repr t with
+        | Kint z -> Local.Integer (Ival.inject_singleton z)
+        | _ -> Local.Term (try Some (Tmap.find t dom) with Not_found -> None)
+      in
+      let term_dom = function
+        | Some v -> v
+        | None -> Ival.top
+      in
+      match encode t1, encode t2 with
+      | Local.Integer cst1, Local.Integer cst2 -> (* assume cmp cst1 cst2 *)
+          if Abstract_interp.Comp.False = Ival.forward_comp_int cmp cst1 cst2
+          then raise Lang.Contradiction;
+          dom
+      | Local.Term None, Local.Term None ->
+          dom (* nothing can be collected *)
+      | Local.Term opt1, Local.Integer cst2 ->
+          let v1 = term_dom opt1 in
+          add t1 (Ival.backward_comp_int_left cmp v1 cst2) dom
+      | Local.Integer cst1, Local.Term opt2 ->
+          let v2 = term_dom opt2 in
+          let cmp_sym = Abstract_interp.Comp.sym cmp in
+          add t2 (Ival.backward_comp_int_left cmp_sym v2 cst1) dom
+      | Local.Term opt1, Local.Term opt2 ->
+          let v1 = term_dom opt1 in
+          let v2 = term_dom opt2 in
+          let cmp_sym = Abstract_interp.Comp.sym cmp in
+          add t1 (Ival.backward_comp_int_left cmp v1 v2)
+            (add t2 (Ival.backward_comp_int_left cmp_sym v2 v1) dom)
+
+  let assume_literal t dom = match Lang.F.repr t with
+    | Eq(a,b) -> assume_cmp Abstract_interp.Comp.Eq a b dom
+    | Leq(a,b) -> assume_cmp Abstract_interp.Comp.Le a b dom
+    | Lt(a,b) -> assume_cmp Abstract_interp.Comp.Lt a b dom
+    | Fun(g,[a]) -> begin try
+          let ubound =
+            c_int_bounds_ival (is_cint g) (* may raise Not_found *) in
+          narrow a ubound dom
+        with Not_found -> dom
+      end
+    | Not p -> begin match Lang.F.repr p with
+        | Fun(g,[a]) -> begin try (* just checks for a contraction *)
+              let ubound =
+                c_int_bounds_ival (is_cint g) (* may raise Not_found *) in
+              let v = find a dom (* may raise Not_found *) in
+              if Ival.is_included v ubound then raise Lang.Contradiction;
+              dom
+            with Not_found -> dom
           end
-      | And _ -> Lang.F.QED.f_iter aux t
-      | _ -> ()
-    in
-    aux (Lang.F.e_prop p)
-
-  method target _ = ()
-  method fixpoint = ()
-
-  method private simplify ~is_goal p =
-    let pool = Lang.get_pool () in
+        | _ -> dom
+      end
+    | _ -> dom
+end
 
-    let reduce op var_domain base =
-      let dom =
-        match Lang.F.repr base with
-        | Kint z -> Ival.inject_singleton z
-        | _ ->
-            try Tmap.find base domain
-            with Not_found -> Ival.top
-      in
-      var_domain := Ival.backward_comp_int_left op !var_domain dom
-    in
-    let rec reduce_on_neg var var_domain t =
-      match Lang.F.repr t with
-      | _ when not (is_prop t) -> ()
-      | Leq(a,b) when Lang.F.equal a var ->
-          reduce Abstract_interp.Comp.Le var_domain b
-      | Leq(b,a) when Lang.F.equal a var ->
-          reduce Abstract_interp.Comp.Ge var_domain b
-      | Lt(a,b) when Lang.F.equal a var ->
-          reduce Abstract_interp.Comp.Lt var_domain b
-      | Lt(b,a) when Lang.F.equal a var ->
-          reduce Abstract_interp.Comp.Gt var_domain b
-      | And l -> List.iter (reduce_on_neg var var_domain) l
-      | _ -> ()
+let is_cint_simplifier =
+  let reduce_bound ~add_bonus quant v tv dom t : term =
+    (** Returns [new_t] such that [c_bind quant (alpha,t)]
+                           equals [c_bind quant v (alpha,new_t)]
+        under the knowledge that  [(not t) ==> (var in dom)].
+        Note: [~add_bonus] has not effect on the correctness of the transformation.
+          It is a parameter that can be used in order to get better results.
+        Bonus: Add additionnal hypothesis when we could deduce better constraint
+        on the variable *)
+    let module Tool = struct
+      exception Stop
+      exception Empty
+      exception Unknown of Integer.t
+      type t = { when_empty: unit -> term;
+                 add_hyp: term list -> term -> term;
+                 when_true: bool ref -> unit;
+                 when_false: bool ref -> unit;
+                 when_stop: unit -> term;
+               }
+    end in
+    let tools = Tool.(match quant with
+        | Forall -> { when_empty=(fun () -> e_true);
+                      add_hyp =(fun hyps t -> e_imply hyps t);
+                      when_true=(fun bonus -> bonus := add_bonus);
+                      when_false=(fun _ -> raise Stop);
+                      when_stop=(fun () -> e_false);
+                    }
+        | Exists  ->{ when_empty= (fun () -> e_false);
+                      add_hyp =(fun hyps t -> e_and (t::hyps));
+                      when_true=(fun _ -> raise Stop);
+                      when_false=(fun bonus -> bonus := add_bonus);
+                      when_stop=(fun () -> e_true);
+                    }
+        | _ -> assert false)
     in
-    let reduce_on_pos var var_domain t =
-      match Lang.F.repr t with
-      | Imply (l,_) -> List.iter (reduce_on_neg var var_domain) l
-      | _ -> ()
-    in
-    let rec walk ~term_pol t =
-      let walk_flip_pol t = walk ~term_pol:(Polarity.flip term_pol) t
-      and walk_same_pol t = walk ~term_pol t
-      and walk_both_pol t = walk ~term_pol:Polarity.Both t
-      in
-      match repr t with
-      | _ when not (is_prop t) -> t
-      | Bind((Forall|Exists),_,_) ->
-          let ctx,t = e_open ~pool ~lambda:false t in
-          let ctx_with_dom =
-            List.map (fun ((quant,var) as qv)  -> match tau_of_var var with
-                | Int ->
-                    let tvar = (e_var var) in
-                    let var_domain = ref Ival.top in
-                    if quant = Forall
-                    then reduce_on_pos tvar var_domain t
-                    else reduce_on_neg tvar var_domain t;
-                    domain <- Tmap.add tvar !var_domain domain;
-                    qv, Some (tvar, var_domain)
-                | _ -> qv, None) ctx
-          in
-          let t = walk_same_pol t in
-          let f_close t = function
-            | (quant,var), None -> e_bind quant var t
-            | (quant,var), Some (tvar,var_domain) ->
-                domain <- Tmap.remove tvar domain;
-                (** Bonus: Add additionnal hypothesis in forall when we could deduce
-                    better constraint on the variable *)
-                let t = if quant = Forall &&
-                           term_pol = Polarity.Pos &&
-                           Ival.cardinal_is_less_than !var_domain max_reduce_quantifiers
-                  then reduce_bound var tvar !var_domain t
-                  else t in
-                e_bind quant var t
-          in
-          List.fold_left f_close t ctx_with_dom
-      | Fun(g,[a]) ->
-          (** Here we simplifies the cints which are redoundant *)
-          begin try
-              let ubound = c_int_bounds_ival (is_cint g) in
-              let dom = (Tmap.find a domain) in
-              if Ival.is_included dom ubound
-              then e_true
+    if Vars.mem v (vars t) then try
+        let bonus_min = ref false in
+        let bonus_max = ref false in
+        let dom = if Ival.cardinal_is_less_than dom max_reduce_quantifiers then
+            (* try to reduce the domain when [var] is still in [t] *)
+            let red reduced i () =
+              match repr (QED.e_subst_var v (e_zint i) t) with
+              | True -> tools.Tool.when_true reduced
+              | False -> tools.Tool.when_false reduced
+              | _ -> raise (Tool.Unknown i) in
+            let min_bound = try Ival.fold_int (red bonus_min) dom ();
+                raise Tool.Empty with Tool.Unknown i -> i in
+            let max_bound = try Ival.fold_int_decrease (red bonus_max) dom ();
+                raise Tool.Empty with Tool.Unknown i -> i in
+            let red_dom = Ival.inject_range (Some min_bound) (Some max_bound) in
+            Ival.narrow dom red_dom
+          else dom
+        in begin match Ival.min_and_max dom with
+          | None, None -> t (* Cannot be reduced *)
+          | Some min, None -> (* May be reduced to [min ...] *)
+              if !bonus_min then tools.Tool.add_hyp [e_leq (e_zint min) tv] t
               else t
-            with Not_found -> t
-          end
-      | Imply (l1,l2) -> e_imply (List.map walk_flip_pol l1) (walk_same_pol l2)
-      | Not p -> e_not (walk_flip_pol p)
-      | And _ | Or _ -> Lang.F.QED.f_map walk_same_pol t
-      | _ ->
-          Lang.F.QED.f_map ~pool ~forall:false ~exists:false walk_both_pol t in
-    Lang.F.p_bool (walk ~term_pol:(Polarity.from_bool is_goal) (Lang.F.e_prop p))
+          | None, Some max -> (* May be reduced to [... max] *)
+              if !bonus_max then tools.Tool.add_hyp [e_leq tv (e_zint max)] t
+              else t
+          | Some min, Some max ->
+              if Integer.equal min max then (* Reduced to only one value: [min] *)
+                QED.e_subst_var v (e_zint min) t
+              else if Integer.lt min max then
+                let h = if !bonus_min then [e_leq (e_zint min) tv] else []
+                in
+                let h = if !bonus_max then (e_leq tv (e_zint max))::h else h
+                in tools.Tool.add_hyp h t
+              else assert false (* Abstract_interp.Error_Bottom raised *)
+        end
+      with
+      | Tool.Stop  -> tools.Tool.when_stop ()
+      | Tool.Empty -> tools.Tool.when_empty ()
+      | Abstract_interp.Error_Bottom -> tools.Tool.when_empty ()
+      | Abstract_interp.Error_Top -> t
+    else (* [alpha] is no more in [t] *)
+    if Ival.is_bottom dom then tools.Tool.when_empty () else t
+  in
+  let module Polarity = struct
+    type t = Pos | Neg | Both
+    let flip = function | Pos -> Neg | Neg -> Pos | Both -> Both
+    let from_bool = function | false -> Neg | true -> Pos
+  end
+  in object (self)
 
-  method simplify_exp (e : term) = e
+    val mutable domain : Dom.t = Dom.top
 
-  method simplify_hyp p = self#simplify ~is_goal:false p
+    method name = "Remove redundant is_cint"
+    method copy = {< domain = domain >}
 
-  method simplify_goal p = self#simplify ~is_goal:true p
+    method target _ = ()
+    method fixpoint = ()
 
-  method simplify_branch p = p
+    method assume p =
+      Lang.iter_consequence_literals
+        (fun p -> domain <- Dom.assume_literal p domain) (Lang.F.e_prop p)
+
+    method private simplify ~is_goal p =
+      let pool = Lang.get_pool () in
+
+      let reduce op var_domain base =
+        let dom =
+          match Lang.F.repr base with
+          | Kint z -> Ival.inject_singleton z
+          | _ ->
+              try Tmap.find base domain
+              with Not_found -> Ival.top
+        in
+        var_domain := Ival.backward_comp_int_left op !var_domain dom
+      in
+      let rec reduce_on_neg var var_domain t =
+        match Lang.F.repr t with
+        | _ when not (is_prop t) -> ()
+        | Leq(a,b) when Lang.F.equal a var ->
+            reduce Abstract_interp.Comp.Le var_domain b
+        | Leq(b,a) when Lang.F.equal a var ->
+            reduce Abstract_interp.Comp.Ge var_domain b
+        | Lt(a,b) when Lang.F.equal a var ->
+            reduce Abstract_interp.Comp.Lt var_domain b
+        | Lt(b,a) when Lang.F.equal a var ->
+            reduce Abstract_interp.Comp.Gt var_domain b
+        | And l -> List.iter (reduce_on_neg var var_domain) l
+        | Not p -> reduce_on_pos var var_domain p
+        | _ -> ()
+      and reduce_on_pos var var_domain t =
+        match Lang.F.repr t with
+        | Neq _ | Leq _ | Lt _ -> reduce_on_neg var var_domain (e_not t)
+        | Imply (l,p) -> List.iter (reduce_on_neg var var_domain) l;
+            reduce_on_pos var var_domain p
+        | Or l -> List.iter (reduce_on_pos var var_domain) l;
+        | Not p -> reduce_on_neg var var_domain p
+        | _ -> ()
+      in
+      (* [~term_pol] gives the polarity of the term [t] from the top level.
+                     That informs about how should be considered the quantifiers
+                     of [t]
+      *)
+      let rec walk ~term_pol t =
+        let walk_flip_pol t = walk ~term_pol:(Polarity.flip term_pol) t
+        and walk_same_pol t = walk ~term_pol t
+        and walk_both_pol t = walk ~term_pol:Polarity.Both t
+        in
+        match repr t with
+        | _ when not (is_prop t) -> t
+        | Bind((Forall|Exists),_,_) ->
+            let ctx,t = e_open ~pool ~lambda:false t in
+            let ctx_with_dom =
+              List.map (fun ((quant,var) as qv)  -> match tau_of_var var with
+                  | Int ->
+                      let tvar = (e_var var) in
+                      let var_domain = ref Ival.top in
+                      if quant = Forall
+                      then reduce_on_pos tvar var_domain t
+                      else reduce_on_neg tvar var_domain t;
+                      domain <- Dom.add tvar !var_domain domain;
+                      qv, Some (tvar, var_domain)
+                  | _ -> qv, None) ctx
+            in
+            let t = walk_same_pol t in
+            let f_close t = function
+              | (quant,var), None -> e_bind quant var t
+              | (quant,var), Some (tvar,var_domain) ->
+                  domain <- Dom.remove tvar domain;
+                  (** Bonus: Add additionnal hypothesis in forall when we could deduce
+                      better constraint on the variable *)
+                  let add_bonus = match term_pol with
+                    | Polarity.Both -> false
+                    | _ -> (term_pol=Polarity.Pos) = (quant=Forall)
+                  in
+                  let t = reduce_bound ~add_bonus quant var tvar !var_domain t in
+                  e_bind quant var t
+            in
+            List.fold_left f_close t ctx_with_dom
+        | Fun(g,[a]) ->
+            (** Here we simplifies the cints which are redoundant *)
+            begin try
+                let ubound = c_int_bounds_ival (is_cint g) in
+                let dom = (Tmap.find a domain) in
+                if Ival.is_included dom ubound
+                then e_true
+                else t
+              with Not_found -> t
+            end
+        | Imply (l1,l2) -> e_imply (List.map walk_flip_pol l1) (walk_same_pol l2)
+        | Not p -> e_not (walk_flip_pol p)
+        | And _ | Or _ -> Lang.F.QED.f_map walk_same_pol t
+        | _ ->
+            Lang.F.QED.f_map ~pool ~forall:false ~exists:false walk_both_pol t in
+      Lang.F.p_bool (walk ~term_pol:(Polarity.from_bool is_goal) (Lang.F.e_prop p))
 
-  method infer = []
-end
+    method simplify_exp (e : term) = e
 
+    method simplify_hyp p = self#simplify ~is_goal:false p
 
-let mask_simplifier =
-  object(self)
+    method simplify_goal p = self#simplify ~is_goal:true p
 
-    (** Must be 2^n-1 *)
-    val mutable magnitude : Integer.t Tmap.t = Tmap.empty
+    method simplify_branch p = p
 
-    method name = "Rewrite unsigned masks"
-    method copy = {< magnitude = magnitude >}
+    method infer = []
+  end
 
-    method private update x m =
-      let better =
-        try Integer.lt m (Tmap.find x magnitude)
-        with Not_found -> true in
-      if better then magnitude <- Tmap.add x m magnitude
 
-    method private collect d x =
-      try
-        let m = Tmap.find x magnitude in
+let mask_simplifier =
+  let update x m ctx =
+    Tmap.insert (fun _ m old -> if Integer.lt m old then (*better*) m else old)
+      x m ctx
+  and rewrite ctx e =
+    let reduce m x = match F.repr x with
+      | Kint v -> F.e_zint (Integer.logand m v)
+      | _ -> x
+    and collect ctx d x = try
+        let m = Tmap.find x ctx in
         match d with
         | None -> Some m
         | Some m0 -> if Integer.lt m m0 then Some m else d
       with Not_found -> d
+    in
+    match F.repr e with
+    | Fun(f,es) when f == f_land ->
+        begin
+          match List.fold_left (collect ctx) None es with
+          | None -> raise Not_found
+          | Some m -> F.e_fun f_land (List.map (reduce m) es)
+        end
+    | _ -> raise Not_found
+  in
+  object
 
-    method private reduce m x =
-      match F.repr x with
-      | Kint v -> F.e_zint (Integer.logand m v)
-      | _ -> x
+    (** Must be 2^n-1 *)
+    val mutable magnitude : Integer.t Tmap.t = Tmap.empty
 
-    method private rewrite e =
-      match F.repr e with
-      | Fun(f,es) when f == f_land ->
-          begin
-            match List.fold_left self#collect None es with
-            | None -> raise Not_found
-            | Some m -> F.e_fun f_land (List.map (self#reduce m) es)
-          end
-      | _ -> raise Not_found
+    method name = "Rewrite unsigned masks"
+    method copy = {< magnitude = magnitude >}
 
     method target _ = ()
     method infer = []
     method fixpoint = ()
 
     method assume p =
-      let rec walk e = match F.repr e with
-        | And es -> List.iter walk es
-        | Fun(f,[x]) ->
-            begin
-              try
-                let iota = is_cint f in
-                if not (Ctypes.signed iota) then
-                  self#update x (snd (Ctypes.bounds iota))
-              with Not_found -> ()
-            end
-        | _ -> ()
-      in walk (F.e_prop p)
+      Lang.iter_consequence_literals
+        (fun p -> match F.repr p with
+           | Fun(f,[x]) -> begin
+               try
+                 let iota = is_cint f in
+                 if not (Ctypes.signed iota) then
+                   magnitude <- update x (snd (Ctypes.bounds iota)) magnitude
+               with Not_found -> ()
+             end
+           | _ -> ()) (F.e_prop p)
 
     method simplify_exp e =
       if Tmap.is_empty magnitude then e else
-        Lang.e_subst self#rewrite e
+        Lang.e_subst (rewrite magnitude) e
 
     method simplify_hyp p =
       if Tmap.is_empty magnitude then p else
-        Lang.p_subst self#rewrite p
+        Lang.p_subst (rewrite magnitude) p
 
     method simplify_branch p =
       if Tmap.is_empty magnitude then p else
-        Lang.p_subst self#rewrite p
+        Lang.p_subst (rewrite magnitude) p
 
     method simplify_goal p =
       if Tmap.is_empty magnitude then p else
-        Lang.p_subst self#rewrite p
+        Lang.p_subst (rewrite magnitude) p
 
   end
 
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index bad92bae2ea0d94393c1868ba127e094d50873b9..f203b8b5cd7187ce016ee7d3f3319ce68ac0e703 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1033,15 +1033,15 @@ struct
         s.cache <- None ;
       end
 
-  let rec assume s p = match F.repr p with
-    | Logic.And ps -> List.iter (assume s) ps
-    | Logic.Eq(a,b) ->
-        if is_cst s a then set_def s p b a ;
-        if is_cst s b then set_def s p a b ;
-    | _ -> ()
+  let collect_set_def s p = Lang.iter_consequence_literals
+      (fun literal -> match Lang.F.repr literal with
+         | Logic.Eq(a,b) ->
+             if is_cst s a then set_def s literal b a ;
+             if is_cst s b then set_def s literal a b ;
+         | _ -> ()) p
 
   let collect s = function
-    | Have p | When p | Core p | Init p -> assume s (F.e_prop p)
+    | Have p | When p | Core p | Init p -> collect_set_def s (F.e_prop p)
     | Type _ | Branch _ | Either _ | State _ -> ()
 
   let subst s =
@@ -1544,8 +1544,7 @@ struct
   let rec collect_step w s =
     match s.condition with
     | Type _ | State _ -> w
-    | Have p | Core p | Init p | When p ->
-        usage w (F.e_prop p)
+    | Have p | Core p | Init p | When p -> usage w (F.e_prop p)
     | Branch(p,a,b) ->
         let wa = collect_seq w a in
         let wb = collect_seq w b in
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 1f2ecea227a8d5771411009634b05f861e16ddf6..2aadf4d38531ee393e2b069d00379e7021abee97 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -987,4 +987,28 @@ class type simplifier =
     method simplify_goal : F.pred -> F.pred
   end
 
+let is_atomic_pred = function
+  | Neq _ | Eq _ | Leq _ | Lt _ | Fun _ -> true
+  | _ -> false
+let is_literal p = match repr p with
+  | Not p -> is_atomic_pred (repr p)
+  | _ ->  is_atomic_pred (repr p)
+
+let iter_consequence_literals f_literal p =
+  let f_literal = (fun p -> if QED.lc_closed p then f_literal p else ()) in
+  let rec aux_pos p = match repr p with
+    | And ps -> List.iter aux_pos ps
+    | Not p ->  aux_neg p
+    | Bind((Forall|Exists),_,a) -> aux_pos (QED.lc_repr a)
+    | rep when is_atomic_pred rep -> f_literal p
+    | _ -> ()
+  and aux_neg p = match repr p with
+    | Imply (hs,p) -> List.iter aux_pos hs ; aux_neg p
+    | Or ps -> List.iter aux_neg ps
+    | Not p -> aux_pos p
+    | Bind((Forall|Exists),_,a) -> aux_neg (QED.lc_repr a)
+    | rep when is_atomic_pred rep -> f_literal (e_not p)
+    | _ -> ()
+  in aux_pos p
+
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index ee4a6dade82b253a7bfbfb82cf5bd26927b89d52..a2a045de99f62845d9ceb8262b98a2d5c9f5dc5a 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -555,6 +555,13 @@ val p_subst : (term -> term) -> pred -> pred (** uses current pool *)
 
 exception Contradiction
 
+val is_literal: F.term -> bool
+val iter_consequence_literals: (F.term -> unit) -> F.term -> unit
+(** [iter_consequence_literals assume_from_litteral hypothesis] applies
+    the function [assume_from_litteral] on literals that are a consequence of the [hypothesis]
+    (i.e. in the hypothesis [not (A && (B || C) ==> D)], only [A] and [not D] are
+    considered as consequence literals). *)
+
 class type simplifier =
   object
     method name : string
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
index 62b6128cf6bfe19b8f5b8e5cb995fb5e915b1c9e..115de5d9648a90244d293e05cf3fe13140cb66c5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
@@ -3,6 +3,199 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function check_acsl
+------------------------------------------------------------
+
+Goal Check 'ko,A1,absorb_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 62):
+Prove: exists i : Z. forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 63) ->
+    P_P(i_1, i, 1.0))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,A2,absorb_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 63):
+Prove: exists i : Z. forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 63) ->
+    (P_P(i, i_1, 1.0) -> P_P(i_1, i, 1.0)))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,A3,absorb_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 64):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((0 <= i_1) -> ((i_1 <= 63) -> P_P(i_1, i, r))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,A4,absorb_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 65):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((0 <= i_1) -> ((i_1 <= 63) -> (P_P(i, i_1, r) ->
+     P_P(i_1, i, r)))))).
+
+------------------------------------------------------------
+
+Goal Check 'ok,C1,absurd_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 67):
+Prove: exists i : Z. forall i_1 : Z. ((i_1 < 0) -> (((-900000) <= i_1) ->
+    (is_uint8(i_1) -> (P_P(i, i_1, 1.0) -> P_P(i_1, i, 1.0))))).
+
+------------------------------------------------------------
+
+Goal Check 'ok,C2,absurd_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 68):
+Prove: exists i : Z. forall i_1 : Z. ((i_1 < 0) -> (((-900000) <= i_1) ->
+    (is_uint8(i_1) -> (P_P(i, i_1, 1.0) -> P_P(i_1, i, 1.0))))).
+
+------------------------------------------------------------
+
+Goal Check 'lack,C3,absurd_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 69):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((i_1 < 0) -> (((-900000) <= i_1) -> (P_P(i, i_1, r) ->
+     P_P(i_1, i, r)))))).
+
+------------------------------------------------------------
+
+Goal Check 'lack,C4,absurd_is_cint' (file tests/wp_acsl/simpl_is_type.i, line 70):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((i_1 < 0) -> (((-900000) <= i_1) -> (P_P(i, i_1, r) ->
+     P_P(i_1, i, r)))))).
+
+------------------------------------------------------------
+
+Goal Check 'ok,C5,absurd_cmp' (file tests/wp_acsl/simpl_is_type.i, line 71):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'ko,B5,no_absurd_cmp' (file tests/wp_acsl/simpl_is_type.i, line 72):
+Assume { (* Goal *) When: (.0 < r) /\ (r < 1.0). }
+Prove: P_P(3, 5, 1.0).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Min1,reduces_min' (file tests/wp_acsl/simpl_is_type.i, line 74):
+Prove: exists i : Z. forall i_1 : Z. ((0 <= i_1) -> (((-5) <= i_1) ->
+    ((i_1 <= 99) -> P_P(i_1, i, 1.0)))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Min2,reduces_min' (file tests/wp_acsl/simpl_is_type.i, line 75):
+Prove: exists i : Z. forall i_1 : Z. ((10 <= i_1) -> ((11 <= i_1) ->
+    ((i_1 <= 99) -> (P_P(10, i, 1.0) -> P_P(i_1, i, 1.0))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Min3,reduces_min' (file tests/wp_acsl/simpl_is_type.i, line 76):
+Prove: exists i : Z. forall i_1 : Z. ((10 <= i_1) -> ((12 <= i_1) ->
+    ((i_1 <= 99) -> (P_P(10, i, 1.0) -> (P_P(11, i, 1.0) ->
+    (P_P(13, i, 1.0) -> P_P(i_1, i, 1.0))))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Min4,reduces_min' (file tests/wp_acsl/simpl_is_type.i, line 77):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. (((-5) <= i_1) -> ((i_1 <= 99) -> P_P(i_1, i, r))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Min5,reduces_min' (file tests/wp_acsl/simpl_is_type.i, line 78):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((10 <= i_1) -> ((i_1 <= 99) -> (P_P(10, i, r) ->
+     P_P(i_1, i, r)))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Min6,reduces_min' (file tests/wp_acsl/simpl_is_type.i, line 79):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((10 <= i_1) -> ((i_1 <= 99) -> (P_P(10, i, r) ->
+     (P_P(11, i, r) -> (P_P(13, i, r) -> P_P(i_1, i, r)))))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Max1,reduces_max' (file tests/wp_acsl/simpl_is_type.i, line 81):
+Prove: exists i : Z. forall i_1 : Z. ((10 <= i_1) -> ((i_1 <= 255) ->
+    ((i_1 <= 599) -> P_P(i_1, i, 1.0)))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Max2,reduces_max' (file tests/wp_acsl/simpl_is_type.i, line 82):
+Prove: exists i : Z. forall i_1 : Z. ((10 <= i_1) -> ((i_1 <= 97) ->
+    ((i_1 <= 99) -> (P_P(98, i, 1.0) -> (P_P(99, i, 1.0) ->
+    P_P(i_1, i, 1.0)))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Max3,reduces_max' (file tests/wp_acsl/simpl_is_type.i, line 83):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((10 <= i_1) -> ((i_1 <= 599) -> P_P(i_1, i, r))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Max4,reduces_max' (file tests/wp_acsl/simpl_is_type.i, line 84):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((10 <= i_1) -> ((i_1 <= 99) -> (P_P(98, i, r) ->
+     (P_P(99, i, r) -> P_P(i_1, i, r))))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,MinMax1,reduce_minmax' (file tests/wp_acsl/simpl_is_type.i, line 86):
+Prove: exists i : Z. forall i_1 : Z. ((0 <= i_1) -> (((-5) <= i_1) ->
+    ((i_1 <= 97) -> ((i_1 <= 99) -> (P_P(98, i, 1.0) -> (P_P(99, i, 1.0) ->
+    P_P(i_1, i, 1.0))))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,MinMax2,reduce_minmax' (file tests/wp_acsl/simpl_is_type.i, line 87):
+Prove: exists i : Z. forall i_1 : Z. ((10 <= i_1) -> ((12 <= i_1) ->
+    ((i_1 <= 97) -> ((i_1 <= 99) -> (P_P(10, i, 1.0) -> (P_P(11, i, 1.0) ->
+    (P_P(13, i, 1.0) -> (P_P(98, i, 1.0) -> (P_P(99, i, 1.0) ->
+    P_P(i_1, i, 1.0)))))))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,MinMax3,reduce_minmax' (file tests/wp_acsl/simpl_is_type.i, line 88):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. (((-5) <= i_1) -> ((i_1 <= 99) -> (P_P(98, i, r) ->
+     (P_P(99, i, r) -> P_P(i_1, i, r))))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,MinMax4,reduce_minmax' (file tests/wp_acsl/simpl_is_type.i, line 89):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((10 <= i_1) -> ((i_1 <= 99) -> (P_P(10, i, r) ->
+     (P_P(11, i, r) -> (P_P(13, i, r) -> (P_P(98, i, r) -> (P_P(99, i, r) ->
+     P_P(i_1, i, r)))))))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Let1,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 92):
+Prove: exists i : Z. P_P(10, i, 1.0).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Let2,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 93):
+Prove: exists i : Z. P_P(0, i, 1.0).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Let3,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 94):
+Prove: exists i : Z. P_P(255, i, 1.0).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Let4,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 95):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((10 <= i_1) -> ((i_1 <= 10) -> P_P(i_1, i, r))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Let5,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 96):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((i_1 <= 0) -> (((-5) <= i_1) -> P_P(i_1, i, r))))).
+
+------------------------------------------------------------
+
+Goal Check 'ko,Let6,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 97):
+Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
+    (exists r : R. ((255 <= i_1) -> ((i_1 <= 599) -> P_P(i_1, i, r))))).
+
+------------------------------------------------------------
 ------------------------------------------------------------
   Function f
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
index 696cfec43770e4113b397f51767d8f05354ec8ec..fc119b8181b6ad0bf377c2a272cd82e97e22ef16 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
@@ -11,7 +11,7 @@
 [wp] [Qed] Goal typed_main_requires_qed_ok_Struct_Simple_a : Valid
 [wp] [Qed] Goal typed_main_requires_qed_ok_Struct_Simple_b : Valid
 [wp] [Qed] Goal typed_main_requires_qed_ok_Simple_Array_0 : Valid
-[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_Simple_Array_1 : Valid
+[wp] [Qed] Goal typed_main_requires_qed_ok_Simple_Array_1 : Valid
 [wp] [Qed] Goal typed_main_requires_qed_ok_With_Array_Struct_5 : Valid
 [wp] [Qed] Goal typed_main_requires_qed_ok_With_Array_Struct_3 : Valid
 [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_Sc_eq : Valid
@@ -25,19 +25,19 @@
 [wp] [Qed] Goal typed_main_requires_qed_ok_2 : Valid
 [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Valid
 [wp] [Qed] Goal typed_main_requires_qed_ok_todo : Valid
-[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Valid
+[wp] [Qed] Goal typed_main_requires_qed_ok_4 : Valid
 [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Valid
 [wp] [Qed] Goal typed_main_requires_qed_ok_direct_init_union : Valid
 [wp] Proved goals:   24 / 24
-  Qed:            17 
-  Alt-Ergo:        7
+  Qed:            19 
+  Alt-Ergo:        5
 [wp] Report in:  'tests/wp_acsl/oracle_qualif/init_value.0.report.json'
 [wp] Report out: 'tests/wp_acsl/result_qualif/init_value.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
-main                14      6 (28..40)      20       100%
+main                16      4 (28..40)      20       100%
 fa1                  1     -                 1       100%
 fa2                  1     -                 1       100%
 fa3                  1     -                 1       100%
-fs1                 -       1 (160..184)     1       100%
+fs1                 -       1 (112..136)     1       100%
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
index 1cb1e0e7c153e74ab3cd5bc0a045af6ee9fd750f..b3420038f619f8d1c9e8bfff710a37558c5ef46f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
@@ -3,7 +3,10 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
-[wp] 15 goals scheduled
+[wp] 18 goals scheduled
+[wp] [Alt-Ergo] Goal typed_check_acsl_check_ok_C1_absurd_is_cint : Valid
+[wp] [Alt-Ergo] Goal typed_check_acsl_check_ok_C2_absurd_is_cint : Valid
+[wp] [Qed] Goal typed_check_acsl_check_ok_C5_absurd_cmp : Valid
 [wp] [Alt-Ergo] Goal typed_f_ensures : Valid
 [wp] [Alt-Ergo] Goal typed_f_loop_invariant_preserved : Valid
 [wp] [Qed] Goal typed_f_loop_invariant_established : Valid
@@ -19,13 +22,14 @@
 [wp] [Alt-Ergo] Goal typed_g_loop_invariant_2_preserved : Valid
 [wp] [Qed] Goal typed_g_loop_invariant_2_established : Valid
 [wp] [Qed] Goal typed_g_loop_assigns : Valid
-[wp] Proved goals:   15 / 15
-  Qed:             6 
-  Alt-Ergo:        9
+[wp] Proved goals:   18 / 18
+  Qed:             7 
+  Alt-Ergo:       11
 [wp] Report in:  'tests/wp_acsl/oracle_qualif/simpl_is_type.0.report.json'
 [wp] Report out: 'tests/wp_acsl/result_qualif/simpl_is_type.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
 f                    3      6 (96..120)      9       100%
 g                    3      3 (36..48)       6       100%
+check_acsl           1      2 (44..56)       3       100%
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/simpl_is_type.i b/src/plugins/wp/tests/wp_acsl/simpl_is_type.i
index 36c26e7c0e7088dbf06908eabba8231aa38b81d3..f7a27800a62c95cef8fec3606afb3ad777959d99 100644
--- a/src/plugins/wp/tests/wp_acsl/simpl_is_type.i
+++ b/src/plugins/wp/tests/wp_acsl/simpl_is_type.i
@@ -3,7 +3,7 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-simplify-is-cint
+   OPT: -wp-simplify-is-cint -wp-prop=-ko,-lack
 */
 
 /** Tests the simplification of (forall x:int. P) into (forall
@@ -56,3 +56,44 @@ int g(int *t, int size, int x){
   return 0;
 
 }
+
+//@ axiomatic A { predicate P(integer x, integer y, real f) reads \nothing; }
+void check_acsl (void) {
+  //@ check ko: A1: absorb_is_cint: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 0 <= x < 64 ==> P(x,y,f);
+  //@ check ko: A2: absorb_is_cint: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 0 <= x < 64 && P(y,x,1.0) ==> P(x,y,f);
+  //@ check ko: A3: absorb_is_cint: \exists integer y ; \forall unsigned char x ; \exists real f ; 0 <= x < 64 ==> P(x,y,f);
+  //@ check ko: A4: absorb_is_cint: \exists integer y ; \forall unsigned char x ; \exists real f ; 0 <= x < 64 && P(y,x,f) ==> P(x,y,f);
+
+  //@ check ok:   C1: absurd_is_cint: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; -900000 <= x < 0 && P(y,x,f) ==> P(x,y,f);
+  //@ check ok:   C2: absurd_is_cint: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; -900000 <= x < 0 && P(y,x,f) ==> P(x,y,f);
+  //@ check lack: C3: absurd_is_cint: \exists integer y ; \forall unsigned char x ; \exists real f ; -900000 <= x < 0 && P(y,x,f) ==> P(x,y,f);
+  //@ check lack: C4: absurd_is_cint: \exists integer y ; \forall unsigned char x ; \exists real f ; -900000 <= x < 0 && P(y,x,f) ==> P(x,y,f);
+  //@ check ok:   C5:     absurd_cmp: \let f = 1.0; \forall integer x ; (\exists integer y ; 0 < y < 1) ==> P(3,5,f);
+  //@ check ko:   B5:  no_absurd_cmp: \let f = 1.0; \forall integer x ; (\exists real    y ; 0 < y < 1) ==> P(3,5,f);
+
+  //@ check ko: Min1: reduces_min: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; -5 <= x < 100 ==> P(x,y,f);
+  //@ check ko: Min2: reduces_min: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 10 <= x < 100 && P(10,y,f) ==> P(x,y,f);
+  //@ check ko: Min3: reduces_min: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 10 <= x < 100 && P(10,y,f) && P(11,y,f) && P(13,y,f) ==> P(x,y,f);
+  //@ check ko: Min4: reduces_min: \exists integer y ; \forall unsigned char x ; \exists real f ; -5 <= x < 100 ==> P(x,y,f);
+  //@ check ko: Min5: reduces_min: \exists integer y ; \forall unsigned char x ; \exists real f ; 10 <= x < 100 && P(10,y,f) ==> P(x,y,f);
+  //@ check ko: Min6: reduces_min: \exists integer y ; \forall unsigned char x ; \exists real f ; 10 <= x < 100 && P(10,y,f) && P(11,y,f) && P(13,y,f) ==> P(x,y,f);
+
+  //@ check ko: Max1: reduces_max: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 10 <= x < 600 ==> P(x,y,f);
+  //@ check ko: Max2: reduces_max: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 10 <= x < 100 && P(98,y,f) && P(99,y,f) ==> P(x,y,f);
+  //@ check ko: Max3: reduces_max: \exists integer y ; \forall unsigned char x ; \exists real f ; 10 <= x < 600 ==> P(x,y,f);
+  //@ check ko: Max4: reduces_max: \exists integer y ; \forall unsigned char x ; \exists real f ; 10 <= x < 100 && P(98,y,f) && P(99,y,f) ==> P(x,y,f);
+
+  //@ check ko: MinMax1: reduce_minmax: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; -5 <= x < 100 && P(98,y,f) && P(99,y,f) ==> P(x,y,f);
+  //@ check ko: MinMax2: reduce_minmax: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 10 <= x < 100 && P(10,y,f) && P(11,y,f) && P(13,y,f) &&P(98,y,f) && P(99,y,f) ==> P(x,y,f);
+  //@ check ko: MinMax3: reduce_minmax: \exists integer y ; \forall unsigned char x ; \exists real f ; -5 <= x < 100 && P(98,y,f) && P(99,y,f) ==> P(x,y,f);
+  //@ check ko: MinMax4: reduce_minmax: \exists integer y ; \forall unsigned char x ; \exists real f ; 10 <= x < 100 && P(10,y,f) && P(11,y,f) && P(13,y,f) &&P(98,y,f) && P(99,y,f) ==> P(x,y,f);
+
+
+  //@ check ko: Let1: intro_let: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 10 <= x < 11 ==> P(x,y,f);
+  //@ check ko: Let2: intro_let: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; -5 <= x < 1 ==> P(x,y,f);
+  //@ check ko: Let3: intro_let: \exists integer y ; \forall unsigned char x ; \let f = 1.0   ; 255 <= x < 600 ==> P(x,y,f);
+  //@ check ko: Let4: intro_let: \exists integer y ; \forall unsigned char x ; \exists real f ; 10 <= x < 11 ==> P(x,y,f);
+  //@ check ko: Let5: intro_let: \exists integer y ; \forall unsigned char x ; \exists real f ; -5 <= x < 1 ==> P(x,y,f);
+  //@ check ko: Let6: intro_let: \exists integer y ; \forall unsigned char x ; \exists real f ; 255 <= x < 600 ==> P(x,y,f);
+
+}
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index fed0f0257b43b01a4adf56ecd94d3c31195a0263..e889fe4a6738733e3c74bc71527620338455930d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -172,9 +172,7 @@ Assume {
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
       ((m[i_1].F1_T_a) = 0))).
   (* Call Effects *)
-  Have: (forall i_1 : Z. ((i_1 != 1) -> (smatrix_1[i_1] = smatrix_0[i_1]))) /\
-      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
-       (((i_1 < 0) \/ (5 <= i_1)) -> (smatrix_1[1][i_1] = m[i_1]))))).
+  Have: forall i_1 : Z. ((i_1 != 1) -> (smatrix_1[i_1] = smatrix_0[i_1])).
 }
 Prove: (m[i].F1_T_a) = 0.
 
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index 92a060753dfd1ee1cb05e5af64a26b33a619de9b..3beaa58f2543d773ccd2649dd8da348ef9a70cb9 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -230,9 +230,7 @@ Assume {
   (* Call 'reset_5' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
   (* Call Effects *)
-  Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1]))) /\
-      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
-       (((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
+  Have: forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1])).
   (* Call 'add_5' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
       (reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
@@ -243,19 +241,16 @@ Prove: m_1[i] = reg_load_0[i].
 
 Goal Post-condition 'Preset' in 'calls_on_array_dim_2_to_1':
 Let m = tt_0[0].
-Let m_1 = tt_1[0].
 Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 4).
   (* Call 'load_5' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
-      (m_1[i_1] = reg_load_0[i_1]))).
+      (tt_1[0][i_1] = reg_load_0[i_1]))).
   (* Call 'reset_5' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
   (* Call Effects *)
-  Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_1[i_1] = tt_0[i_1]))) /\
-      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
-       (((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
+  Have: forall i_1 : Z. ((i_1 != 0) -> (tt_1[i_1] = tt_0[i_1])).
   (* Call 'add_5' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
       (reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
@@ -276,9 +271,7 @@ Assume {
   (* Call 'reset_5' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
   (* Call Effects *)
-  Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1]))) /\
-      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
-       (((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
+  Have: forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1])).
   (* Call 'add_5' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
       (reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 099a8b0731ad6cd478d7ada6d46db738c28d17bc..7ed70002fbc5d83e5b704f38f2a51dc1652dab1f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -1278,10 +1278,6 @@ Goal Post-condition (file tests/wp_typed/user_init.i, line 68) in 'init_t2_v2':
 Assume {
   (* Goal *)
   When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
       ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
@@ -1296,24 +1292,16 @@ Assume {
   Type: is_uint32(i).
   (* Goal *)
   When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
-      ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+      ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
-      ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+      ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
 }
@@ -1329,26 +1317,18 @@ Prove: true.
 Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 76):
 Assume {
   Type: is_uint32(i).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_1[i][i_1] = v))).
 }
 Prove: to_uint32(1 + i) <= 10.
 
@@ -1365,24 +1345,16 @@ Assume {
   Type: is_uint32(i) /\ is_uint32(j).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 < i) -> ((0 <= i_2) ->
-      ((i_2 <= 19) -> (t2_2[i_3][i_2] = v))))).
+      ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 < i) -> ((0 <= i_2) ->
-      ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_2[i_3][i_2]))))).
+      ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_1[i_3][i_2]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (m[i_2] = v))).
   (* Invariant 'Range_j' *)
@@ -1405,10 +1377,6 @@ Assume {
   Type: is_uint32(i) /\ is_uint32(j).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
       ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
@@ -1416,10 +1384,6 @@ Assume {
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
       ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
@@ -1442,26 +1406,18 @@ Prove: true.
 Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 82):
 Assume {
   Type: is_uint32(i) /\ is_uint32(j).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_1[i][i_1] = v))).
   (* Invariant 'Range_j' *)
   Have: (0 <= j) /\ (j <= 20).
   (* Then *)
@@ -1498,27 +1454,19 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
+      ((i_6 <= 19) -> (t2_0[i_7][i_6] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i_2) /\ (i_2 <= 10).
   (* Then *)
   Have: i_2 <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
+      ((i_6 <= 19) -> (t2_1[i_7][i_6] = t2_0[i_7][i_6]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
-      (t2_2[i_2][i_6] = v))).
+      (t2_1[i_2][i_6] = v))).
 }
 Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
     (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
@@ -1532,27 +1480,19 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
+      ((i_6 <= 19) -> (t2_0[i_7][i_6] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i_2) /\ (i_2 <= 10).
   (* Then *)
   Have: i_2 <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
+      ((i_6 <= 19) -> (t2_1[i_7][i_6] = t2_0[i_7][i_6]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
-      (t2_2[i_2][i_6] = v))).
+      (t2_1[i_2][i_6] = v))).
 }
 Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
     (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
@@ -1571,26 +1511,18 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
+      ((i_6 <= 19) -> (t2_0[i_7][i_6] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i_2) /\ (i_2 <= 10).
   (* Then *)
   Have: i_2 <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
+      ((i_6 <= 19) -> (t2_1[i_7][i_6] = t2_0[i_7][i_6]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < j) -> (t2_2[i_2][i_6] = v))).
+  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < j) -> (t2_1[i_2][i_6] = v))).
   (* Invariant 'Range_j' *)
   Have: (0 <= j) /\ (j <= 20).
   (* Then *)
@@ -1607,24 +1539,16 @@ Assume {
   Type: is_uint32(i) /\ is_uint32(j).
   (* Goal *)
   When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: i <= 10.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_1[i][i_1] = v))).
   (* Invariant 'Range_j' *)
   Have: j <= 20.
 }
@@ -1648,10 +1572,6 @@ Assume {
   Have: i_3 <= 19.
   Have: 0 <= i.
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
-      ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
-      (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
 }
 Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
     (i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
@@ -1661,26 +1581,18 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
 Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 80):
 Assume {
   Type: is_uint32(i).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_1[i][i_1] = v))).
 }
 Prove: i < to_uint32(1 + i).
 
@@ -1694,26 +1606,18 @@ Prove: true.
 Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 87):
 Assume {
   Type: is_uint32(i) /\ is_uint32(j).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_1[i][i_1] = v))).
   (* Invariant 'Range_j' *)
   Have: (0 <= j) /\ (j <= 20).
   (* Then *)
@@ -1736,10 +1640,6 @@ Assume {
   Type: is_sint32(v).
   (* Goal *)
   When: (0 <= i) /\ (i <= 9).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
       P_MemSet20(t2_0[i_1], 20, v))).
@@ -1754,10 +1654,6 @@ Assume {
       IsArray1_sint32(t2_0[i]).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       P_MemSet20(t2_0[i_2], 20, v_1))).
@@ -1781,10 +1677,6 @@ Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
       IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1809,10 +1701,6 @@ Let m = v[j <- v_1].
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
       is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]) /\ IsArray1_sint32(m).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1835,10 +1723,6 @@ Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, li
 Let m = t2_0[i].
 Assume {
   Type: is_uint32(i) /\ is_sint32(v) /\ IsArray1_sint32(m).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v))).
@@ -1855,10 +1739,6 @@ Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
       is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1905,10 +1785,6 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_1[i_7][i_6] = t2_0[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < i_2) ->
       P_MemSet20(t2_0[i_6], 20, v_1))).
@@ -1931,10 +1807,6 @@ Assume {
       IsArray1_sint32(t2_0[i]).
   (* Goal *)
   When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       P_MemSet20(t2_0[i_2], 20, v_1))).
@@ -1974,10 +1846,6 @@ Assume {
   Have: i_3 <= 19.
   Have: 0 <= i.
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
-      ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
-      (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
 }
 Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
     (i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
@@ -1988,10 +1856,6 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 1
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
       IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -2015,10 +1879,6 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 1
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
       is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index 620a41fc301d404db82f618cac7e8a585d940513..f759219c74fa5cf2cda5b811b530c4a10cb3cc1c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -1278,10 +1278,6 @@ Goal Post-condition (file tests/wp_typed/user_init.i, line 68) in 'init_t2_v2':
 Assume {
   (* Goal *)
   When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
       ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
@@ -1296,24 +1292,16 @@ Assume {
   Type: is_uint32(i).
   (* Goal *)
   When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
-      ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+      ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
-      ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+      ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
 }
@@ -1329,26 +1317,18 @@ Prove: true.
 Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 76):
 Assume {
   Type: is_uint32(i).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_1[i][i_1] = v))).
 }
 Prove: to_uint32(1 + i) <= 10.
 
@@ -1365,24 +1345,16 @@ Assume {
   Type: is_uint32(i) /\ is_uint32(j).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 < i) -> ((0 <= i_2) ->
-      ((i_2 <= 19) -> (t2_2[i_3][i_2] = v))))).
+      ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 < i) -> ((0 <= i_2) ->
-      ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_2[i_3][i_2]))))).
+      ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_1[i_3][i_2]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (m[i_2] = v))).
   (* Invariant 'Range_j' *)
@@ -1405,10 +1377,6 @@ Assume {
   Type: is_uint32(i) /\ is_uint32(j).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
       ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
@@ -1416,10 +1384,6 @@ Assume {
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
-      ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
-      (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
       ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
@@ -1442,26 +1406,18 @@ Prove: true.
 Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 82):
 Assume {
   Type: is_uint32(i) /\ is_uint32(j).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_1[i][i_1] = v))).
   (* Invariant 'Range_j' *)
   Have: (0 <= j) /\ (j <= 20).
   (* Then *)
@@ -1498,27 +1454,19 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
+      ((i_6 <= 19) -> (t2_0[i_7][i_6] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i_2) /\ (i_2 <= 10).
   (* Then *)
   Have: i_2 <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
+      ((i_6 <= 19) -> (t2_1[i_7][i_6] = t2_0[i_7][i_6]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
-      (t2_2[i_2][i_6] = v))).
+      (t2_1[i_2][i_6] = v))).
 }
 Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
     (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
@@ -1532,27 +1480,19 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
+      ((i_6 <= 19) -> (t2_0[i_7][i_6] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i_2) /\ (i_2 <= 10).
   (* Then *)
   Have: i_2 <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
+      ((i_6 <= 19) -> (t2_1[i_7][i_6] = t2_0[i_7][i_6]))))).
   (* Invariant 'Partial_j' *)
   Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
-      (t2_2[i_2][i_6] = v))).
+      (t2_1[i_2][i_6] = v))).
 }
 Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
     (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
@@ -1571,26 +1511,18 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
+      ((i_6 <= 19) -> (t2_0[i_7][i_6] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i_2) /\ (i_2 <= 10).
   (* Then *)
   Have: i_2 <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
-      ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
+      ((i_6 <= 19) -> (t2_1[i_7][i_6] = t2_0[i_7][i_6]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < j) -> (t2_2[i_2][i_6] = v))).
+  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < j) -> (t2_1[i_2][i_6] = v))).
   (* Invariant 'Range_j' *)
   Have: (0 <= j) /\ (j <= 20).
   (* Then *)
@@ -1607,24 +1539,16 @@ Assume {
   Type: is_uint32(i) /\ is_uint32(j).
   (* Goal *)
   When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: i <= 10.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_1[i][i_1] = v))).
   (* Invariant 'Range_j' *)
   Have: j <= 20.
 }
@@ -1648,10 +1572,6 @@ Assume {
   Have: i_3 <= 19.
   Have: 0 <= i.
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
-      ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
-      (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
 }
 Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
     (i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
@@ -1661,26 +1581,18 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
 Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 80):
 Assume {
   Type: is_uint32(i).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_1[i][i_1] = v))).
 }
 Prove: i < to_uint32(1 + i).
 
@@ -1694,26 +1606,18 @@ Prove: true.
 Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 87):
 Assume {
   Type: is_uint32(i) /\ is_uint32(j).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+      ((i_1 <= 19) -> (t2_0[i_2][i_1] = v))))).
   (* Invariant 'Range_i' *)
   Have: (0 <= i) /\ (i <= 10).
   (* Then *)
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_j' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
   (* Invariant 'Previous_i' *)
   Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+      ((i_1 <= 19) -> (t2_1[i_2][i_1] = t2_0[i_2][i_1]))))).
   (* Invariant 'Partial_j' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_1[i][i_1] = v))).
   (* Invariant 'Range_j' *)
   Have: (0 <= j) /\ (j <= 20).
   (* Then *)
@@ -1736,10 +1640,6 @@ Assume {
   Type: is_sint32(v).
   (* Goal *)
   When: (0 <= i) /\ (i <= 9).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
       P_MemSet20(t2_0[i_1], 20, v))).
@@ -1754,10 +1654,6 @@ Assume {
       IsArray1_sint32(t2_0[i]).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       P_MemSet20(t2_0[i_2], 20, v_1))).
@@ -1781,10 +1677,6 @@ Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
       IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1809,10 +1701,6 @@ Let m = v[j <- v_1].
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
       is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]) /\ IsArray1_sint32(m).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1835,10 +1723,6 @@ Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, li
 Let m = t2_0[i].
 Assume {
   Type: is_uint32(i) /\ is_sint32(v) /\ IsArray1_sint32(m).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v))).
@@ -1855,10 +1739,6 @@ Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
       is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1905,10 +1785,6 @@ Assume {
   (* Goal *)
   When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
       (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
-      ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
-      (t2_1[i_7][i_6] = t2_0[i_7][i_6])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < i_2) ->
       P_MemSet20(t2_0[i_6], 20, v_1))).
@@ -1931,10 +1807,6 @@ Assume {
       IsArray1_sint32(t2_0[i]).
   (* Goal *)
   When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((0 <= i_2) -> ((i_3 <= 9) ->
-      ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
-      (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       P_MemSet20(t2_0[i_2], 20, v_1))).
@@ -1974,10 +1846,6 @@ Assume {
   Have: i_3 <= 19.
   Have: 0 <= i.
   Have: i <= 9.
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
-      ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
-      (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
 }
 Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
     (i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
@@ -1988,10 +1856,6 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 1
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
       IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -2015,10 +1879,6 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 1
 Assume {
   Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
       is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
-  (* Loop assigns 'tactic,Zone_i' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
-      ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
-      (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
   (* Invariant 'Partial_i' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       P_MemSet20(t2_0[i_1], 20, v_1))).
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index 476ee7df2e400ce497d6f2692ba419dd46bab530..cc112824722069d119c08dbe0974f80fb1083582 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -110,7 +110,7 @@ Functions           WP     Alt-Ergo        Total   Success
 init                 6      4 (80..104)     10       100%
 init_t1              6      4 (12..24)      10       100%
 init_t2_v1           9      8 (40..52)      17       100%
-init_t2_v2           9      8 (32..44)      17       100%
+init_t2_v2           9      8 (24..36)      17       100%
 init_t2_v3           7      8 (28..40)      15       100%
 init_t2_bis_v1       7      4 (208..256)    11       100%
 init_t2_bis_v2       7      4 (192..240)    11       100%