diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index c80e3d856df2bb4e30891f3a8aa70bb35820a76c..7dce79dd88cbd3e6e2cd113c0690e73d9cc0b06e 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1308,7 +1308,8 @@ struct
 
   let assigned_loc seq obj = function
     | Ref x -> noref ~op:"assigns to" x
-    | Val((CVAL|CREF),_,[]) -> [] (* full update *)
+    | Val((CVAL|CREF),x,[]) ->
+        [ Assert (monotonic_initialized seq obj x []) ]
     | Val((CVAL|CREF),_,_) as vloc ->
         let v = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
         memvar_assigned seq obj vloc (e_var v)
@@ -1320,7 +1321,8 @@ struct
   let assigned_array seq obj l elt n =
     match l with
     | Ref x -> noref ~op:"assigns to" x
-    | Val((CVAL|CREF),_,[]) -> [] (* full update *)
+    | Val((CVAL|CREF),x,[]) ->
+        [ Assert (monotonic_initialized seq obj x []) ]
     | Val((CVAL|CREF),x,ofs) as vloc ->
         let te = Lang.tau_of_object elt in
         let v = Lang.freshvar ~basename:"v" Qed.Logic.(Array(Int,te)) in
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
index 877f61f698c7c5491b55d89680f8988a74b1a58e..139898f8d3eff53ad8b3d93d5c5f9c1e1332f5ef 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
@@ -1,56 +1,119 @@
+/* run.config
+  OPT: -wp-prop=CHECK
+*/
+/* run.config_qualif
+  OPT: -wp-prop=CHECK
+*/
+
 struct S {
   int i ;
   int a[10] ;
 };
 
-int main(struct S* s){
+void initialize(struct S* s){
   s->i = 0 ;
   /*@
-    loop invariant 0 <= i <= 10;
-    loop invariant \initialized(&s->a[0 .. i-1]);
+    loop invariant CHECK: 0 <= i <= 10 && \initialized(&s->a[0 .. i-1]);
+    loop assigns CHECK: i, s->a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s->a[i] = 0;
+
+  //@ check CHECK: \initialized(s);
+}
+
+void range(struct S* s){
+  s->i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s->a[0 .. i-1]);
     loop assigns i, s->a[0 .. 9];
   */
   for(int i = 0; i < 10; ++i) s->a[i] = 0;
 
-  //@ check \initialized(s);
-  
-  /*@ loop assigns i, s->a[1 .. 4]; */
+  /*@ loop assigns CHECK: i, s->a[1 .. 4]; */
   for(int i = 0; i < 10; ++i){
     if(1 <= i && i <= 4) s->a[i] = 1 ;
   }
+  //@ check CHECK: \initialized(s);
+}
+
+void field(struct S* s){
+  s->i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s->a[0 .. i-1]);
+    loop assigns i, s->a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s->a[i] = 0;
 
-  //@ check \initialized(s);
-  
-  /*@ loop assigns i, s->i; */
+  /*@ loop assigns CHECK: i, s->i; */
   for(int i = 0; i < 10; ++i){
     s->i++;
   }
+  //@ check CHECK: \initialized(s);
+}
 
-  //@ check \initialized(s);
-  
-  /*@ 
+void array(struct S* s){
+  s->i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s->a[0 .. i-1]);
+    loop assigns i, s->a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s->a[i] = 0;
+
+  /*@
     loop invariant 0 <= i <= 10;
-    loop assigns i, s->a[0..9]; 
+    loop assigns CHECK: i, s->a[0..9];
   */
   for(int i = 0; i < 10; ++i){
     s->a[i] = 1 ;
   }
+  //@ check CHECK: \initialized(s);
+}
 
-  //@ check \initialized(s);
-  
-  /*@ loop assigns i, s->a[4]; */
+void index(struct S* s){
+  s->i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s->a[0 .. i-1]);
+    loop assigns i, s->a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s->a[i] = 0;
+
+  /*@ loop assigns CHECK: i, s->a[4]; */
   for(int i = 0; i < 10; ++i){
     if(i == 4) s->a[i] = 1 ;
   }
+  //@ check CHECK: \initialized(s);
+}
 
-  //@ check \initialized(s);
-  
-  /*@ loop assigns i, { s->a[i] | integer i ; i \in { 0, 2, 4 } }; */
+void descr(struct S* s){
+  s->i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s->a[0 .. i-1]);
+    loop assigns i, s->a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s->a[i] = 0;
+
+  /*@ loop assigns CHECK: i, { s->a[i] | integer i ; i \in { 0, 2, 4 } }; */
   for(int i = 0; i < 10; ++i){
     if(i == 0 || i == 2 || i == 4) s->a[i] = 1 ;
   }
-  
-  //@ check \initialized(s);
-  //@ check SMOKE: \false;
+  //@ check CHECK: \initialized(s);
 }
 
+void comp(struct S* s){
+  s->i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s->a[0 .. i-1]);
+    loop assigns i, s->a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s->a[i] = 0;
+
+  /*@
+    loop invariant 0 <= i <= 10 ;
+    loop assigns CHECK: i, *s;
+  */
+  for(int i = 0; i < 10; ++i){
+    s->a[i] = 1 ;
+    s->i++;
+  }
+  //@ check CHECK: \initialized(s);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
index 72dcc1acd7a5f2d7c35b82bc0186f112698ecf04..6ce93865705c61be2b35da0848b416e4ebe90a72 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
@@ -1,57 +1,126 @@
+/* run.config
+  OPT: -wp-prop=CHECK
+*/
+/* run.config_qualif
+  OPT: -wp-prop=CHECK
+*/
+
 struct S {
   int i ;
   int a[10] ;
 };
 
-int main(void){
+void initialize(void){
   struct S s ;
   s.i = 0 ;
   /*@
-    loop invariant 0 <= i <= 10;
-    loop invariant \initialized(&s.a[0 .. i-1]);
-    loop assigns i, s.a[0 .. 9];
+    loop invariant CHECK: 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+    loop assigns CHECK: i, s.a[0 .. 9];
   */
   for(int i = 0; i < 10; ++i) s.a[i] = 0;
 
-  //@ check \initialized(&s);
+  //@ check CHECK: \initialized(&s);
+}
+
+void range(void){
+  struct S s ;
+  s.i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+    loop assigns i, s.a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s.a[i] = 0;
 
-  /*@ loop assigns i, s.a[1 .. 4]; */
+  /*@ loop assigns CHECK: i, s.a[1 .. 4]; */
   for(int i = 0; i < 10; ++i){
     if(1 <= i && i <= 4) s.a[i] = 1 ;
   }
+  //@ check CHECK: \initialized(&s);
+}
+
+void field(void){
+  struct S s ;
+  s.i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+    loop assigns i, s.a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s.a[i] = 0;
 
-  //@ check \initialized(&s);
-  
-  /*@ loop assigns i, s.i; */
+  /*@ loop assigns CHECK: i, s.i; */
   for(int i = 0; i < 10; ++i){
     s.i++;
   }
+  //@ check CHECK: \initialized(&s);
+}
+
+void array(void){
+  struct S s ;
+  s.i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+    loop assigns i, s.a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s.a[i] = 0;
 
-  //@ check \initialized(&s);
-  
-  /*@ 
+  /*@
     loop invariant 0 <= i <= 10;
-    loop assigns i, s.a[0..9]; 
+    loop assigns CHECK: i, s.a[0..9];
   */
   for(int i = 0; i < 10; ++i){
     s.a[i] = 1 ;
   }
+  //@ check CHECK: \initialized(&s);
+}
 
-  //@ check \initialized(&s);
+void index(void){
+  struct S s ;
+  s.i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+    loop assigns i, s.a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s.a[i] = 0;
 
-  /*@ loop assigns i, s.a[4]; */
+  /*@ loop assigns CHECK: i, s.a[4]; */
   for(int i = 0; i < 10; ++i){
     if(i == 4) s.a[i] = 1 ;
   }
+  //@ check CHECK: \initialized(&s);
+}
 
-  //@ check \initialized(&s);
+void descr(void){
+  struct S s ;
+  s.i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+    loop assigns i, s.a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s.a[i] = 0;
 
-  /*@ loop assigns i, { s.a[i] | integer i ; i \in { 0, 2, 4 } }; */
+  /*@ loop assigns CHECK: i, { s.a[i] | integer i ; i \in { 0, 2, 4 } }; */
   for(int i = 0; i < 10; ++i){
     if(i == 0 || i == 2 || i == 4) s.a[i] = 1 ;
   }
-  
-  //@ check \initialized(&s);
-  //@ check SMOKE: \false;
+  //@ check CHECK: \initialized(&s);
 }
 
+void comp(void){
+  struct S s ;
+  s.i = 0 ;
+  /*@
+    loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+    loop assigns i, s.a[0 .. 9];
+  */
+  for(int i = 0; i < 10; ++i) s.a[i] = 0;
+
+  /*@
+    loop invariant 0 <= i <= 10 ;
+    loop assigns CHECK: i, s;
+  */
+  for(int i = 0; i < 10; ++i){
+    s.a[i] = 1 ;
+    s.i++;
+  }
+  //@ check CHECK: \initialized(&s);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
index 468f735b1db1917594a335ab0f1de83ac7eb77fb..9010d65214fc0afad229dbba9b5a89bb9b515245 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
@@ -4,609 +4,468 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 ------------------------------------------------------------
-  Function main
+  Function array
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 9):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 69):
 Let m = Init_0[shiftfield_F1_S_i(s) <- true].
 Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Init_undef_1, m, a_1, 10).
+Let a_3 = havoc(Init_undef_0, m, a_1, 10).
+Let a_4 = Load_Init_S1_S(s, a_3).
 Assume {
-  Type: is_sint32(i) /\ is_sint32(1 + i).
+  Type: is_sint32(i) /\ is_sint32(i_1).
   (* Heap *)
   Type: region(s.base) <= 0.
   (* Loop assigns ... *)
-  Have: forall i_1 : Z. let a_2 = shift_sint32(a, i_1) in ((0 <= i_1) ->
-      ((i_1 <= 9) -> ((m[a_2]=true) -> (a_1[a_2]=true)))).
+  Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+      ((i_2 <= 9) -> ((m[a_5]=true) -> (a_2[a_5]=true)))).
   (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_1[shift_sint32(a, i_1)]=true))).
+  Have: (0 <= i) /\ (i <= 10) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+       (a_2[shift_sint32(a, i_2)]=true)))).
+  (* Else *)
+  Have: 10 <= i.
+  (* Loop assigns 'CHECK' *)
+  Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+      ((i_2 <= 9) -> ((a_2[a_5]=true) -> (a_3[a_5]=true)))).
   (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Then *)
-  Have: i <= 9.
+  Have: (0 <= i_1) /\ (i_1 <= 10).
+  (* Else *)
+  Have: 10 <= i_1.
 }
-Prove: (-1) <= i.
+Prove: ((a_4.Init_F1_S_i)=true) /\
+    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+     ((a_4.Init_F1_S_a)[i_2]=true)))).
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 9):
+Goal Loop assigns 'CHECK' (1/3):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 10):
-Let m = Init_0[shiftfield_F1_S_i(s) <- true].
-Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: region(s.base) <= 0.
-  (* Goal *)
-  When: (0 <= i_1) /\ (i_1 <= i).
-  (* Loop assigns ... *)
-  Have: forall i_2 : Z. let a_2 = shift_sint32(a, i_2) in ((0 <= i_2) ->
-      ((i_2 <= 9) -> ((m[a_2]=true) -> (a_1[a_2]=true)))).
-  (* Invariant *)
-  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
-      (a_1[shift_sint32(a, i_2)]=true))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Then *)
-  Have: i <= 9.
-}
-Prove: (a_1[shift_sint32(a, i) <- true][shift_sint32(a, i_1)]=true).
+Goal Loop assigns 'CHECK' (2/3):
+Effect at line 66
+Prove: true.
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 10):
+Goal Loop assigns 'CHECK' (3/3):
+Effect at line 67
 Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function comp
+------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 15):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 118):
 Let m = Init_0[shiftfield_F1_S_i(s) <- true].
 Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
 Let a_2 = Load_Init_S1_S(s, a_1).
+Let a_3 = Load_Init_S1_S(s, havoc(Init_undef_0, m, s, 11)).
+Let P = a_3.Init_F1_S_i.
+Let a_4 = a_3.Init_F1_S_a.
 Assume {
-  Type: is_sint32(i).
+  Type: is_sint32(i) /\ is_sint32(i_1).
   (* Heap *)
   Type: region(s.base) <= 0.
   (* Loop assigns ... *)
-  Have: forall i_1 : Z. let a_3 = shift_sint32(a, i_1) in ((0 <= i_1) ->
-      ((i_1 <= 9) -> ((m[a_3]=true) -> (a_1[a_3]=true)))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_1[shift_sint32(a, i_1)]=true))).
+  Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+      ((i_2 <= 9) -> ((m[a_5]=true) -> (a_1[a_5]=true)))).
   (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
+  Have: (0 <= i) /\ (i <= 10) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+       (a_1[shift_sint32(a, i_2)]=true)))).
   (* Else *)
   Have: 10 <= i.
+  (* Loop assigns 'CHECK' *)
+  Have: ((((a_2.Init_F1_S_i)=true) -> (P=true))) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+       (((a_2.Init_F1_S_a)[i_2]=true) -> (a_4[i_2]=true))))).
+  (* Invariant *)
+  Have: (0 <= i_1) /\ (i_1 <= 10).
+  (* Else *)
+  Have: 10 <= i_1.
 }
-Prove: ((a_2.Init_F1_S_i)=true) /\
-    (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
-     ((a_2.Init_F1_S_a)[i_1]=true)))).
+Prove: (P=true) /\
+    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (a_4[i_2]=true)))).
 
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 22):
+Goal Loop assigns 'CHECK' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'CHECK' (2/3):
+Effect at line 114
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'CHECK' (3/3):
+Effect at line 115
 Let m = Init_0[shiftfield_F1_S_i(s) <- true].
 Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
-Let a_2 = havoc(Init_undef_0, a_1, shift_sint32(a, 1), 4).
-Let a_3 = Load_Init_S1_S(s, a_2).
+Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_2 = Load_Init_S1_S(s, a_1).
+Let a_3 = Load_Init_S1_S(s, havoc(Init_undef_1, m, s, 11)).
 Assume {
-  Type: is_sint32(i) /\ is_sint32(i_1).
+  Type: is_sint32(i_1) /\ is_sint32(i).
   (* Heap *)
-  Type: region(s.base) <= 0.
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_sint32(a, i), 1).
   (* Loop assigns ... *)
   Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 <= i_2) ->
       ((i_2 <= 9) -> ((m[a_4]=true) -> (a_1[a_4]=true)))).
   (* Invariant *)
-  Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
-      (a_1[shift_sint32(a, i_2)]=true))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Else *)
-  Have: 10 <= i.
-  (* Loop assigns ... *)
-  Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 < i_2) ->
-      ((i_2 <= 4) -> ((a_1[a_4]=true) -> (a_2[a_4]=true)))).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+       (a_1[shift_sint32(a, i_2)]=true)))).
   (* Else *)
   Have: 10 <= i_1.
+  (* Loop assigns 'CHECK' *)
+  Have: ((((a_2.Init_F1_S_i)=true) -> ((a_3.Init_F1_S_i)=true))) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+       (((a_2.Init_F1_S_a)[i_2]=true) -> ((a_3.Init_F1_S_a)[i_2]=true))))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
 }
-Prove: ((a_3.Init_F1_S_i)=true) /\
-    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
-     ((a_3.Init_F1_S_a)[i_2]=true)))).
+Prove: (-1) <= i.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function descr
+------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 29):
-Let a = shiftfield_F1_S_i(s).
-Let m = Init_0[a <- true].
-Let a_1 = shiftfield_F1_S_a(s).
-Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
-Let a_3 = havoc(Init_undef_0, a_2, shift_sint32(a_1, 1), 4).
-Let a_4 = Load_Init_S1_S(s, a_3[a <- true]).
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 99):
+Let a = shiftfield_F1_S_a(s).
+Let a_1 = shiftfield_F1_S_i(s).
+Let m = Init_1[a_1 <- true].
+Let a_2 = shift_sint32(a, 0).
+Let a_3 = havoc(Init_undef_0, m, a_2, 10).
+Let a_4 = Load_Init_S1_S(s, Init_0).
 Assume {
-  Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2).
+  Type: is_sint32(i) /\ is_sint32(i_1).
   (* Heap *)
   Type: region(s.base) <= 0.
   (* Loop assigns ... *)
-  Have: forall i_3 : Z. let a_5 = shift_sint32(a_1, i_3) in ((0 <= i_3) ->
-      ((i_3 <= 9) -> ((m[a_5]=true) -> (a_2[a_5]=true)))).
-  (* Invariant *)
-  Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i) ->
-      (a_2[shift_sint32(a_1, i_3)]=true))).
+  Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+      ((i_2 <= 9) -> ((m[a_5]=true) -> (a_3[a_5]=true)))).
   (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
+  Have: (0 <= i) /\ (i <= 10) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+       (a_3[shift_sint32(a, i_2)]=true)))).
   (* Else *)
   Have: 10 <= i.
-  (* Loop assigns ... *)
-  Have: forall i_3 : Z. let a_5 = shift_sint32(a_1, i_3) in ((0 < i_3) ->
-      ((i_3 <= 4) -> ((a_2[a_5]=true) -> (a_3[a_5]=true)))).
+  (* Loop assigns 'CHECK' *)
+  Have: (forall a_5 : addr.
+         ((forall i_2 : Z. (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) ->
+           (shift_sint32(a, i_2) != a_5))) ->
+         ((a_3[a_5]=true) <-> (Init_0[a_5]=true)))) /\
+      (forall a_5 : addr.
+       ((forall i_2 : Z. (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) ->
+         (shift_sint32(a, i_2) != a_5))) ->
+       (havoc(Mint_undef_0, Mint_0[a_1 <- 0], a_2, 10)[a_5] = Mint_1[a_5]))) /\
+      (forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in
+       (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) -> ((a_3[a_5]=true) ->
+       (Init_0[a_5]=true)))).
   (* Else *)
   Have: 10 <= i_1.
-  (* Else *)
-  Have: 10 <= i_2.
 }
 Prove: ((a_4.Init_F1_S_i)=true) /\
-    (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
-     ((a_4.Init_F1_S_a)[i_3]=true)))).
+    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+     ((a_4.Init_F1_S_a)[i_2]=true)))).
 
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 32):
-Let a = shiftfield_F1_S_i(s).
-Let m = Init_0[a <- true].
-Let a_1 = shiftfield_F1_S_a(s).
-Let a_2 = shift_sint32(a_1, 0).
+Goal Loop assigns 'CHECK' (1/5):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'CHECK' (2/5):
+Effect at line 96
+Let a = shiftfield_F1_S_a(s).
+Let a_1 = shiftfield_F1_S_i(s).
+Let m = Init_0[a_1 <- true].
+Let a_2 = shift_sint32(a, 0).
 Let a_3 = havoc(Init_undef_0, m, a_2, 10).
-Let a_4 = havoc(Init_undef_1, a_3, shift_sint32(a_1, 1), 4).
-Let a_5 = a_4[a <- true].
 Assume {
-  Type: is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\ is_sint32(i) /\
-      is_sint32(1 + i).
+  Type: is_sint32(i_2) /\ is_sint32(i_3).
   (* Heap *)
-  Type: region(s.base) <= 0.
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (!invalid(Malloc_0, shift_sint32(a, i_4), 1)) /\
+      ((i_4 = 0) \/ (i_4 = 2) \/ (i_4 = 4)) /\
+      ((i = 0) \/ (i = 2) \/ (i = 4)).
   (* Loop assigns ... *)
-  Have: forall i_4 : Z. let a_6 = shift_sint32(a_1, i_4) in ((0 <= i_4) ->
-      ((i_4 <= 9) -> ((m[a_6]=true) -> (a_3[a_6]=true)))).
-  (* Invariant *)
-  Have: forall i_4 : Z. ((0 <= i_4) -> ((i_4 < i_1) ->
-      (a_3[shift_sint32(a_1, i_4)]=true))).
+  Have: forall i_5 : Z. let a_4 = shift_sint32(a, i_5) in ((0 <= i_5) ->
+      ((i_5 <= 9) -> ((m[a_4]=true) -> (a_3[a_4]=true)))).
   (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
-  (* Else *)
-  Have: 10 <= i_1.
-  (* Loop assigns ... *)
-  Have: forall i_4 : Z. let a_6 = shift_sint32(a_1, i_4) in ((0 < i_4) ->
-      ((i_4 <= 4) -> ((a_3[a_6]=true) -> (a_4[a_6]=true)))).
+  Have: (0 <= i_2) /\ (i_2 <= 10) /\
+      (forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) ->
+       (a_3[shift_sint32(a, i_5)]=true)))).
   (* Else *)
   Have: 10 <= i_2.
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: forall i_4 : Z. let a_6 = shift_sint32(a_1, i_4) in ((0 <= i_4) ->
-      ((i_4 <= 9) -> ((a_5[a_6]=true) ->
-      (havoc(Init_undef_2, a_5, a_2, 10)[a_6]=true)))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
+  (* Loop assigns 'CHECK' *)
+  Have: (forall a_4 : addr.
+         ((forall i_5 : Z. (((i_5 = 0) \/ (i_5 = 2) \/ (i_5 = 4)) ->
+           (shift_sint32(a, i_5) != a_4))) ->
+         ((a_3[a_4]=true) <-> (Init_1[a_4]=true)))) /\
+      (forall a_4 : addr.
+       ((forall i_5 : Z. (((i_5 = 0) \/ (i_5 = 2) \/ (i_5 = 4)) ->
+         (shift_sint32(a, i_5) != a_4))) ->
+       (havoc(Mint_undef_0, Mint_0[a_1 <- 0], a_2, 10)[a_4] = Mint_1[a_4]))) /\
+      (forall i_5 : Z. let a_4 = shift_sint32(a, i_5) in
+       (((i_5 = 0) \/ (i_5 = 2) \/ (i_5 = 4)) -> ((a_3[a_4]=true) ->
+       (Init_1[a_4]=true)))).
   (* Then *)
-  Have: i <= 9.
+  Have: i_3 <= 9.
 }
-Prove: (-1) <= i.
+Prove: (i = 0) \/ (i = 2) \/ (i = 4) \/
+    ((i_1 != 0) /\ (i_1 != 2) /\ (i_1 != 4)).
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 32):
+Goal Loop assigns 'CHECK' (3/5):
+Effect at line 97
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 39):
+Goal Loop assigns 'CHECK' (4/5):
+Effect at line 97
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'CHECK' (5/5):
+Effect at line 97
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function field
+------------------------------------------------------------
+
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 51):
 Let a = shiftfield_F1_S_i(s).
 Let m = Init_0[a <- true].
 Let a_1 = shiftfield_F1_S_a(s).
-Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Init_undef_2, m, a_2, 10).
-Let a_4 = havoc(Init_undef_1, a_3, shift_sint32(a_1, 1), 4).
-Let a_5 = a_4[a <- true].
-Let a_6 = havoc(Init_undef_0, a_5, a_2, 10).
-Let a_7 = Load_Init_S1_S(s, a_6).
+Let a_2 = havoc(Init_undef_0, m, shift_sint32(a_1, 0), 10).
+Let a_3 = Load_Init_S1_S(s, a_2[a <- true]).
 Assume {
-  Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3).
+  Type: is_sint32(i) /\ is_sint32(i_1).
   (* Heap *)
   Type: region(s.base) <= 0.
   (* Loop assigns ... *)
-  Have: forall i_4 : Z. let a_8 = shift_sint32(a_1, i_4) in ((0 <= i_4) ->
-      ((i_4 <= 9) -> ((m[a_8]=true) -> (a_3[a_8]=true)))).
-  (* Invariant *)
-  Have: forall i_4 : Z. ((0 <= i_4) -> ((i_4 < i) ->
-      (a_3[shift_sint32(a_1, i_4)]=true))).
+  Have: forall i_2 : Z. let a_4 = shift_sint32(a_1, i_2) in ((0 <= i_2) ->
+      ((i_2 <= 9) -> ((m[a_4]=true) -> (a_2[a_4]=true)))).
   (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
+  Have: (0 <= i) /\ (i <= 10) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+       (a_2[shift_sint32(a_1, i_2)]=true)))).
   (* Else *)
   Have: 10 <= i.
-  (* Loop assigns ... *)
-  Have: forall i_4 : Z. let a_8 = shift_sint32(a_1, i_4) in ((0 < i_4) ->
-      ((i_4 <= 4) -> ((a_3[a_8]=true) -> (a_4[a_8]=true)))).
   (* Else *)
   Have: 10 <= i_1.
-  (* Else *)
-  Have: 10 <= i_2.
-  (* Loop assigns ... *)
-  Have: forall i_4 : Z. let a_8 = shift_sint32(a_1, i_4) in ((0 <= i_4) ->
-      ((i_4 <= 9) -> ((a_5[a_8]=true) -> (a_6[a_8]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_3) /\ (i_3 <= 10).
-  (* Else *)
-  Have: 10 <= i_3.
 }
-Prove: ((a_7.Init_F1_S_i)=true) /\
-    (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
-     ((a_7.Init_F1_S_a)[i_4]=true)))).
+Prove: ((a_3.Init_F1_S_i)=true) /\
+    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+     ((a_3.Init_F1_S_a)[i_2]=true)))).
 
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 46):
-Let a = shiftfield_F1_S_a(s).
-Let a_1 = shift_sint32(a, 4).
-Let a_2 = shiftfield_F1_S_i(s).
-Let m = Init_0[a_2 <- true].
-Let a_3 = shift_sint32(a, 0).
-Let a_4 = havoc(Init_undef_2, m, a_3, 10).
-Let a_5 = havoc(Init_undef_1, a_4, shift_sint32(a, 1), 4).
-Let a_6 = a_5[a_2 <- true].
-Let a_7 = havoc(Init_undef_0, a_6, a_3, 10).
-Let a_8 = Load_Init_S1_S(s, a_7[a_1 <- i]).
-Assume {
-  Type: is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
-      is_sint32(i_4) /\ is_sint32(i_5).
-  (* Heap *)
-  Type: region(s.base) <= 0.
-  (* Loop assigns ... *)
-  Have: forall i_6 : Z. let a_9 = shift_sint32(a, i_6) in ((0 <= i_6) ->
-      ((i_6 <= 9) -> ((m[a_9]=true) -> (a_4[a_9]=true)))).
-  (* Invariant *)
-  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < i_1) ->
-      (a_4[shift_sint32(a, i_6)]=true))).
-  (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
-  (* Else *)
-  Have: 10 <= i_1.
-  (* Loop assigns ... *)
-  Have: forall i_6 : Z. let a_9 = shift_sint32(a, i_6) in ((0 < i_6) ->
-      ((i_6 <= 4) -> ((a_4[a_9]=true) -> (a_5[a_9]=true)))).
-  (* Else *)
-  Have: 10 <= i_2.
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: forall i_6 : Z. let a_9 = shift_sint32(a, i_6) in ((0 <= i_6) ->
-      ((i_6 <= 9) -> ((a_6[a_9]=true) -> (a_7[a_9]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_4) /\ (i_4 <= 10).
-  (* Else *)
-  Have: 10 <= i_4.
-  (* Loop assigns ... *)
-  Have: ((Init_undef_0[a_1]=true) -> (i=true)).
-  (* Else *)
-  Have: 10 <= i_5.
-}
-Prove: ((a_8.Init_F1_S_i)=true) /\
-    (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
-     ((a_8.Init_F1_S_a)[i_6]=true)))).
+Goal Loop assigns 'CHECK' (1/2):
+Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 53):
-Let a = shiftfield_F1_S_a(s).
-Let a_1 = shiftfield_F1_S_i(s).
-Let m = Init_1[a_1 <- true].
-Let a_2 = shift_sint32(a, 0).
-Let a_3 = havoc(Init_undef_0, m, a_2, 10).
-Let a_4 = shift_sint32(a, 1).
-Let a_5 = havoc(Init_undef_1, a_3, a_4, 4).
-Let a_6 = a_5[a_1 <- true].
-Let a_7 = havoc(Init_undef_2, a_6, a_2, 10).
-Let a_8 = shift_sint32(a, 4).
-Let a_9 = a_7[a_8 <- i_6].
-Let a_10 = Load_Init_S1_S(s, Init_0).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
-      is_sint32(i_4) /\ is_sint32(i_5).
-  (* Heap *)
-  Type: region(s.base) <= 0.
-  (* Loop assigns ... *)
-  Have: forall i_7 : Z. let a_11 = shift_sint32(a, i_7) in ((0 <= i_7) ->
-      ((i_7 <= 9) -> ((m[a_11]=true) -> (a_3[a_11]=true)))).
-  (* Invariant *)
-  Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 < i) ->
-      (a_3[shift_sint32(a, i_7)]=true))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Else *)
-  Have: 10 <= i.
-  (* Loop assigns ... *)
-  Have: forall i_7 : Z. let a_11 = shift_sint32(a, i_7) in ((0 < i_7) ->
-      ((i_7 <= 4) -> ((a_3[a_11]=true) -> (a_5[a_11]=true)))).
-  (* Else *)
-  Have: 10 <= i_1.
-  (* Else *)
-  Have: 10 <= i_2.
-  (* Loop assigns ... *)
-  Have: forall i_7 : Z. let a_11 = shift_sint32(a, i_7) in ((0 <= i_7) ->
-      ((i_7 <= 9) -> ((a_6[a_11]=true) -> (a_7[a_11]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_3) /\ (i_3 <= 10).
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: ((Init_undef_2[a_8]=true) -> (i_6=true)).
-  (* Else *)
-  Have: 10 <= i_4.
-  (* Loop assigns ... *)
-  Have: (forall a_11 : addr.
-         ((forall i_7 : Z. (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) ->
-           (shift_sint32(a, i_7) != a_11))) ->
-         ((a_9[a_11]=true) <-> (Init_0[a_11]=true)))) /\
-      (forall a_11 : addr.
-       ((forall i_7 : Z. (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) ->
-         (shift_sint32(a, i_7) != a_11))) ->
-       (havoc(Mint_undef_0,
-          havoc(Mint_undef_1, havoc(Mint_undef_2, Mint_0[a_1 <- 0], a_2, 10),
-            a_4, 4)[a_1 <- v], a_2, 10)[a_8 <- v_1][a_11] = Mint_1[a_11]))) /\
-      (forall i_7 : Z. let a_11 = shift_sint32(a, i_7) in
-       (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) -> ((a_9[a_11]=true) ->
-       (Init_0[a_11]=true)))).
-  (* Else *)
-  Have: 10 <= i_5.
-}
-Prove: ((a_10.Init_F1_S_i)=true) /\
-    (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
-     ((a_10.Init_F1_S_a)[i_7]=true)))).
+Goal Loop assigns 'CHECK' (2/2):
+Effect at line 48
+Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function index
+------------------------------------------------------------
 
-Goal Check 'SMOKE' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 54):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 84):
 Let a = shiftfield_F1_S_a(s).
-Let a_1 = shiftfield_F1_S_i(s).
-Let m = Init_0[a_1 <- true].
-Let a_2 = shift_sint32(a, 0).
-Let a_3 = havoc(Init_undef_0, m, a_2, 10).
-Let a_4 = shift_sint32(a, 1).
-Let a_5 = havoc(Init_undef_1, a_3, a_4, 4).
-Let a_6 = a_5[a_1 <- true].
-Let a_7 = havoc(Init_undef_2, a_6, a_2, 10).
-Let a_8 = shift_sint32(a, 4).
-Let a_9 = a_7[a_8 <- i_6].
+Let a_1 = shift_sint32(a, 4).
+Let m = Init_0[shiftfield_F1_S_i(s) <- true].
+Let a_2 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_3 = Load_Init_S1_S(s, a_2[a_1 <- i]).
 Assume {
-  Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
-      is_sint32(i_4) /\ is_sint32(i_5).
+  Type: is_sint32(i_1) /\ is_sint32(i_2).
   (* Heap *)
   Type: region(s.base) <= 0.
   (* Loop assigns ... *)
-  Have: forall i_7 : Z. let a_10 = shift_sint32(a, i_7) in ((0 <= i_7) ->
-      ((i_7 <= 9) -> ((m[a_10]=true) -> (a_3[a_10]=true)))).
+  Have: forall i_3 : Z. let a_4 = shift_sint32(a, i_3) in ((0 <= i_3) ->
+      ((i_3 <= 9) -> ((m[a_4]=true) -> (a_2[a_4]=true)))).
   (* Invariant *)
-  Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 < i) ->
-      (a_3[shift_sint32(a, i_7)]=true))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Else *)
-  Have: 10 <= i.
-  (* Loop assigns ... *)
-  Have: forall i_7 : Z. let a_10 = shift_sint32(a, i_7) in ((0 < i_7) ->
-      ((i_7 <= 4) -> ((a_3[a_10]=true) -> (a_5[a_10]=true)))).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
+       (a_2[shift_sint32(a, i_3)]=true)))).
   (* Else *)
   Have: 10 <= i_1.
+  (* Loop assigns 'CHECK' *)
+  Have: ((Init_undef_0[a_1]=true) -> (i=true)).
   (* Else *)
   Have: 10 <= i_2.
-  (* Loop assigns ... *)
-  Have: forall i_7 : Z. let a_10 = shift_sint32(a, i_7) in ((0 <= i_7) ->
-      ((i_7 <= 9) -> ((a_6[a_10]=true) -> (a_7[a_10]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_3) /\ (i_3 <= 10).
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: ((Init_undef_2[a_8]=true) -> (i_6=true)).
-  (* Else *)
-  Have: 10 <= i_4.
-  (* Loop assigns ... *)
-  Have: (forall a_10 : addr.
-         ((forall i_7 : Z. (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) ->
-           (shift_sint32(a, i_7) != a_10))) ->
-         ((a_9[a_10]=true) <-> (Init_1[a_10]=true)))) /\
-      (forall a_10 : addr.
-       ((forall i_7 : Z. (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) ->
-         (shift_sint32(a, i_7) != a_10))) ->
-       (havoc(Mint_undef_0,
-          havoc(Mint_undef_1, havoc(Mint_undef_2, Mint_0[a_1 <- 0], a_2, 10),
-            a_4, 4)[a_1 <- v], a_2, 10)[a_8 <- v_1][a_10] = Mint_1[a_10]))) /\
-      (forall i_7 : Z. let a_10 = shift_sint32(a, i_7) in
-       (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) -> ((a_9[a_10]=true) ->
-       (Init_1[a_10]=true)))).
-  (* Else *)
-  Have: 10 <= i_5.
 }
-Prove: false.
-
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 11) (1/3):
-Prove: true.
+Prove: ((a_3.Init_F1_S_i)=true) /\
+    (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+     ((a_3.Init_F1_S_a)[i_3]=true)))).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 11) (2/3):
-Effect at line 13
+Goal Loop assigns 'CHECK' (1/3):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 11) (3/3):
-Effect at line 13
+Goal Loop assigns 'CHECK' (2/3):
+Effect at line 81
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 17) (1/3):
+Goal Loop assigns 'CHECK' (3/3):
+Effect at line 82
 Prove: true.
 
 ------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 17) (2/3):
-Effect at line 18
-Prove: true.
-
 ------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 17) (3/3):
-Effect at line 19
-Prove: true.
-
+  Function initialize
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 24) (1/2):
-Prove: true.
+Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 16):
+Let m = Init_0[shiftfield_F1_S_i(s) <- true].
+Let a = shiftfield_F1_S_a(s).
+Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Assume {
+  Type: is_sint32(i) /\ is_sint32(1 + i).
+  (* Heap *)
+  Type: region(s.base) <= 0.
+  (* Loop assigns 'CHECK' *)
+  Have: forall i_1 : Z. let a_2 = shift_sint32(a, i_1) in ((0 <= i_1) ->
+      ((i_1 <= 9) -> ((m[a_2]=true) -> (a_1[a_2]=true)))).
+  (* Invariant 'CHECK' *)
+  Have: (0 <= i) /\ (i <= 10) /\
+      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+       (a_1[shift_sint32(a, i_1)]=true)))).
+  (* Then *)
+  Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+    (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+     (a_1[shift_sint32(a, i) <- true][shift_sint32(a, i_1)]=true)))).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 24) (2/2):
-Effect at line 25
+Goal Establishment of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 16):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 33) (1/3):
-Prove: true.
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 21):
+Let m = Init_0[shiftfield_F1_S_i(s) <- true].
+Let a = shiftfield_F1_S_a(s).
+Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_2 = Load_Init_S1_S(s, a_1).
+Assume {
+  Type: is_sint32(i).
+  (* Heap *)
+  Type: region(s.base) <= 0.
+  (* Loop assigns 'CHECK' *)
+  Have: forall i_1 : Z. let a_3 = shift_sint32(a, i_1) in ((0 <= i_1) ->
+      ((i_1 <= 9) -> ((m[a_3]=true) -> (a_1[a_3]=true)))).
+  (* Invariant 'CHECK' *)
+  Have: (0 <= i) /\ (i <= 10) /\
+      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+       (a_1[shift_sint32(a, i_1)]=true)))).
+  (* Else *)
+  Have: 10 <= i.
+}
+Prove: ((a_2.Init_F1_S_i)=true) /\
+    (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
+     ((a_2.Init_F1_S_a)[i_1]=true)))).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 33) (2/3):
-Effect at line 35
+Goal Loop assigns 'CHECK' (1/3):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 33) (3/3):
-Effect at line 36
+Goal Loop assigns 'CHECK' (2/3):
+Effect at line 19
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 41) (1/3):
+Goal Loop assigns 'CHECK' (3/3):
+Effect at line 19
 Prove: true.
 
 ------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 41) (2/3):
-Effect at line 42
-Prove: true.
-
 ------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 41) (3/3):
-Effect at line 43
-Prove: true.
-
+  Function range
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (1/5):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (2/5):
-Effect at line 49
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 36):
+Let m = Init_0[shiftfield_F1_S_i(s) <- true].
 Let a = shiftfield_F1_S_a(s).
-Let a_1 = shiftfield_F1_S_i(s).
-Let m = Init_0[a_1 <- true].
-Let a_2 = shift_sint32(a, 0).
-Let a_3 = havoc(Init_undef_0, m, a_2, 10).
-Let a_4 = shift_sint32(a, 1).
-Let a_5 = havoc(Init_undef_1, a_3, a_4, 4).
-Let a_6 = a_5[a_1 <- true].
-Let a_7 = havoc(Init_undef_2, a_6, a_2, 10).
-Let a_8 = shift_sint32(a, 4).
-Let a_9 = a_7[a_8 <- i_9].
+Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
+Let a_2 = havoc(Init_undef_0, a_1, shift_sint32(a, 1), 4).
+Let a_3 = Load_Init_S1_S(s, a_2).
 Assume {
-  Type: is_sint32(i_2) /\ is_sint32(i_3) /\ is_sint32(i_4) /\
-      is_sint32(i_5) /\ is_sint32(i_6) /\ is_sint32(i_7).
+  Type: is_sint32(i) /\ is_sint32(i_1).
   (* Heap *)
-  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
-  (* Goal *)
-  When: (!invalid(Malloc_0, shift_sint32(a, i_8), 1)) /\
-      ((i_8 = 0) \/ (i_8 = 2) \/ (i_8 = 4)) /\
-      ((i = 0) \/ (i = 2) \/ (i = 4)).
-  (* Loop assigns ... *)
-  Have: forall i_10 : Z. let a_10 = shift_sint32(a, i_10) in ((0 <= i_10) ->
-      ((i_10 <= 9) -> ((m[a_10]=true) -> (a_3[a_10]=true)))).
-  (* Invariant *)
-  Have: forall i_10 : Z. ((0 <= i_10) -> ((i_10 < i_2) ->
-      (a_3[shift_sint32(a, i_10)]=true))).
-  (* Invariant *)
-  Have: (0 <= i_2) /\ (i_2 <= 10).
-  (* Else *)
-  Have: 10 <= i_2.
-  (* Loop assigns ... *)
-  Have: forall i_10 : Z. let a_10 = shift_sint32(a, i_10) in ((0 < i_10) ->
-      ((i_10 <= 4) -> ((a_3[a_10]=true) -> (a_5[a_10]=true)))).
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Else *)
-  Have: 10 <= i_4.
+  Type: region(s.base) <= 0.
   (* Loop assigns ... *)
-  Have: forall i_10 : Z. let a_10 = shift_sint32(a, i_10) in ((0 <= i_10) ->
-      ((i_10 <= 9) -> ((a_6[a_10]=true) -> (a_7[a_10]=true)))).
+  Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+      ((i_2 <= 9) -> ((m[a_4]=true) -> (a_1[a_4]=true)))).
   (* Invariant *)
-  Have: (0 <= i_5) /\ (i_5 <= 10).
+  Have: (0 <= i) /\ (i <= 10) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+       (a_1[shift_sint32(a, i_2)]=true)))).
   (* Else *)
-  Have: 10 <= i_5.
-  (* Loop assigns ... *)
-  Have: ((Init_undef_2[a_8]=true) -> (i_9=true)).
+  Have: 10 <= i.
+  (* Loop assigns 'CHECK' *)
+  Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 < i_2) ->
+      ((i_2 <= 4) -> ((a_1[a_4]=true) -> (a_2[a_4]=true)))).
   (* Else *)
-  Have: 10 <= i_6.
-  (* Loop assigns ... *)
-  Have: (forall a_10 : addr.
-         ((forall i_10 : Z. (((i_10 = 0) \/ (i_10 = 2) \/ (i_10 = 4)) ->
-           (shift_sint32(a, i_10) != a_10))) ->
-         ((a_9[a_10]=true) <-> (Init_1[a_10]=true)))) /\
-      (forall a_10 : addr.
-       ((forall i_10 : Z. (((i_10 = 0) \/ (i_10 = 2) \/ (i_10 = 4)) ->
-         (shift_sint32(a, i_10) != a_10))) ->
-       (havoc(Mint_undef_0,
-          havoc(Mint_undef_1, havoc(Mint_undef_2, Mint_0[a_1 <- 0], a_2, 10),
-            a_4, 4)[a_1 <- v], a_2, 10)[a_8 <- v_1][a_10] = Mint_1[a_10]))) /\
-      (forall i_10 : Z. let a_10 = shift_sint32(a, i_10) in
-       (((i_10 = 0) \/ (i_10 = 2) \/ (i_10 = 4)) -> ((a_9[a_10]=true) ->
-       (Init_1[a_10]=true)))).
-  (* Then *)
-  Have: i_7 <= 9.
+  Have: 10 <= i_1.
 }
-Prove: (i = 0) \/ (i = 2) \/ (i = 4) \/
-    ((i_1 != 0) /\ (i_1 != 2) /\ (i_1 != 4)).
+Prove: ((a_3.Init_F1_S_i)=true) /\
+    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+     ((a_3.Init_F1_S_a)[i_2]=true)))).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (3/5):
-Effect at line 50
+Goal Loop assigns 'CHECK' (1/3):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (4/5):
-Effect at line 50
+Goal Loop assigns 'CHECK' (2/3):
+Effect at line 33
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (5/5):
-Effect at line 50
+Goal Loop assigns 'CHECK' (3/3):
+Effect at line 34
 Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
index ed0a5eb4569f80bd839e7aaa3ad41f000b48ea05..a549395cc4430bff15b37b26a8a62959d5d06c25 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
@@ -4,91 +4,58 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 ------------------------------------------------------------
-  Function main
+  Function array
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 10):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 73):
 Assume {
-  Type: is_sint32(i) /\ is_sint32(1 + i).
-  (* Invariant *)
-  Have: ((0 < i) ->
-      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true))))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Then *)
+  Have: 0 <= i.
   Have: i <= 9.
-}
-Prove: (-1) <= i.
-
-------------------------------------------------------------
-
-Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 10):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 11):
-Assume {
-  Have: i_1 <= i.
-  Have: 0 <= i_1.
-  Type: is_sint32(i) /\ is_sint32(1 + i).
-  (* Goal *)
-  When: 0 <= i.
+  Type: is_sint32(i_1) /\ is_sint32(i_2).
   (* Invariant *)
-  Have: ((0 < i) ->
-      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true))))).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (((0 < i_1) ->
+       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v_1[i_3]=true)))))).
+  (* Else *)
+  Have: 10 <= i_1.
+  (* Loop assigns 'CHECK' *)
+  Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v_1[i_3]=true) ->
+      (v[i_3]=true)))).
   (* Invariant *)
-  Have: i <= 10.
-  (* Then *)
-  Have: i <= 9.
+  Have: (0 <= i_2) /\ (i_2 <= 10).
+  (* Else *)
+  Have: 10 <= i_2.
 }
-Prove: (v[i <- true][i_1]=true).
+Prove: (v[i]=true).
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 11):
+Goal Loop assigns 'CHECK':
 Prove: true.
 
 ------------------------------------------------------------
-
-Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 16):
-Assume {
-  Have: 0 <= i.
-  Have: i <= 9.
-  Type: is_sint32(i_1).
-  (* Invariant *)
-  Have: ((0 < i_1) ->
-      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true))))).
-  (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
-  (* Else *)
-  Have: 10 <= i_1.
-}
-Prove: (v[i]=true).
-
+------------------------------------------------------------
+  Function comp
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 23):
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 125):
 Let a = Init_s_0.Init_F1_S_a.
 Assume {
   Have: 0 <= i.
   Have: i <= 9.
   Type: is_sint32(i_1) /\ is_sint32(i_2).
   (* Invariant *)
-  Have: ((0 < i_1) ->
-      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true))))).
-  (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (((0 < i_1) ->
+       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
   (* Else *)
   Have: 10 <= i_1.
-  (* Loop assigns ... *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
-       (((i_3 <= 0) \/ (5 <= i_3)) -> ((a[i_3]=true) <-> (v[i_3]=true)))))) /\
-      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
-       (((i_3 <= 0) \/ (5 <= i_3)) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))) /\
-      (forall i_3 : Z. ((0 < i_3) -> ((0 <= i_3) -> ((i_3 <= 4) ->
-       ((i_3 <= 9) -> ((v[i_3]=true) -> (a[i_3]=true))))))).
+  (* Loop assigns 'CHECK' *)
+  Have: ((Init_s_0.Init_F1_S_i)=true) /\
+      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v[i_3]=true) ->
+       (a[i_3]=true))))).
+  (* Invariant *)
+  Have: (0 <= i_2) /\ (i_2 <= 10).
   (* Else *)
   Have: 10 <= i_2.
 }
@@ -96,379 +63,237 @@ Prove: (a[i]=true).
 
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 30):
+Goal Loop assigns 'CHECK':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function descr
+------------------------------------------------------------
+
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
 Let a = Init_s_0.Init_F1_S_a.
 Assume {
   Have: 0 <= i.
   Have: i <= 9.
-  Type: is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3).
-  (* Invariant *)
-  Have: ((0 < i_1) ->
-      (forall i_4 : Z. ((0 <= i_4) -> ((i_4 < i_1) -> (v[i_4]=true))))).
+  Type: is_sint32(i_1) /\ is_sint32(i_2).
   (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (((0 < i_1) ->
+       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
   (* Else *)
   Have: 10 <= i_1.
-  (* Loop assigns ... *)
+  (* Loop assigns 'CHECK' *)
   Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
-       (((i_4 <= 0) \/ (5 <= i_4)) -> ((a[i_4]=true) <-> (v[i_4]=true)))))) /\
-      (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
-       (((i_4 <= 0) \/ (5 <= i_4)) -> ((s.F1_S_a)[i_4] = v_1[i_4]))))) /\
-      (forall i_4 : Z. ((0 < i_4) -> ((0 <= i_4) -> ((i_4 <= 4) ->
-       ((i_4 <= 9) -> ((v[i_4]=true) -> (a[i_4]=true))))))).
+      (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
+       ((0 <= i_3) -> ((i_3 <= 9) -> ((a[i_3]=true) <-> (v[i_3]=true)))))))) /\
+      (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
+       ((0 <= i_3) -> ((i_3 <= 9) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))))) /\
+      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v[i_3]=true) ->
+       (((i_3 = 0) \/ (i_3 = 2) \/ (i_3 = 4)) -> (a[i_3]=true)))))).
   (* Else *)
   Have: 10 <= i_2.
-  (* Else *)
-  Have: 10 <= i_3.
 }
 Prove: (a[i]=true).
 
 ------------------------------------------------------------
 
-Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 33):
+Goal Loop assigns 'CHECK' (1/5):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'CHECK' (2/5):
+Effect at line 102
 Let a = Init_s_0.Init_F1_S_a.
 Assume {
-  Type: is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\ is_sint32(i) /\
-      is_sint32(1 + i).
-  (* Invariant *)
-  Have: ((0 < i_1) ->
-      (forall i_4 : Z. ((0 <= i_4) -> ((i_4 < i_1) -> (v[i_4]=true))))).
+  Type: is_sint32(i_2) /\ is_sint32(i_3).
+  (* Goal *)
+  When: (0 <= i_4) /\ (i_4 <= 9) /\ ((i_4 = 0) \/ (i_4 = 2) \/ (i_4 = 4)) /\
+      ((i_1 = 0) \/ (i_1 = 2) \/ (i_1 = 4)).
   (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
-  (* Else *)
-  Have: 10 <= i_1.
-  (* Loop assigns ... *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
-       (((i_4 <= 0) \/ (5 <= i_4)) -> ((a[i_4]=true) <-> (v[i_4]=true)))))) /\
-      (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
-       (((i_4 <= 0) \/ (5 <= i_4)) -> ((s.F1_S_a)[i_4] = v_1[i_4]))))) /\
-      (forall i_4 : Z. ((0 < i_4) -> ((0 <= i_4) -> ((i_4 <= 4) ->
-       ((i_4 <= 9) -> ((v[i_4]=true) -> (a[i_4]=true))))))).
+  Have: (0 <= i_2) /\ (i_2 <= 10) /\
+      (((0 < i_2) ->
+       (forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) -> (v[i_5]=true)))))).
   (* Else *)
   Have: 10 <= i_2.
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) -> ((a[i_4]=true) ->
-      (v_2[i_4]=true)))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
+  (* Loop assigns 'CHECK' *)
+  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
+      (forall i_5 : Z. ((i_5 != 0) -> ((i_5 != 2) -> ((i_5 != 4) ->
+       ((0 <= i_5) -> ((i_5 <= 9) -> ((a[i_5]=true) <-> (v[i_5]=true)))))))) /\
+      (forall i_5 : Z. ((i_5 != 0) -> ((i_5 != 2) -> ((i_5 != 4) ->
+       ((0 <= i_5) -> ((i_5 <= 9) -> ((s.F1_S_a)[i_5] = v_1[i_5]))))))) /\
+      (forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) -> ((v[i_5]=true) ->
+       (((i_5 = 0) \/ (i_5 = 2) \/ (i_5 = 4)) -> (a[i_5]=true)))))).
   (* Then *)
-  Have: i <= 9.
+  Have: i_3 <= 9.
 }
-Prove: (-1) <= i.
+Prove: ((i != 0) /\ (i != 2) /\ (i != 4)) \/
+    (exists i_5 : Z. (i_5 <= i_1) /\ (i_1 <= i_5) /\
+     ((i_5 = 0) \/ (i_5 = 2) \/ (i_5 = 4))).
 
 ------------------------------------------------------------
 
-Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 33):
+Goal Loop assigns 'CHECK' (3/5):
+Effect at line 103
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 40):
-Let a = Init_s_0.Init_F1_S_a.
-Assume {
-  Have: 0 <= i.
-  Have: i <= 9.
-  Type: is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\ is_sint32(i_4).
-  (* Invariant *)
-  Have: ((0 < i_1) ->
-      (forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_1) -> (v_1[i_5]=true))))).
-  (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
-  (* Else *)
-  Have: 10 <= i_1.
-  (* Loop assigns ... *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
-       (((i_5 <= 0) \/ (5 <= i_5)) -> ((a[i_5]=true) <-> (v_1[i_5]=true)))))) /\
-      (forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
-       (((i_5 <= 0) \/ (5 <= i_5)) -> ((s.F1_S_a)[i_5] = v_2[i_5]))))) /\
-      (forall i_5 : Z. ((0 < i_5) -> ((0 <= i_5) -> ((i_5 <= 4) ->
-       ((i_5 <= 9) -> ((v_1[i_5]=true) -> (a[i_5]=true))))))).
-  (* Else *)
-  Have: 10 <= i_2.
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) -> ((a[i_5]=true) ->
-      (v[i_5]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_4) /\ (i_4 <= 10).
-  (* Else *)
-  Have: 10 <= i_4.
-}
-Prove: (v[i]=true).
+Goal Loop assigns 'CHECK' (4/5):
+Effect at line 103
+Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 47):
-Let a = Init_s_0.Init_F1_S_a.
-Assume {
-  Have: 0 <= i.
-  Have: i <= 9.
-  Type: is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
-      is_sint32(i_4) /\ is_sint32(i_5).
-  (* Invariant *)
-  Have: ((0 < i_1) ->
-      (forall i_6 : Z. ((0 <= i_6) -> ((i_6 < i_1) -> (v_2[i_6]=true))))).
-  (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
-  (* Else *)
-  Have: 10 <= i_1.
-  (* Loop assigns ... *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
-       (((i_6 <= 0) \/ (5 <= i_6)) -> ((a[i_6]=true) <-> (v_2[i_6]=true)))))) /\
-      (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
-       (((i_6 <= 0) \/ (5 <= i_6)) -> ((s.F1_S_a)[i_6] = v_3[i_6]))))) /\
-      (forall i_6 : Z. ((0 < i_6) -> ((0 <= i_6) -> ((i_6 <= 4) ->
-       ((i_6 <= 9) -> ((v_2[i_6]=true) -> (a[i_6]=true))))))).
-  (* Else *)
-  Have: 10 <= i_2.
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((a[i_6]=true) ->
-      (v[i_6]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_4) /\ (i_4 <= 10).
-  (* Else *)
-  Have: 10 <= i_4.
-  (* Loop assigns ... *)
-  Have: ((v[4]=true) -> (v_1=true)).
-  (* Else *)
-  Have: 10 <= i_5.
-}
-Prove: (v[4 <- v_1][i]=true).
+Goal Loop assigns 'CHECK' (5/5):
+Effect at line 103
+Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function field
+------------------------------------------------------------
 
-Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 54):
-Let a = Init_s_0.Init_F1_S_a.
-Let m = v_2[4 <- v_3].
-Let a_1 = Init_s_1.Init_F1_S_a.
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 54):
 Assume {
   Have: 0 <= i.
   Have: i <= 9.
-  Type: is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
-      is_sint32(i_4) /\ is_sint32(i_5) /\ is_sint32(i_6).
-  (* Invariant *)
-  Have: ((0 < i_1) ->
-      (forall i_7 : Z. ((0 <= i_7) -> ((i_7 < i_1) -> (v[i_7]=true))))).
+  Type: is_sint32(i_1) /\ is_sint32(i_2).
   (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (((0 < i_1) ->
+       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
   (* Else *)
   Have: 10 <= i_1.
-  (* Loop assigns ... *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_1.Init_F1_S_i)=true) /\
-      (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
-       (((i_7 <= 0) \/ (5 <= i_7)) -> ((a_1[i_7]=true) <-> (v[i_7]=true)))))) /\
-      (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
-       (((i_7 <= 0) \/ (5 <= i_7)) -> ((s.F1_S_a)[i_7] = v_1[i_7]))))) /\
-      (forall i_7 : Z. ((0 < i_7) -> ((0 <= i_7) -> ((i_7 <= 4) ->
-       ((i_7 <= 9) -> ((v[i_7]=true) -> (a_1[i_7]=true))))))).
   (* Else *)
   Have: 10 <= i_2.
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) -> ((a_1[i_7]=true) ->
-      (v_2[i_7]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_4) /\ (i_4 <= 10).
-  (* Else *)
-  Have: 10 <= i_4.
-  (* Loop assigns ... *)
-  Have: ((v_2[4]=true) -> (v_3=true)).
-  (* Else *)
-  Have: 10 <= i_5.
-  (* Loop assigns ... *)
-  Have: ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_7 : Z. ((i_7 != 0) -> ((i_7 != 2) -> ((i_7 != 4) ->
-       ((0 <= i_7) -> ((i_7 <= 9) -> ((a[i_7]=true) <-> (m[i_7]=true)))))))) /\
-      (forall i_7 : Z. ((i_7 != 0) -> ((i_7 != 2) -> ((i_7 != 4) ->
-       ((0 <= i_7) -> ((i_7 <= 9) ->
-       ((s_1.F1_S_a)[i_7] = v_4[4 <- v_5][i_7]))))))) /\
-      (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) -> ((m[i_7]=true) ->
-       (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) -> (a[i_7]=true)))))).
-  (* Else *)
-  Have: 10 <= i_6.
 }
-Prove: (a[i]=true).
+Prove: (v[i]=true).
+
+------------------------------------------------------------
+
+Goal Loop assigns 'CHECK':
+Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function index
+------------------------------------------------------------
 
-Goal Check 'SMOKE' (file tests/wp_acsl/assigned_initialized_memvar.i, line 55):
-Let a = Init_s_1.Init_F1_S_a.
-Let m = v_2[4 <- v_3].
-Let a_1 = Init_s_0.Init_F1_S_a.
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 89):
 Assume {
-  Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
-      is_sint32(i_4) /\ is_sint32(i_5).
-  (* Invariant *)
-  Have: ((0 < i) ->
-      (forall i_6 : Z. ((0 <= i_6) -> ((i_6 < i) -> (v[i_6]=true))))).
+  Have: 0 <= i.
+  Have: i <= 9.
+  Type: is_sint32(i_1) /\ is_sint32(i_2).
   (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Else *)
-  Have: 10 <= i.
-  (* Loop assigns ... *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
-       (((i_6 <= 0) \/ (5 <= i_6)) -> ((a_1[i_6]=true) <-> (v[i_6]=true)))))) /\
-      (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
-       (((i_6 <= 0) \/ (5 <= i_6)) -> ((s.F1_S_a)[i_6] = v_1[i_6]))))) /\
-      (forall i_6 : Z. ((0 < i_6) -> ((0 <= i_6) -> ((i_6 <= 4) ->
-       ((i_6 <= 9) -> ((v[i_6]=true) -> (a_1[i_6]=true))))))).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (((0 < i_1) ->
+       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
   (* Else *)
   Have: 10 <= i_1.
+  (* Loop assigns 'CHECK' *)
+  Have: ((v[4]=true) -> (v_1=true)).
   (* Else *)
   Have: 10 <= i_2.
-  (* Loop assigns ... *)
-  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((a_1[i_6]=true) ->
-      (v_2[i_6]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_3) /\ (i_3 <= 10).
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Loop assigns ... *)
-  Have: ((v_2[4]=true) -> (v_3=true)).
-  (* Else *)
-  Have: 10 <= i_4.
-  (* Loop assigns ... *)
-  Have: ((Init_s_1.Init_F1_S_i)=true) /\
-      (forall i_6 : Z. ((i_6 != 0) -> ((i_6 != 2) -> ((i_6 != 4) ->
-       ((0 <= i_6) -> ((i_6 <= 9) -> ((a[i_6]=true) <-> (m[i_6]=true)))))))) /\
-      (forall i_6 : Z. ((i_6 != 0) -> ((i_6 != 2) -> ((i_6 != 4) ->
-       ((0 <= i_6) -> ((i_6 <= 9) ->
-       ((s_1.F1_S_a)[i_6] = v_4[4 <- v_5][i_6]))))))) /\
-      (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((m[i_6]=true) ->
-       (((i_6 = 0) \/ (i_6 = 2) \/ (i_6 = 4)) -> (a[i_6]=true)))))).
-  (* Else *)
-  Have: 10 <= i_5.
 }
-Prove: false.
+Prove: (v[4 <- v_1][i]=true).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 12):
+Goal Loop assigns 'CHECK' (1/2):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 18) (1/2):
+Goal Loop assigns 'CHECK' (2/2):
+Effect at line 87
 Prove: true.
 
 ------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 18) (2/2):
-Effect at line 20
-Prove: true.
-
 ------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 25):
-Prove: true.
-
+  Function initialize
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 34):
-Prove: true.
+Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 17):
+Assume {
+  Type: is_sint32(i) /\ is_sint32(1 + i).
+  (* Invariant 'CHECK' *)
+  Have: (0 <= i) /\ (i <= 10) /\
+      (((0 < i) ->
+       (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
+  (* Then *)
+  Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+    (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+     (v[i <- true][i_1]=true)))).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 42) (1/2):
+Goal Establishment of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 17):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 42) (2/2):
-Effect at line 44
-Prove: true.
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 22):
+Assume {
+  Have: 0 <= i.
+  Have: i <= 9.
+  Type: is_sint32(i_1).
+  (* Invariant 'CHECK' *)
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (((0 < i_1) ->
+       (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
+  (* Else *)
+  Have: 10 <= i_1.
+}
+Prove: (v[i]=true).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (1/5):
+Goal Loop assigns 'CHECK':
 Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function range
+------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (2/5):
-Effect at line 50
-Let a = Init_s_1.Init_F1_S_a.
-Let m = v_2[4 <- v_3].
-Let a_1 = Init_s_0.Init_F1_S_a.
+Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 38):
+Let a = Init_s_0.Init_F1_S_a.
 Assume {
-  Type: is_sint32(i_2) /\ is_sint32(i_3) /\ is_sint32(i_4) /\
-      is_sint32(i_5) /\ is_sint32(i_6) /\ is_sint32(i_7).
-  (* Goal *)
-  When: (0 <= i_8) /\ (i_8 <= 9) /\ ((i_8 = 0) \/ (i_8 = 2) \/ (i_8 = 4)) /\
-      ((i_1 = 0) \/ (i_1 = 2) \/ (i_1 = 4)).
-  (* Invariant *)
-  Have: ((0 < i_2) ->
-      (forall i_9 : Z. ((0 <= i_9) -> ((i_9 < i_2) -> (v[i_9]=true))))).
+  Have: 0 <= i.
+  Have: i <= 9.
+  Type: is_sint32(i_1) /\ is_sint32(i_2).
   (* Invariant *)
-  Have: (0 <= i_2) /\ (i_2 <= 10).
+  Have: (0 <= i_1) /\ (i_1 <= 10) /\
+      (((0 < i_1) ->
+       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
   (* Else *)
-  Have: 10 <= i_2.
-  (* Loop assigns ... *)
+  Have: 10 <= i_1.
+  (* Loop assigns 'CHECK' *)
   Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) ->
-       (((i_9 <= 0) \/ (5 <= i_9)) -> ((a_1[i_9]=true) <-> (v[i_9]=true)))))) /\
-      (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) ->
-       (((i_9 <= 0) \/ (5 <= i_9)) -> ((s.F1_S_a)[i_9] = v_1[i_9]))))) /\
-      (forall i_9 : Z. ((0 < i_9) -> ((0 <= i_9) -> ((i_9 <= 4) ->
-       ((i_9 <= 9) -> ((v[i_9]=true) -> (a_1[i_9]=true))))))).
-  (* Else *)
-  Have: 10 <= i_3.
-  (* Else *)
-  Have: 10 <= i_4.
-  (* Loop assigns ... *)
-  Have: forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((a_1[i_9]=true) ->
-      (v_2[i_9]=true)))).
-  (* Invariant *)
-  Have: (0 <= i_5) /\ (i_5 <= 10).
-  (* Else *)
-  Have: 10 <= i_5.
-  (* Loop assigns ... *)
-  Have: ((v_2[4]=true) -> (v_3=true)).
+      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+       (((i_3 <= 0) \/ (5 <= i_3)) -> ((a[i_3]=true) <-> (v[i_3]=true)))))) /\
+      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+       (((i_3 <= 0) \/ (5 <= i_3)) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))) /\
+      (forall i_3 : Z. ((0 < i_3) -> ((0 <= i_3) -> ((i_3 <= 4) ->
+       ((i_3 <= 9) -> ((v[i_3]=true) -> (a[i_3]=true))))))).
   (* Else *)
-  Have: 10 <= i_6.
-  (* Loop assigns ... *)
-  Have: ((Init_s_1.Init_F1_S_i)=true) /\
-      (forall i_9 : Z. ((i_9 != 0) -> ((i_9 != 2) -> ((i_9 != 4) ->
-       ((0 <= i_9) -> ((i_9 <= 9) -> ((a[i_9]=true) <-> (m[i_9]=true)))))))) /\
-      (forall i_9 : Z. ((i_9 != 0) -> ((i_9 != 2) -> ((i_9 != 4) ->
-       ((0 <= i_9) -> ((i_9 <= 9) ->
-       ((s_1.F1_S_a)[i_9] = v_4[4 <- v_5][i_9]))))))) /\
-      (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((m[i_9]=true) ->
-       (((i_9 = 0) \/ (i_9 = 2) \/ (i_9 = 4)) -> (a[i_9]=true)))))).
-  (* Then *)
-  Have: i_7 <= 9.
+  Have: 10 <= i_2.
 }
-Prove: ((i != 0) /\ (i != 2) /\ (i != 4)) \/
-    (exists i_9 : Z. (i_9 <= i_1) /\ (i_1 <= i_9) /\
-     ((i_9 = 0) \/ (i_9 = 2) \/ (i_9 = 4))).
-
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (3/5):
-Effect at line 51
-Prove: true.
+Prove: (a[i]=true).
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (4/5):
-Effect at line 51
+Goal Loop assigns 'CHECK' (1/2):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (5/5):
-Effect at line 51
+Goal Loop assigns 'CHECK' (2/2):
+Effect at line 36
 Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/052040e80d2b0a66ce3f375f87b6ff42.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/052040e80d2b0a66ce3f375f87b6ff42.json
deleted file mode 100644
index b8e36e2803fcc35bf7625695f4ebcfc62989c064..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/052040e80d2b0a66ce3f375f87b6ff42.json
+++ /dev/null
@@ -1 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0a455ba1935274c35611d5fdf0fc2f8f.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0a455ba1935274c35611d5fdf0fc2f8f.json
deleted file mode 100644
index 9125f6b41d6f85c5c09a01c4ce601217fbea99c9..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0a455ba1935274c35611d5fdf0fc2f8f.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0127,
-  "steps": 32 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/1f0cf3c12d6f9cc69fd1da4055c79d9b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/1f0cf3c12d6f9cc69fd1da4055c79d9b.json
new file mode 100644
index 0000000000000000000000000000000000000000..502a5a6726f3d706a21759996c5f19f4706c1cc1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/1f0cf3c12d6f9cc69fd1da4055c79d9b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0165,
+  "steps": 66 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/3663b5118c844863a6d247b05714c0ce.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/3663b5118c844863a6d247b05714c0ce.json
new file mode 100644
index 0000000000000000000000000000000000000000..bfc7218d01d9d7134b26d9d28d5a3fbd9ff2b22d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/3663b5118c844863a6d247b05714c0ce.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0078,
+  "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/46d8e3b4a96b7cde8b04fa3be200b8a8.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/46d8e3b4a96b7cde8b04fa3be200b8a8.json
new file mode 100644
index 0000000000000000000000000000000000000000..5e2ba964b607098157b5f7770195d847928ae929
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/46d8e3b4a96b7cde8b04fa3be200b8a8.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0247,
+  "steps": 90 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5638c5e45ea8450040bc5a67415363a5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5638c5e45ea8450040bc5a67415363a5.json
deleted file mode 100644
index fc60b98b9e002045a095ef5326ea9b0a2d1fe575..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5638c5e45ea8450040bc5a67415363a5.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.249,
-  "steps": 550 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5651f36fea599e9ff5d67e9df8679972.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5651f36fea599e9ff5d67e9df8679972.json
deleted file mode 100644
index 29e4ca835905de63d07c3980f02885158b984d15..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5651f36fea599e9ff5d67e9df8679972.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0086,
-  "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/84ac30ceabf40ae460d3a6638be6ea4d.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/84ac30ceabf40ae460d3a6638be6ea4d.json
index c0b0613e97a7c4900c15cfb5db9efd479e85bb6b..aa69f984d404403b79912866dc7dde4df7666d7c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/84ac30ceabf40ae460d3a6638be6ea4d.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/84ac30ceabf40ae460d3a6638be6ea4d.json
@@ -1,2 +1,2 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0385,
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0365,
   "steps": 190 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/945f495a93303995087d23241c179c2f.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/945f495a93303995087d23241c179c2f.json
deleted file mode 100644
index 24271896cafb873a9ac2c20b81e2c5e66f103fc1..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/945f495a93303995087d23241c179c2f.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.049,
-  "steps": 153 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/95004af59474d658afa48c1fddcc4b38.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/95004af59474d658afa48c1fddcc4b38.json
deleted file mode 100644
index e0c1ac6b238a9f36c34e4f2133c9c5c68633eee7..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/95004af59474d658afa48c1fddcc4b38.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1454,
-  "steps": 321 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/afc7b014ce6a006d5c920be6c963bab6.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/afc7b014ce6a006d5c920be6c963bab6.json
new file mode 100644
index 0000000000000000000000000000000000000000..2d135b932262eac686db74e68bedbba1dde0980a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/afc7b014ce6a006d5c920be6c963bab6.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+  "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b8ca0e444c91c4ef4790a8775a3da864.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b8ca0e444c91c4ef4790a8775a3da864.json
deleted file mode 100644
index 0b5ca39ac99b3118433d8908822190ef6e3ea8e5..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b8ca0e444c91c4ef4790a8775a3da864.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0672,
-  "steps": 147 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b9b74fb903d3948de1f1284737fcc1b4.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b9b74fb903d3948de1f1284737fcc1b4.json
deleted file mode 100644
index 80d093eb059e04b8babcaaf8f01b0e8ff417b5de..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b9b74fb903d3948de1f1284737fcc1b4.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0097,
-  "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/bdce48a1a69da57c8397d85bcbd98c2c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/bdce48a1a69da57c8397d85bcbd98c2c.json
new file mode 100644
index 0000000000000000000000000000000000000000..e60f40f1ec46178c38a2c5cab25567c2859b6990
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/bdce48a1a69da57c8397d85bcbd98c2c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0093,
+  "steps": 31 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/c10d834a86946a7d1b5074a8355dfd03.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/c10d834a86946a7d1b5074a8355dfd03.json
new file mode 100644
index 0000000000000000000000000000000000000000..9df9b2eaddd59d31e4f17f731a4d3b294e765d6a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/c10d834a86946a7d1b5074a8355dfd03.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0182,
+  "steps": 74 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/d6725ba9afba4fa566a3d7e0f0b0925e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/d6725ba9afba4fa566a3d7e0f0b0925e.json
new file mode 100644
index 0000000000000000000000000000000000000000..0db2f6426cebdfe71e0e3aed538846daa0587886
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/d6725ba9afba4fa566a3d7e0f0b0925e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.024,
+  "steps": 120 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/df1b1f99fbd7c697efdffd3389b62ba3.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/df1b1f99fbd7c697efdffd3389b62ba3.json
index 9fbe0e773195d3d1a78dd26470be3048bc22ce1a..2f019245a619324e5a1ba5e8bc28d86dfbd7fe68 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/df1b1f99fbd7c697efdffd3389b62ba3.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/df1b1f99fbd7c697efdffd3389b62ba3.json
@@ -1,2 +1,2 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0146,
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0226,
   "steps": 66 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/e4f6b760b38c0d0d9e14569809271d9f.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/e4f6b760b38c0d0d9e14569809271d9f.json
deleted file mode 100644
index 627150223b0a45b795051db34423bf4232e3377f..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/e4f6b760b38c0d0d9e14569809271d9f.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.005,
-  "steps": 14 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/fd966dcda2718c7b28f5491d99ce724d.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/fd966dcda2718c7b28f5491d99ce724d.json
new file mode 100644
index 0000000000000000000000000000000000000000..02f068903adda07a7e45312f3246e693d6919423
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/fd966dcda2718c7b28f5491d99ce724d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0226,
+  "steps": 108 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
index 290341bb6702a6d5fd4139067d6b63dbdf1e9291..1bde0d25a862104f5b8142f86c31c1c369c4c284 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
@@ -3,43 +3,48 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
-[wp] 32 goals scheduled
-[wp] [Alt-Ergo] Goal typed_main_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_main_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_main_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_main_loop_invariant_2_established : Valid
-[wp] [Alt-Ergo] Goal typed_main_check : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_2 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_3 : Valid
-[wp] [Alt-Ergo] Goal typed_main_loop_invariant_3_preserved : Valid
-[wp] [Qed] Goal typed_main_loop_invariant_3_established : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_4 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_5 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_6 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_SMOKE : Unsuccess
-[wp] [Qed] Goal typed_main_loop_assigns_part1 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_part3 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_2_part1 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_2_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_2_part3 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_3_part1 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_3_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_4_part1 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_4_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_4_part3 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_5_part1 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_5_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_5_part3 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_main_loop_assigns_6_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part3 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part4 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part5 : Valid
-[wp] Proved goals:   31 / 32
+[wp] 31 goals scheduled
+[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
+[wp] [Qed] Goal typed_array_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_array_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_array_loop_assigns_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
+[wp] [Qed] Goal typed_comp_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_comp_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_comp_loop_assigns_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part4 : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
+[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
+[wp] [Qed] Goal typed_field_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_field_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
+[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_index_loop_assigns_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_initialize_loop_invariant_CHECK_preserved : Valid
+[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
+[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
+[wp] [Qed] Goal typed_initialize_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_initialize_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_initialize_loop_assigns_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
+[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_range_loop_assigns_part3 : Valid
+[wp] Proved goals:   31 / 31
   Qed:            21 
-  Alt-Ergo:       10  (unsuccess: 1)
+  Alt-Ergo:       10
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  main                     21       10       32      96.9%
+  initialize                4        2        6       100%
+  range                     3        1        4       100%
+  field                     2        1        3       100%
+  array                     3        1        4       100%
+  index                     3        1        4       100%
+  descr                     4        2        6       100%
+  comp                      2        2        4       100%
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json
index ea3a6ca498de1a84eaa7034a7a233f7b9d49a99b..85457ede2a164cbece6157bf7d10fb0a74f439ac 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json
@@ -1,2 +1,2 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0065,
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0056,
   "steps": 13 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/16b1ffeb650eff31ca67078e2b2b9d2a.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/16b1ffeb650eff31ca67078e2b2b9d2a.json
new file mode 100644
index 0000000000000000000000000000000000000000..c819ca8e5167391d4b7b017cf8030830b707fd2c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/16b1ffeb650eff31ca67078e2b2b9d2a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0016,
+  "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/22fb5b9d2061ff10c69cfd7b3caaa4fa.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/22fb5b9d2061ff10c69cfd7b3caaa4fa.json
new file mode 100644
index 0000000000000000000000000000000000000000..c91fca52c67a54258b2d0d4da6aefff4c485a855
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/22fb5b9d2061ff10c69cfd7b3caaa4fa.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+  "steps": 41 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/24dfaa29dea1b41ec3b7520a3e9fef5a.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/24dfaa29dea1b41ec3b7520a3e9fef5a.json
new file mode 100644
index 0000000000000000000000000000000000000000..8efc904030b04408fa0470874a7a47c85f655fc9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/24dfaa29dea1b41ec3b7520a3e9fef5a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0057,
+  "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/2ff76ae8947b7c9d0efda0d01090aeec.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/2ff76ae8947b7c9d0efda0d01090aeec.json
deleted file mode 100644
index 5b4e2cd33790209667a0dd8b4545a50dddf1804a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/2ff76ae8947b7c9d0efda0d01090aeec.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0107,
-  "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json
index d542926cdcc6739d3ae09b367396afb506ce3c94..d667555c447d7687b24ee65ed7807c39eab63db7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json
@@ -1,2 +1,2 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0072,
   "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/3d3436a5d8286651f426c8c10c38b0df.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/3d3436a5d8286651f426c8c10c38b0df.json
new file mode 100644
index 0000000000000000000000000000000000000000..b2fc0a48478629d895a080d074776c51c130c133
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/3d3436a5d8286651f426c8c10c38b0df.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0034,
+  "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/48c345fb8ef6505124dadd81cfdffa01.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/48c345fb8ef6505124dadd81cfdffa01.json
new file mode 100644
index 0000000000000000000000000000000000000000..7ec494e485b62acc9c1d98a1adcca01fb33f3311
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/48c345fb8ef6505124dadd81cfdffa01.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0059,
+  "steps": 16 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/7790b93ea943473c622f27192935dc0e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/7790b93ea943473c622f27192935dc0e.json
deleted file mode 100644
index 91964651c8db76b8c2cc405d17deea035c5f7966..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/7790b93ea943473c622f27192935dc0e.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0227,
-  "steps": 94 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/86af4cc180f45c49dd87882bd812e6de.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/86af4cc180f45c49dd87882bd812e6de.json
new file mode 100644
index 0000000000000000000000000000000000000000..d02f4d3e05750d443600cb8e8ea27c49fc096779
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/86af4cc180f45c49dd87882bd812e6de.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0048,
+  "steps": 15 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/9fc719583241f8c265dc2b57924b4e5c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/9fc719583241f8c265dc2b57924b4e5c.json
deleted file mode 100644
index a445667f615b52816e63b3abbf0a525df2cb3b9d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/9fc719583241f8c265dc2b57924b4e5c.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0091,
-  "steps": 42 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json
deleted file mode 100644
index c5053a8333f4df66b12a61cc6c2c78562e0ab815..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0072,
-  "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/cb1d16f7fccc06c0aca70c20a5f04c82.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/cb1d16f7fccc06c0aca70c20a5f04c82.json
new file mode 100644
index 0000000000000000000000000000000000000000..a159364080a4c75ced21ce2a403dd7f074691b33
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/cb1d16f7fccc06c0aca70c20a5f04c82.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0048,
+  "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ed2046f443d594d7a695098d6732bd53.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ed2046f443d594d7a695098d6732bd53.json
deleted file mode 100644
index b8e36e2803fcc35bf7625695f4ebcfc62989c064..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ed2046f443d594d7a695098d6732bd53.json
+++ /dev/null
@@ -1 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f65786f87e448872f8395e84331fc2fa.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f65786f87e448872f8395e84331fc2fa.json
deleted file mode 100644
index 94e34ea6e492abe1ebc7bab2d19383b0ee9ce04f..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f65786f87e448872f8395e84331fc2fa.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0077,
-  "steps": 33 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json
deleted file mode 100644
index 0f8cdb45879194dbd98a3323504e3308c5b57504..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0046,
-  "steps": 11 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f84e2f80d92f69c9bae45d521a10486b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f84e2f80d92f69c9bae45d521a10486b.json
deleted file mode 100644
index 152e6b163fbafb5164f9c9e9008edbb910a874d5..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f84e2f80d92f69c9bae45d521a10486b.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0018,
-  "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fe9862be590507dedbd24e64a535ac03.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fe9862be590507dedbd24e64a535ac03.json
deleted file mode 100644
index c4f419fb7917a2d4f6a311c33145566ce3ed1f52..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fe9862be590507dedbd24e64a535ac03.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0087,
-  "steps": 39 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index 5184840f613aaecc5cfdbbd139e082f8ed438e5f..45f96059729f403bf623e724e9e3b002964abac5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -3,36 +3,39 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
-[wp] 25 goals scheduled
-[wp] [Alt-Ergo] Goal typed_main_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_main_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_main_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_main_loop_invariant_2_established : Valid
-[wp] [Alt-Ergo] Goal typed_main_check : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_2 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_3 : Valid
-[wp] [Alt-Ergo] Goal typed_main_loop_invariant_3_preserved : Valid
-[wp] [Qed] Goal typed_main_loop_invariant_3_established : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_4 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_5 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_6 : Valid
-[wp] [Alt-Ergo] Goal typed_main_check_SMOKE : Unsuccess
-[wp] [Qed] Goal typed_main_loop_assigns : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_2_part1 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_2_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_3 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_4 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_5_part1 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_5_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_main_loop_assigns_6_part2 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part3 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part4 : Valid
-[wp] [Qed] Goal typed_main_loop_assigns_6_part5 : Valid
-[wp] Proved goals:   24 / 25
-  Qed:            14 
-  Alt-Ergo:       10  (unsuccess: 1)
+[wp] 22 goals scheduled
+[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
+[wp] [Qed] Goal typed_array_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
+[wp] [Qed] Goal typed_comp_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part4 : Valid
+[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
+[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
+[wp] [Qed] Goal typed_field_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
+[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_initialize_loop_invariant_CHECK_preserved : Valid
+[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
+[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
+[wp] [Qed] Goal typed_initialize_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
+[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
+[wp] Proved goals:   22 / 22
+  Qed:            13 
+  Alt-Ergo:        9
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  main                     14       10       25      96.0%
+  initialize                2        2        4       100%
+  range                     2        1        3       100%
+  field                     1        1        2       100%
+  array                     1        1        2       100%
+  index                     2        1        3       100%
+  descr                     4        2        6       100%
+  comp                      1        1        2       100%
 ------------------------------------------------------------