diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index f4924f0490375eaf58d70a78c06ad2ef72486d16..3957a58125d11475b0f07091ccb0d32b9e51096b 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -815,177 +815,295 @@ 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
- | _ -> ()
+ | _ -> dom
+ end
+ | _ -> dom
+end
+
+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
- aux (Lang.F.e_prop p)
+ 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
+ | 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 target _ = ()
- method fixpoint = ()
+ val mutable domain : Dom.t = Dom.top
- method private simplify ~is_goal p =
- let pool = Lang.get_pool () in
+ method name = "Remove redundant is_cint"
+ method copy = {< domain = domain >}
- 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
+ method target _ = ()
+ method fixpoint = ()
+
+ method assume p =
+ Lang.iter_confident_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
- 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
- | _ -> ()
- 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
+ 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
- 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
- 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))
+ (* [~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 simplify_exp (e : term) = e
+ method simplify_exp (e : term) = e
- method simplify_hyp p = self#simplify ~is_goal:false p
+ method simplify_hyp p = self#simplify ~is_goal:false p
- method simplify_goal p = self#simplify ~is_goal:true p
+ method simplify_goal p = self#simplify ~is_goal:true p
- method simplify_branch p = p
+ method simplify_branch p = p
- method infer = []
-end
+ method infer = []
+ end
let mask_simplifier =
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 4bdd96e577592e920b55247a65817225f9fce919..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
@@ -165,20 +165,17 @@ Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
------------------------------------------------------------
Goal Check 'ko,Let1,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 92):
-Prove: exists i : Z. forall i_1 : Z. ((10 <= i_1) -> ((i_1 <= 10) ->
- P_P(i_1, i, 1.0))).
+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. forall i_1 : Z. ((i_1 <= 0) -> ((0 <= i_1) ->
- (((-5) <= i_1) -> P_P(i_1, i, 1.0)))).
+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. forall i_1 : Z. ((255 <= i_1) -> ((i_1 <= 255) ->
- ((i_1 <= 599) -> P_P(i_1, i, 1.0)))).
+Prove: exists i : Z. P_P(255, i, 1.0).
------------------------------------------------------------
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_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%