Merge branch 'feature/patrick/improved-wp-simplifiers' into 'master'

[wp] Improves simplifiers

See merge request frama-c/frama-c!2294

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

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
+
 (* -------------------------------------------------------------------------- *)

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

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
 ------------------------------------------------------------

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%
 -------------------------------------------------------------

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%
 -------------------------------------------------------------

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);
+
+}

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.
 

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])))).

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%