diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
new file mode 100644
index 0000000000000000000000000000000000000000..877f61f698c7c5491b55d89680f8988a74b1a58e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
@@ -0,0 +1,56 @@
+struct S {
+  int i ;
+  int a[10] ;
+};
+
+int main(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];
+  */
+  for(int i = 0; i < 10; ++i) s->a[i] = 0;
+
+  //@ check \initialized(s);
+  
+  /*@ loop assigns i, s->a[1 .. 4]; */
+  for(int i = 0; i < 10; ++i){
+    if(1 <= i && i <= 4) s->a[i] = 1 ;
+  }
+
+  //@ check \initialized(s);
+  
+  /*@ loop assigns i, s->i; */
+  for(int i = 0; i < 10; ++i){
+    s->i++;
+  }
+
+  //@ check \initialized(s);
+  
+  /*@ 
+    loop invariant 0 <= i <= 10;
+    loop assigns i, s->a[0..9]; 
+  */
+  for(int i = 0; i < 10; ++i){
+    s->a[i] = 1 ;
+  }
+
+  //@ check \initialized(s);
+  
+  /*@ loop assigns i, s->a[4]; */
+  for(int i = 0; i < 10; ++i){
+    if(i == 4) s->a[i] = 1 ;
+  }
+
+  //@ check \initialized(s);
+  
+  /*@ loop assigns 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;
+}
+
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
new file mode 100644
index 0000000000000000000000000000000000000000..72dcc1acd7a5f2d7c35b82bc0186f112698ecf04
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
@@ -0,0 +1,57 @@
+struct S {
+  int i ;
+  int a[10] ;
+};
+
+int main(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];
+  */
+  for(int i = 0; i < 10; ++i) s.a[i] = 0;
+
+  //@ check \initialized(&s);
+
+  /*@ loop assigns i, s.a[1 .. 4]; */
+  for(int i = 0; i < 10; ++i){
+    if(1 <= i && i <= 4) s.a[i] = 1 ;
+  }
+
+  //@ check \initialized(&s);
+  
+  /*@ loop assigns i, s.i; */
+  for(int i = 0; i < 10; ++i){
+    s.i++;
+  }
+
+  //@ check \initialized(&s);
+  
+  /*@ 
+    loop invariant 0 <= i <= 10;
+    loop assigns i, s.a[0..9]; 
+  */
+  for(int i = 0; i < 10; ++i){
+    s.a[i] = 1 ;
+  }
+
+  //@ check \initialized(&s);
+
+  /*@ loop assigns i, s.a[4]; */
+  for(int i = 0; i < 10; ++i){
+    if(i == 4) s.a[i] = 1 ;
+  }
+
+  //@ check \initialized(&s);
+
+  /*@ loop assigns 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;
+}
+
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
new file mode 100644
index 0000000000000000000000000000000000000000..76148a465d89b0644d34c616c5f9ef8ad6501c4f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
@@ -0,0 +1,51 @@
+struct S {
+  int x ;
+  int y ;
+} ;
+struct C {
+  int x ;
+  struct S s ;
+  int a[10] ;
+} ;
+
+void test(int* x, int (*a)[2], struct C* c){
+  //@ check unknown: \initialized(x);
+  //@ check unknown: \initialized(a);
+  //@ check unknown: \initialized(c);
+
+  *x = 1 ;
+  //@ check qed_ok: \initialized(x);
+
+  (*a)[0] = 1 ;
+  //@ check qed_ok: \initialized(&(*a)[0]);
+  //@ check unknown: \initialized(&(*a)[1]);
+  //@ check unknown: \initialized(&(*a));
+
+  (*a)[1] = 2 ;
+  //@ check qed_ok: \initialized(&(*a)[0]);
+  //@ check qed_ok: \initialized(&(*a)[1]);
+  //@ check qed_ok: \initialized(&a);
+
+  c->x = 1 ;
+  //@ check qed_ok: \initialized(&c->x);
+  //@ check unknown: \initialized(&c->s);
+  //@ check unknown: \initialized(&c->a);
+  //@ check unknown: \initialized(c);
+
+  c->s.x = 1;
+  //@ check qed_ok: \initialized(&c->s.x);
+  //@ check unknown: \initialized(&c->s.y);
+  //@ check unknown: \initialized(&c->s);
+  //@ check unknown: \initialized(c);
+
+  c->s.y = 1 ;
+  //@ check provable: \initialized(&c->s);
+  //@ check unknown: \initialized(c);
+
+  c->a[0] = c->a[1] = c->a[2] = c->a[3] = c->a[4] = c->a[5] = c->a[6] = c->a[7] = c->a[8] = 1;
+  //@ check provable: \initialized(&c->a[0..8]) ;
+  //@ check unknown: \initialized(c);
+
+  c->a[9] = 1 ;
+  //@ check provable: \initialized(c);
+}
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
new file mode 100644
index 0000000000000000000000000000000000000000..468f735b1db1917594a335ab0f1de83ac7eb77fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
@@ -0,0 +1,612 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 9):
+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 ... *)
+  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 *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+      (a_1[shift_sint32(a, i_1)]=true))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* Then *)
+  Have: i <= 9.
+}
+Prove: (-1) <= i.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 9):
+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 Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 10):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 15):
+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 ... *)
+  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))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* 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 Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 22):
+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).
+Assume {
+  Type: is_sint32(i) /\ is_sint32(i_1).
+  (* Heap *)
+  Type: region(s.base) <= 0.
+  (* 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)))).
+  (* Else *)
+  Have: 10 <= i_1.
+}
+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 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]).
+Assume {
+  Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2).
+  (* 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))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* 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)))).
+  (* 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)))).
+
+------------------------------------------------------------
+
+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).
+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).
+  (* Heap *)
+  Type: region(s.base) <= 0.
+  (* 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))).
+  (* 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)))).
+  (* 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).
+  (* Then *)
+  Have: i <= 9.
+}
+Prove: (-1) <= i.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memtyped.i, line 32):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/assigned_initialized_memtyped.i, line 39):
+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).
+Assume {
+  Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3).
+  (* 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))).
+  (* Invariant *)
+  Have: (0 <= i) /\ (i <= 10).
+  (* 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)))).
+
+------------------------------------------------------------
+
+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 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 Check 'SMOKE' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 54):
+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].
+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_10 = shift_sint32(a, i_7) in ((0 <= i_7) ->
+      ((i_7 <= 9) -> ((m[a_10]=true) -> (a_3[a_10]=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)))).
+  (* Else *)
+  Have: 10 <= i_1.
+  (* 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.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 11) (2/3):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 11) (3/3):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 17) (1/3):
+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.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 24) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 24) (2/2):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 33) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 33) (2/3):
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 33) (3/3):
+Effect at line 36
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 41) (1/3):
+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.
+
+------------------------------------------------------------
+
+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
+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].
+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).
+  (* 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.
+  (* 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)))).
+  (* Invariant *)
+  Have: (0 <= i_5) /\ (i_5 <= 10).
+  (* Else *)
+  Have: 10 <= i_5.
+  (* Loop assigns ... *)
+  Have: ((Init_undef_2[a_8]=true) -> (i_9=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.
+}
+Prove: (i = 0) \/ (i = 2) \/ (i = 4) \/
+    ((i_1 != 0) /\ (i_1 != 2) /\ (i_1 != 4)).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (3/5):
+Effect at line 50
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (4/5):
+Effect at line 50
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memtyped.i, line 48) (5/5):
+Effect at line 50
+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
new file mode 100644
index 0000000000000000000000000000000000000000..71276a1d27b4d849127b4cac0d9e4d06f92a50c3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
@@ -0,0 +1,447 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 10):
+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: 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.
+  (* Invariant *)
+  Have: ((0 < i) ->
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true))))).
+  (* Invariant *)
+  Have: i <= 10.
+  (* Then *)
+  Have: i <= 9.
+}
+Prove: (v[i <- true][i_1]=true).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 11):
+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).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 23):
+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).
+  (* 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) -> ((v[i_3]=true) ->
+       (a[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]))))).
+  (* Else *)
+  Have: 10 <= i_2.
+}
+Prove: (a[i]=true).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 30):
+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))))).
+  (* 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) -> ((v[i_4]=true) ->
+       (a[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]))))).
+  (* 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):
+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))))).
+  (* 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) -> ((v[i_4]=true) ->
+       (a[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]))))).
+  (* 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).
+  (* Then *)
+  Have: i <= 9.
+}
+Prove: (-1) <= i.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/assigned_initialized_memvar.i, line 33):
+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) -> ((v_1[i_5]=true) ->
+       (a[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]))))).
+  (* 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 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) -> ((v_2[i_6]=true) ->
+       (a[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]))))).
+  (* 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 Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 54):
+Let a = Init_s_0.Init_F1_S_a.
+Let a_1 = Init_s_1.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) /\ is_sint32(i_6).
+  (* Invariant *)
+  Have: ((0 < i_1) ->
+      (forall i_7 : Z. ((0 <= i_7) -> ((i_7 < i_1) -> (v[i_7]=true))))).
+  (* Invariant *)
+  Have: (0 <= i_1) /\ (i_1 <= 10).
+  (* 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) -> ((v[i_7]=true) ->
+       (a_1[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]))))).
+  (* 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. ((0 <= i_7) -> ((i_7 <= 9) ->
+       ((v_2[4 <- v_3][i_7]=true) -> (a[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]))))))).
+  (* Else *)
+  Have: 10 <= i_6.
+}
+Prove: (a[i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'SMOKE' (file tests/wp_acsl/assigned_initialized_memvar.i, line 55):
+Let a = Init_s_0.Init_F1_S_a.
+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))))).
+  (* 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) -> ((v[i_6]=true) ->
+       (a[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]))))).
+  (* Else *)
+  Have: 10 <= i_1.
+  (* Else *)
+  Have: 10 <= i_2.
+  (* Loop assigns ... *)
+  Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((a[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. ((0 <= i_6) -> ((i_6 <= 9) ->
+       ((v_2[4 <- v_3][i_6]=true) -> ((Init_s_1.Init_F1_S_a)[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]))))))).
+  (* Else *)
+  Have: 10 <= i_5.
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 12):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 18) (1/2):
+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.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 34):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 42) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 42) (2/2):
+Effect at line 44
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (1/5):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (2/5):
+Effect at line 50
+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))))).
+  (* Invariant *)
+  Have: (0 <= i_2) /\ (i_2 <= 10).
+  (* Else *)
+  Have: 10 <= i_2.
+  (* Loop assigns ... *)
+  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
+      (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((v[i_9]=true) ->
+       (a[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]))))).
+  (* Else *)
+  Have: 10 <= i_3.
+  (* Else *)
+  Have: 10 <= i_4.
+  (* Loop assigns ... *)
+  Have: forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((a[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)).
+  (* Else *)
+  Have: 10 <= i_6.
+  (* Loop assigns ... *)
+  Have: ((Init_s_1.Init_F1_S_i)=true) /\
+      (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) ->
+       ((v_2[4 <- v_3][i_9]=true) -> ((Init_s_1.Init_F1_S_a)[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]))))))).
+  (* Then *)
+  Have: i_7 <= 9.
+}
+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.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (4/5):
+Effect at line 51
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (5/5):
+Effect at line 51
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a3d7ea7b5a0e45db32c3d49439ea3dd594acdded
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
@@ -0,0 +1,276 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function test
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 12):
+Assume { (* Heap *) Type: region(x.base) <= 0. }
+Prove: (Init_0[x]=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 13):
+Assume {
+  (* Heap *)
+  Type: region(a.base) <= 0.
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 1).
+}
+Prove: (ArrayInit1_int(a, 2, Init_0)[i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 14):
+Let a = Load_Init_S2_C(c, Init_0).
+Let a_1 = a.Init_F2_C_s.
+Assume { (* Heap *) Type: region(c.base) <= 0. }
+Prove: ((a.Init_F2_C_x)=true) /\ ((a_1.Init_F1_S_x)=true) /\
+    ((a_1.Init_F1_S_y)=true) /\
+    (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a.Init_F2_C_a)[i]=true)))).
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 20):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 21):
+Assume { (* Heap *) Type: (region(a.base) <= 0) /\ (region(x.base) <= 0). }
+Prove: (Init_0[x <- true][shift_sint32(a, 1)]=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 22):
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(x.base) <= 0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 1).
+}
+Prove: (ArrayInit1_int(a, 2, Init_0[x <- true][shift_sint32(a, 0) <- true])
+          [i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 25):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 26):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 27):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 30):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 31):
+Let a_1 = Load_Init_S1_S(shiftfield_F2_C_s(c),
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true]).
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_1.Init_F1_S_x)=true) /\ ((a_1.Init_F1_S_y)=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 32):
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 9).
+}
+Prove: (ArrayInit1_int(shiftfield_F2_C_a(c), 10,
+          Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+            <- true][shiftfield_F2_C_x(c) <- true])[i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 33):
+Let a_1 = Load_Init_S2_C(c,
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true]).
+Let a_2 = a_1.Init_F2_C_s.
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_1.Init_F2_C_x)=true) /\ ((a_2.Init_F1_S_x)=true) /\
+    ((a_2.Init_F1_S_y)=true) /\
+    (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_1.Init_F2_C_a)[i]=true)))).
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 36):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 37):
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+          <- true][shiftfield_F1_S_y(shiftfield_F2_C_s(c))]=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 38):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = Load_Init_S1_S(a_1,
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+              <- true]).
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_2.Init_F1_S_x)=true) /\ ((a_2.Init_F1_S_y)=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 39):
+Let a_1 = Load_Init_S2_C(c,
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true]
+              [shiftfield_F1_S_x(shiftfield_F2_C_s(c)) <- true]).
+Let a_2 = a_1.Init_F2_C_s.
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_1.Init_F2_C_x)=true) /\ ((a_2.Init_F1_S_x)=true) /\
+    ((a_2.Init_F1_S_y)=true) /\
+    (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_1.Init_F2_C_a)[i]=true)))).
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 42):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = Load_Init_S1_S(a_1,
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+              <- true][shiftfield_F1_S_y(a_1) <- true]).
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_2.Init_F1_S_x)=true) /\ ((a_2.Init_F1_S_y)=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 43):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = Load_Init_S2_C(c,
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+              <- true][shiftfield_F1_S_y(a_1) <- true]).
+Let a_3 = a_2.Init_F2_C_s.
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_2.Init_F2_C_x)=true) /\ ((a_3.Init_F1_S_x)=true) /\
+    ((a_3.Init_F1_S_y)=true) /\
+    (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_2.Init_F2_C_a)[i]=true)))).
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 46):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = shiftfield_F2_C_a(c).
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 8).
+}
+Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+          <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+          <- true][shiftfield_F1_S_y(a_1) <- true][shift_sint32(a_2, 8)
+          <- true][shift_sint32(a_2, 7) <- true][shift_sint32(a_2, 6)
+          <- true][shift_sint32(a_2, 5) <- true][shift_sint32(a_2, 4)
+          <- true][shift_sint32(a_2, 3) <- true][shift_sint32(a_2, 2)
+          <- true][shift_sint32(a_2, 1) <- true][shift_sint32(a_2, 0)
+          <- true][shift_sint32(a_2, i)]=true).
+
+------------------------------------------------------------
+
+Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 47):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = shiftfield_F2_C_a(c).
+Let a_3 = Load_Init_S2_C(c,
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+              <- true][shiftfield_F1_S_y(a_1) <- true][shift_sint32(a_2, 8)
+              <- true][shift_sint32(a_2, 7) <- true][shift_sint32(a_2, 6)
+              <- true][shift_sint32(a_2, 5) <- true][shift_sint32(a_2, 4)
+              <- true][shift_sint32(a_2, 3) <- true][shift_sint32(a_2, 2)
+              <- true][shift_sint32(a_2, 1) <- true][shift_sint32(a_2, 0)
+              <- true]).
+Let a_4 = a_3.Init_F2_C_s.
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_3.Init_F2_C_x)=true) /\ ((a_4.Init_F1_S_x)=true) /\
+    ((a_4.Init_F1_S_y)=true) /\
+    (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_3.Init_F2_C_a)[i]=true)))).
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 50):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = shiftfield_F2_C_a(c).
+Let a_3 = Load_Init_S2_C(c,
+            Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+              <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+              <- true][shiftfield_F1_S_y(a_1) <- true][shift_sint32(a_2, 8)
+              <- true][shift_sint32(a_2, 7) <- true][shift_sint32(a_2, 6)
+              <- true][shift_sint32(a_2, 5) <- true][shift_sint32(a_2, 4)
+              <- true][shift_sint32(a_2, 3) <- true][shift_sint32(a_2, 2)
+              <- true][shift_sint32(a_2, 1) <- true][shift_sint32(a_2, 0)
+              <- true][shift_sint32(a_2, 9) <- true]).
+Let a_4 = a_3.Init_F2_C_s.
+Assume {
+  (* Heap *)
+  Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+      (region(x.base) <= 0).
+}
+Prove: ((a_3.Init_F2_C_x)=true) /\ ((a_4.Init_F1_S_x)=true) /\
+    ((a_4.Init_F1_S_y)=true) /\
+    (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_3.Init_F2_C_a)[i]=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
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/052040e80d2b0a66ce3f375f87b6ff42.json
@@ -0,0 +1 @@
+{ "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
new file mode 100644
index 0000000000000000000000000000000000000000..9125f6b41d6f85c5c09a01c4ce601217fbea99c9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0a455ba1935274c35611d5fdf0fc2f8f.json
@@ -0,0 +1,2 @@
+{ "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/5638c5e45ea8450040bc5a67415363a5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5638c5e45ea8450040bc5a67415363a5.json
new file mode 100644
index 0000000000000000000000000000000000000000..fc60b98b9e002045a095ef5326ea9b0a2d1fe575
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5638c5e45ea8450040bc5a67415363a5.json
@@ -0,0 +1,2 @@
+{ "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
new file mode 100644
index 0000000000000000000000000000000000000000..29e4ca835905de63d07c3980f02885158b984d15
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/5651f36fea599e9ff5d67e9df8679972.json
@@ -0,0 +1,2 @@
+{ "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
new file mode 100644
index 0000000000000000000000000000000000000000..c0b0613e97a7c4900c15cfb5db9efd479e85bb6b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/84ac30ceabf40ae460d3a6638be6ea4d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0385,
+  "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
new file mode 100644
index 0000000000000000000000000000000000000000..24271896cafb873a9ac2c20b81e2c5e66f103fc1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/945f495a93303995087d23241c179c2f.json
@@ -0,0 +1,2 @@
+{ "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
new file mode 100644
index 0000000000000000000000000000000000000000..e0c1ac6b238a9f36c34e4f2133c9c5c68633eee7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/95004af59474d658afa48c1fddcc4b38.json
@@ -0,0 +1,2 @@
+{ "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/b8ca0e444c91c4ef4790a8775a3da864.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b8ca0e444c91c4ef4790a8775a3da864.json
new file mode 100644
index 0000000000000000000000000000000000000000..0b5ca39ac99b3118433d8908822190ef6e3ea8e5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b8ca0e444c91c4ef4790a8775a3da864.json
@@ -0,0 +1,2 @@
+{ "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
new file mode 100644
index 0000000000000000000000000000000000000000..80d093eb059e04b8babcaaf8f01b0e8ff417b5de
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/b9b74fb903d3948de1f1284737fcc1b4.json
@@ -0,0 +1,2 @@
+{ "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/df1b1f99fbd7c697efdffd3389b62ba3.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/df1b1f99fbd7c697efdffd3389b62ba3.json
new file mode 100644
index 0000000000000000000000000000000000000000..9fbe0e773195d3d1a78dd26470be3048bc22ce1a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/df1b1f99fbd7c697efdffd3389b62ba3.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0146,
+  "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
new file mode 100644
index 0000000000000000000000000000000000000000..627150223b0a45b795051db34423bf4232e3377f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/e4f6b760b38c0d0d9e14569809271d9f.json
@@ -0,0 +1,2 @@
+{ "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.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8d8c5b5b37c44e6db9f664d1bbb3cfa11fdd4655
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
@@ -0,0 +1,46 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 32 goals scheduled
+[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session'
+[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
+  Qed:            21 
+  Alt-Ergo:       10  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  main                     21       10       32      96.9%
+------------------------------------------------------------
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
new file mode 100644
index 0000000000000000000000000000000000000000..81296a4df59b413a9f34fb0747f96952e7a8637c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0044,
+  "steps": 13 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0ea068d1821f3b958beb619aabd2bf71.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0ea068d1821f3b958beb619aabd2bf71.json
new file mode 100644
index 0000000000000000000000000000000000000000..27cea6ffc6d103500343ad46a2d96fed743e278e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0ea068d1821f3b958beb619aabd2bf71.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0051,
+  "steps": 47 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/26f2bec626edf9f3b21ce506a0dbc878.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/26f2bec626edf9f3b21ce506a0dbc878.json
new file mode 100644
index 0000000000000000000000000000000000000000..6d1863edc6336c62b39c81fc5cd63e0e8e092bc4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/26f2bec626edf9f3b21ce506a0dbc878.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0074,
+  "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/47fdc2d6da39295871208bb185768ba9.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/47fdc2d6da39295871208bb185768ba9.json
new file mode 100644
index 0000000000000000000000000000000000000000..119359e0f31a5aa313ebd7c2db0fdaf2e18cce6b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/47fdc2d6da39295871208bb185768ba9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0023,
+  "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/532fc8247c18cc12fc05c6dca37a85df.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/532fc8247c18cc12fc05c6dca37a85df.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/532fc8247c18cc12fc05c6dca37a85df.json
@@ -0,0 +1 @@
+{ "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/5829cd050c6e5edf4241b52cfb347dbc.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/5829cd050c6e5edf4241b52cfb347dbc.json
new file mode 100644
index 0000000000000000000000000000000000000000..bab04bc361ebfe2c1c2ce364c43b98a1e291f140
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/5829cd050c6e5edf4241b52cfb347dbc.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0094,
+  "steps": 39 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/81f6bbec14f78ded8be06b4d83acbdca.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/81f6bbec14f78ded8be06b4d83acbdca.json
new file mode 100644
index 0000000000000000000000000000000000000000..53ba6839db5cae325141f52649eb2781dac5842b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/81f6bbec14f78ded8be06b4d83acbdca.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0057,
+  "steps": 21 }
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
new file mode 100644
index 0000000000000000000000000000000000000000..81d5e9d2f02ec5c7aba39d05f3bfde0ba8093fdc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0066,
+  "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/c17ff689fb984c1d15fced512cddb9f0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/c17ff689fb984c1d15fced512cddb9f0.json
new file mode 100644
index 0000000000000000000000000000000000000000..0e6c81c0a50af4d3768e755af594b3fa0640a296
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/c17ff689fb984c1d15fced512cddb9f0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0082,
+  "steps": 25 }
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
new file mode 100644
index 0000000000000000000000000000000000000000..4f004cd73a5911825124808ce65b40222a9e9f7e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0048,
+  "steps": 11 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fbb170335579f1933320c49f3fd8f1ca.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fbb170335579f1933320c49f3fd8f1ca.json
new file mode 100644
index 0000000000000000000000000000000000000000..9059ef128495bd6c611174f4853ba9098137e28d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fbb170335579f1933320c49f3fd8f1ca.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0081,
+  "steps": 20 }
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
new file mode 100644
index 0000000000000000000000000000000000000000..1e4969d23d850c5762c8b6ad815a6f617570b05b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -0,0 +1,39 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 25 goals scheduled
+[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session'
+[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)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  main                     14       10       25      96.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/2702cd81e561c5c1596a65481c05f129.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/2702cd81e561c5c1596a65481c05f129.json
new file mode 100644
index 0000000000000000000000000000000000000000..3c790cc07f2094751ed98cc6ed39a66e3a3c7425
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/2702cd81e561c5c1596a65481c05f129.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1538,
+  "steps": 11 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/28744b6608a5f351a734556f82197132.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/28744b6608a5f351a734556f82197132.json
new file mode 100644
index 0000000000000000000000000000000000000000..9816a098bf8e261dce0dd0f5d9df5c0ae69828b8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/28744b6608a5f351a734556f82197132.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.4007,
+  "steps": 70 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/51000d68001519bba1ac23af992d5de0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/51000d68001519bba1ac23af992d5de0.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/51000d68001519bba1ac23af992d5de0.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/5b37dd65672a6613ff93b1aad99d1462.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/5b37dd65672a6613ff93b1aad99d1462.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/5b37dd65672a6613ff93b1aad99d1462.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/82c12b8306cfe612f5440485b2d7dba7.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/82c12b8306cfe612f5440485b2d7dba7.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/82c12b8306cfe612f5440485b2d7dba7.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/8ac59cb035804eef1eeb78faeac2d646.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/8ac59cb035804eef1eeb78faeac2d646.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/8ac59cb035804eef1eeb78faeac2d646.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/938944c0eb3b8153f9975cf9df58b1e3.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/938944c0eb3b8153f9975cf9df58b1e3.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/938944c0eb3b8153f9975cf9df58b1e3.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/9d85780d2569a36247e3e4a2c7960244.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/9d85780d2569a36247e3e4a2c7960244.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/9d85780d2569a36247e3e4a2c7960244.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/9dd332bb66f12035d8679f1bfe937510.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/9dd332bb66f12035d8679f1bfe937510.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/9dd332bb66f12035d8679f1bfe937510.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/ace0e229b99ba4827691371a58a81204.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/ace0e229b99ba4827691371a58a81204.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/ace0e229b99ba4827691371a58a81204.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/ce787053deb7473ae1656c67852a16db.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/ce787053deb7473ae1656c67852a16db.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/ce787053deb7473ae1656c67852a16db.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d0dea0f9c40c22c7cf95a7ce83f51a3c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d0dea0f9c40c22c7cf95a7ce83f51a3c.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d0dea0f9c40c22c7cf95a7ce83f51a3c.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d656511a5fe16b7b52bc7ce928656687.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d656511a5fe16b7b52bc7ce928656687.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d656511a5fe16b7b52bc7ce928656687.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/eee0ba12fe324670f9250c4d50d2b3c0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/eee0ba12fe324670f9250c4d50d2b3c0.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/eee0ba12fe324670f9250c4d50d2b3c0.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/f59c3690e813371dbfc90ef1c574d362.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/f59c3690e813371dbfc90ef1c574d362.json
new file mode 100644
index 0000000000000000000000000000000000000000..8ed32d78ed0ced1fc192fd235d070e243768fa1b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/f59c3690e813371dbfc90ef1c574d362.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0082,
+  "steps": 15 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/fde9205db7f447e0889ad2dc702b1d17.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/fde9205db7f447e0889ad2dc702b1d17.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/fde9205db7f447e0889ad2dc702b1d17.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..003c83000b91fc1ab1314a3547dfe2861662762a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
@@ -0,0 +1,37 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 23 goals scheduled
+[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session'
+[wp] [Alt-Ergo] Goal typed_test_check_unknown : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_3 : Unsuccess
+[wp] [Qed] Goal typed_test_check_qed_ok : Valid
+[wp] [Qed] Goal typed_test_check_qed_ok_2 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_4 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_5 : Unsuccess
+[wp] [Qed] Goal typed_test_check_qed_ok_3 : Valid
+[wp] [Qed] Goal typed_test_check_qed_ok_4 : Valid
+[wp] [Qed] Goal typed_test_check_qed_ok_5 : Valid
+[wp] [Qed] Goal typed_test_check_qed_ok_6 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_6 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_7 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_8 : Unsuccess
+[wp] [Qed] Goal typed_test_check_qed_ok_7 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_9 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_10 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_11 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_provable : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_12 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_provable_2 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_unknown_13 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_check_provable_3 : Valid
+[wp] Proved goals:   10 / 23
+  Qed:             7 
+  Alt-Ergo:        3  (unsuccess: 13)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  test                      7        3       23      43.5%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/3031ad00f971861aae099806997c8413.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/3031ad00f971861aae099806997c8413.json
new file mode 100644
index 0000000000000000000000000000000000000000..95051841046a88d8062e50559dda4983db5fdf1f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/3031ad00f971861aae099806997c8413.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0034,
+  "steps": 5 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/5c2a44e757abacde26f5081aeeb8cd42.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/5c2a44e757abacde26f5081aeeb8cd42.json
new file mode 100644
index 0000000000000000000000000000000000000000..bff366ddbeab3f1dc00b2f240fda0aa7c6d22f72
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/5c2a44e757abacde26f5081aeeb8cd42.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "steps": 7 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/5e11e16d3bdef94a9e79073dbee378c6.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/5e11e16d3bdef94a9e79073dbee378c6.json
new file mode 100644
index 0000000000000000000000000000000000000000..bd5324a63d8d3f377a60689ff9b16120b45e4db7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/5e11e16d3bdef94a9e79073dbee378c6.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0072,
+  "steps": 6 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/8992f7f080748be0b29a31cf47208af3.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/8992f7f080748be0b29a31cf47208af3.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/8992f7f080748be0b29a31cf47208af3.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/a24ad3a34f18593488e5d801d393dde6.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/a24ad3a34f18593488e5d801d393dde6.json
new file mode 100644
index 0000000000000000000000000000000000000000..d290032f9bb7f654794d98bc79aca93777b84cc1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/a24ad3a34f18593488e5d801d393dde6.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0037,
+  "steps": 6 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/c951fdb6d5b9c5cf37b30b8e09d451d2.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/c951fdb6d5b9c5cf37b30b8e09d451d2.json
new file mode 100644
index 0000000000000000000000000000000000000000..9c6e34917ff3b60ec03f09aa34751bd5d074dd4e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/c951fdb6d5b9c5cf37b30b8e09d451d2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0003,
+  "steps": 5 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/d4db793d5927f5155b26139dee98cdc5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/d4db793d5927f5155b26139dee98cdc5.json
new file mode 100644
index 0000000000000000000000000000000000000000..60cef0488b3ce0f4a806c46797a24c53aafd7781
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/d4db793d5927f5155b26139dee98cdc5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0037,
+  "steps": 5 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/fcfc9f465c8cb0d89783e7a308867761.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/fcfc9f465c8cb0d89783e7a308867761.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session/cache/fcfc9f465c8cb0d89783e7a308867761.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
index ea40fb15e882b9468480b994c6da3818d571bd08..1f5d08de549f42592679492c6254025fd89525de 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
@@ -7,6 +7,7 @@
 [wp] [Qed] Goal typed_globals_check_qed_ok : Valid
 [wp] [Qed] Goal typed_globals_check_qed_ok_2 : Valid
 [wp] [Qed] Goal typed_globals_check_qed_ok_3 : Valid
+[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session'
 [wp] [Alt-Ergo] Goal typed_globals_check_qed_ko : Unsuccess
 [wp] [Qed] Goal typed_globals_check_qed_ok_4 : Valid
 [wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_2 : Unsuccess