diff --git a/src/plugins/wp/cfgInit.ml b/src/plugins/wp/cfgInit.ml
index eba644dc7dd4d1fa48b39b5c04e5254444fc64ae..414da17ebf2cd686f8fc16bd2b9d48581949d42b 100644
--- a/src/plugins/wp/cfgInit.ml
+++ b/src/plugins/wp/cfgInit.ml
@@ -26,22 +26,22 @@ module Make(W : Mcfg.S) =
 struct
 
   let compute_global_init wenv filter obj =
-    Globals.Vars.fold_in_file_order
+    Globals.Vars.fold_in_file_rev_order
       (fun var initinfo obj ->
+
          if var.vstorage = Extern then obj else
            let do_init = match filter with
              | `All -> true
              | `InitConst -> Cil.isGlobalInitConst var
            in if not do_init then obj
-           else
-             let old_loc = Cil.CurrentLoc.get () in
+           else let old_loc = Cil.CurrentLoc.get () in
              Cil.CurrentLoc.set var.vdecl ;
              let obj = W.init wenv var initinfo.init obj in
              Cil.CurrentLoc.set old_loc ; obj
       ) obj
 
   let process_global_const wenv obj =
-    Globals.Vars.fold_in_file_order
+    Globals.Vars.fold_in_file_rev_order
       (fun var _initinfo obj ->
          if Cil.isGlobalInitConst var
          then W.const wenv var obj
diff --git a/src/plugins/wp/tests/wp_acsl/global_const_dependencies.i b/src/plugins/wp/tests/wp_acsl/global_const_dependencies.i
new file mode 100644
index 0000000000000000000000000000000000000000..e87a30d5f0cb74cbcd7715fd9ef15309dc13ab18
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/global_const_dependencies.i
@@ -0,0 +1,7 @@
+static int const A = 1 ;
+static int const B = A+1 ;
+
+int main(void) {
+  //@ assert B == 2 ;
+  return 0;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/global_const_dependencies.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/global_const_dependencies.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bd77fee4cecfe2ccf1421799a799c489c35c07ed
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/global_const_dependencies.res.oracle
@@ -0,0 +1,12 @@
+# frama-c -wp [...]
+[kernel] Parsing global_const_dependencies.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Assertion (file global_const_dependencies.i, line 5):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
index 6071ee00dc7180186cdb32f3429492cf6da89d2b..5c44d6289ed42523daac49a6eff9c7d7982e3573 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
@@ -140,15 +140,13 @@ Assume {
   Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
       IsArray_sint32(ta3_0).
   (* Initializer *)
-  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
-  (* Initializer *)
-  Init: ta3_0[1] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
   (* Initializer *)
-  Init: ta3_0[3] = 1.
+  Init: x_1 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  Init: x = 1.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
+  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
   (* Initializer *)
   Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
   (* Initializer *)
@@ -156,13 +154,15 @@ Assume {
   (* Initializer *)
   Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
   (* Initializer *)
-  Init: x_1 = 1.
+  Init: ta3_0[1] = 1.
   (* Initializer *)
-  Init: x = 1.
+  Init: ta3_0[3] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
 }
 Prove: (x = x_1) /\ (x_3 = x_2).
 
@@ -179,15 +179,13 @@ Assume {
   Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
       IsArray_sint32(ta3_0).
   (* Initializer *)
-  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
-  (* Initializer *)
-  Init: ta3_0[1] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
   (* Initializer *)
-  Init: ta3_0[3] = 1.
+  Init: x_1 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  Init: x = 1.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
+  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
   (* Initializer *)
   Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
   (* Initializer *)
@@ -195,13 +193,15 @@ Assume {
   (* Initializer *)
   Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
   (* Initializer *)
-  Init: x_1 = 1.
+  Init: ta3_0[1] = 1.
   (* Initializer *)
-  Init: x = 1.
+  Init: ta3_0[3] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
 }
 Prove: x_2 = 1.
 
@@ -218,15 +218,13 @@ Assume {
   Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
       IsArray_sint32(ta3_0).
   (* Initializer *)
-  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
-  (* Initializer *)
-  Init: ta3_0[1] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
   (* Initializer *)
-  Init: ta3_0[3] = 1.
+  Init: x_1 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  Init: x = 1.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
+  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
   (* Initializer *)
   Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
   (* Initializer *)
@@ -234,13 +232,15 @@ Assume {
   (* Initializer *)
   Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
   (* Initializer *)
-  Init: x_1 = 1.
+  Init: ta3_0[1] = 1.
   (* Initializer *)
-  Init: x = 1.
+  Init: ta3_0[3] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
 }
 Prove: x_2 = 1.
 
@@ -257,15 +257,13 @@ Assume {
   Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
       IsArray_sint32(ta3_0).
   (* Initializer *)
-  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
-  (* Initializer *)
-  Init: ta3_0[1] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
   (* Initializer *)
-  Init: ta3_0[3] = 1.
+  Init: x_1 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  Init: x = 1.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
+  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
   (* Initializer *)
   Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
   (* Initializer *)
@@ -273,13 +271,15 @@ Assume {
   (* Initializer *)
   Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
   (* Initializer *)
-  Init: x_1 = 1.
+  Init: ta3_0[1] = 1.
   (* Initializer *)
-  Init: x = 1.
+  Init: ta3_0[3] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
 }
 Prove: x_2 = 1.
 
@@ -380,1339 +380,1338 @@ Prove: x_3 = 1.
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Struct_Simple_a' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: x_1 = 2.
+Prove: x_5 = 2.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Struct_Simple_b' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
+  (* Initializer *)
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: a_5[0] = 2.
+  (* Initializer *)
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[2] = 4.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
-  (* Initializer *)
-  Init: a_2[0] = 2.
-  (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: x = 0.
+Prove: x_4 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Simple_Array_0' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: x_2 = 1.
+Prove: x_3 = 1.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Simple_Array_1' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Let x_6 = t[1].
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(x_6) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(x_6) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
+  (* Initializer *)
+  Init: a_5[0] = 2.
+  (* Initializer *)
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[2] = 4.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
-  (* Initializer *)
-  Init: x_1 = 2.
-  (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: x_6 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,With_Array_Struct_5' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
-Let a_8 = a[5].
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
+Let a_8 = a_6[5].
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a_8).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_8).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: a_8 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,With_Array_Struct_3' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: a_1 = 4.
+Prove: a_7 = 4.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Sc_eq' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
+  (* Initializer *)
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: a_5[0] = 2.
+  (* Initializer *)
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[2] = 4.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
-  (* Initializer *)
-  Init: a_2[0] = 2.
-  (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: EqS3_Sc(sc1_0, sc0_0).
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Sc_t' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
-Let a_8 = a_4[2].
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
+Let a_8 = a_3[2].
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_8) /\ is_sint32(a_6) /\
-      is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\ is_sint32(a_1) /\
-      is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_8) /\ is_sint32(a_2) /\
+      is_sint32(a[1]) /\ is_sint32(a[2]) /\ is_sint32(a_7) /\
+      is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: a_8 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Sc_t' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: a_6 = 4.
+Prove: a_2 = 4.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Sc_c_2' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: a_6[0] = 1.
+  (* Initializer *)
+  Init: a_6[1] = 2.
+  (* Initializer *)
+  Init: a_6[2] = 3.
+  (* Initializer *)
+  Init: a_7 = 4.
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
+  (* Initializer *)
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
   Init: a_5[0] = 2.
   (* Initializer *)
   Init: a_5[1] = 3.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
   Init: a_4[0] = 2.
   (* Initializer *)
   Init: a_4[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
   Init: a_3[0] = 2.
   (* Initializer *)
   Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: x_2 = 1.
-  (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
-  (* Initializer *)
-  Init: x_1 = 2.
-  (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: x_3 = 4.
+Prove: x_2 = 4.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Sc_c_3' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: x_4 = 0.
+Prove: x_1 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Tab_no_init' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Let x_6 = tab_0[5].
 Assume {
-  Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(x_6) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+  Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(x_6) /\ is_sint16(x) /\
+      is_sint32(x_3) /\ is_sint32(t[1]) /\ is_sint32(t1_0[4]) /\
+      is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_2) /\ is_sint32(x_1) /\
+      is_sint32(a_3[2]) /\ is_sint32(a_2) /\ is_sint32(a[1]) /\
+      is_sint32(a[2]) /\ is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: x_6 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,Tab_todo' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
@@ -1720,330 +1719,330 @@ Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 31) /\ is_sint32(i).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a_7[i_1] = 2))).
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_7[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a_6[i_1] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_4[i_1] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_3[i_1] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a[i_1] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a[i_1] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a[i_1] = 0))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: tab_0[i] <= 255.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
-Let a_8 = a_7[1].
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
+Let a_8 = a[1].
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_8) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a_8) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: a_8 = 2.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
-Let a_8 = a_7[2].
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
+Let a_8 = a[2].
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_8) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a_8) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: a_8 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
@@ -2051,220 +2050,219 @@ Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 3).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a_7[i_1] = 2))).
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_7[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a_6[i_1] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_4[i_1] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_3[i_1] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a[i_1] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a[i_1] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a[i_1] = 0))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: t1_0[i] = 1.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,todo' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Let x_6 = t1_0[4].
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(x_6) /\ is_sint32(x_1) /\ is_sint32(x) /\ is_sint32(x_3) /\
-      is_sint32(x_4) /\ is_sint32(a_4[2]) /\ is_sint32(a_6) /\
-      is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\ is_sint32(a_1) /\
-      is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\ is_sint32(x_6) /\
+      is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_2) /\ is_sint32(x_1) /\
+      is_sint32(a_3[2]) /\ is_sint32(a_2) /\ is_sint32(a[1]) /\
+      is_sint32(a[2]) /\ is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
+  (* Initializer *)
+  Init: a_5[2] = 4.
+  (* Initializer *)
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[2] = 4.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
-  (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: x_2 = 1.
-  (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: x_6 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
@@ -2272,110 +2270,110 @@ Assume {
   (* Goal *)
   When: (6 <= i) /\ (i <= 6).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a_7[i_1] = 2))).
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_7[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a_6[i_1] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_4[i_1] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
+  (* Initializer *)
+  Init: a_5[2] = 4.
+  (* Initializer *)
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[2] = 4.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_3[i_1] = 0))).
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[0] = 1.
-  (* Initializer *)
-  Init: a[1] = 2.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a[i_1] = 0))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a[i_1] = 2))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a[i_1] = 0))).
   (* Initializer *)
-  Init: x_2 = 1.
-  (* Initializer *)
-  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: t1_0[i] = 2.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
@@ -2383,193 +2381,193 @@ Assume {
   (* Goal *)
   When: (7 <= i) /\ (i <= 9).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a_7[i_1] = 2))).
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_7[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a_6[i_1] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
+  (* Initializer *)
+  Init: a_5[0] = 2.
+  (* Initializer *)
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_4[i_1] = 0))).
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[2] = 4.
   (* Initializer *)
   Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
-  (* Initializer *)
-  Init: a_2[0] = 2.
-  (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a_3[i_1] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 9) -> (a[i_1] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 1) -> (a[i_1] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i_1 : Z. ((2 <= i_1) -> ((i_1 <= 2) -> (a[i_1] = 0))).
   (* Initializer *)
-  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 1) -> (t[i_1] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 31) -> (tab_0[i_1] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
 Prove: t1_0[i] = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ok,direct_init_union' in 'main':
-Let x = s.F1_S_b.
-Let x_1 = s.F1_S_a.
-Let x_2 = t[0].
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
-Let a_2 = sc0_0.F3_Sc_b.
-Let a_3 = sc1_0.F3_Sc_b.
-Let x_3 = sc2_0.F3_Sc_c.
-Let a_4 = sc2_0.F3_Sc_b.
-Let x_4 = sc3_0.F3_Sc_c.
-Let a_5 = sc3_0.F3_Sc_b.
-Let a_6 = a_5[2].
-Let a_7 = sq0_0.F3_Sc_b.
-Let x_5 = u.F4_U_a.
+Let x = u.F4_U_a.
+Let a = sq0_0.F3_Sc_b.
+Let x_1 = sc3_0.F3_Sc_c.
+Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
+Let x_2 = sc2_0.F3_Sc_c.
+Let a_3 = sc2_0.F3_Sc_b.
+Let a_4 = sc1_0.F3_Sc_b.
+Let a_5 = sc0_0.F3_Sc_b.
+Let a_6 = st_0.F2_St_tab.
+Let a_7 = a_6[3].
+Let x_3 = t[0].
+Let x_4 = s.F1_S_b.
+Let x_5 = s.F1_S_a.
 Assume {
   Type: IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ is_uint8(tab_0[5]) /\
-      is_sint16(x_5) /\ is_sint32(x_2) /\ is_sint32(t[1]) /\
-      is_sint32(t1_0[4]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(a_4[2]) /\
-      is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
-      is_sint32(a_1) /\ is_sint32(a[5]).
+      is_sint16(x) /\ is_sint32(x_3) /\ is_sint32(t[1]) /\
+      is_sint32(t1_0[4]) /\ is_sint32(x_5) /\ is_sint32(x_4) /\
+      is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(a_3[2]) /\
+      is_sint32(a_2) /\ is_sint32(a[1]) /\ is_sint32(a[2]) /\
+      is_sint32(a_7) /\ is_sint32(a_6[5]).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
       IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: x_5 = (-1).
+  Init: x_5 = 2.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: x_4 = 0.
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_a) = 2.
+  Init: x_3 = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a_7[i] = 2))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_7[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: (sq0_0.F3_Sc_c) = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_5[1] = 3.
+  Init: a_6[0] = 1.
   (* Initializer *)
-  Init: a_6 = 4.
+  Init: a_6[1] = 2.
   (* Initializer *)
-  Init: x_4 = 0.
+  Init: a_6[2] = 3.
   (* Initializer *)
-  Init: (sc2_0.F3_Sc_a) = 1.
+  Init: a_7 = 4.
   (* Initializer *)
-  Init: a_4[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_6[i] = 0))).
   (* Initializer *)
-  Init: a_4[1] = 3.
+  Init: (sc0_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_4[i] = 0))).
+  Init: a_5[0] = 2.
   (* Initializer *)
-  Init: x_3 = 4.
+  Init: a_5[1] = 3.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_a) = 1.
+  Init: a_5[2] = 4.
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: (sc0_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: (sc1_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_3[2] = 4.
+  Init: a_4[0] = 2.
   (* Initializer *)
-  Init: (sc1_0.F3_Sc_c) = 5.
+  Init: a_4[1] = 3.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_a) = 1.
+  Init: a_4[2] = 4.
   (* Initializer *)
-  Init: a_2[0] = 2.
+  Init: (sc1_0.F3_Sc_c) = 5.
   (* Initializer *)
-  Init: a_2[1] = 3.
+  Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_2[2] = 4.
+  Init: a_3[0] = 2.
   (* Initializer *)
-  Init: (sc0_0.F3_Sc_c) = 5.
+  Init: a_3[1] = 3.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a_3[i] = 0))).
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: x_2 = 4.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a_1 = 4.
+  Init: a_1[0] = 2.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+  Init: a_1[1] = 3.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  Init: a_2 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  Init: x_1 = 0.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  Init: (sq0_0.F3_Sc_a) = 2.
   (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
   (* Initializer *)
-  Init: x_2 = 1.
+  Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (sq0_0.F3_Sc_c) = 2.
   (* Initializer *)
-  Init: x_1 = 2.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: x = 0.
+  Init: x = (-1).
 }
-Prove: x_5 = (-1).
+Prove: x = (-1).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
index f751ef040819de7de6ccd6c0e9e35341c41ceec5..821291b40ccce48898653fb99fb582b4c1811661 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
@@ -192,34 +192,42 @@ Prove: x = 1.
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,Sc_eq_ko' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(t[1]) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  (* Initializer *)
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -231,61 +239,61 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
 Prove: EqS3_Sc(sc2_0, sc3_0).
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,Sc_t' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(t[1]) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  (* Initializer *)
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -297,61 +305,61 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
-Prove: a_4 = 3.
+Prove: a_1 = 3.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,Sc_c_2' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(t[1]) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -363,62 +371,62 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
 Prove: x = 2.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,Tab_no_init' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Let x_1 = tab_0[5].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(x_1) /\
       is_sint32(t[1]) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  (* Initializer *)
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -430,61 +438,61 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
 Prove: x_1 = 1.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,With_Array_Struct_3' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(t[1]) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -496,62 +504,62 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
-Prove: a_1 = 3.
+Prove: a_4 = 3.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,Simple_Array_1' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Let x_1 = t[1].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(x_1) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  (* Initializer *)
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -563,62 +571,62 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
 Prove: x_1 = 1.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,T1_6' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Let x_1 = t1_0[6].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(t[1]) /\ is_sint32(x_1) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  (* Initializer *)
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -630,62 +638,62 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
 Prove: x_1 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,indirect_init_union_b' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Let x_1 = u.F4_U_b.
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(t[1]) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(x_1) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(x_1) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  (* Initializer *)
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -697,62 +705,62 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
 Prove: x_1 = 0.
 
 ------------------------------------------------------------
 
 Goal Pre-condition 'qed_ko,indirect_init_union_t' in 'main_ko':
-Let a = st_0.F2_St_tab.
-Let a_1 = a[3].
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
 Let x = sc2_0.F3_Sc_c.
 Let a_2 = sc2_0.F3_Sc_b.
-Let a_3 = sc3_0.F3_Sc_b.
-Let a_4 = a_3[2].
+Let a_3 = st_0.F2_St_tab.
+Let a_4 = a_3[3].
 Let a_5 = (u.F4_U_t)[0].
 Assume {
   Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_uint8(tab_0[5]) /\
       is_sint32(t[1]) /\ is_sint32(t1_0[6]) /\ is_sint32(x) /\
-      is_sint64(u.F4_U_b) /\ is_sint16(a_5) /\ is_sint32(a_4) /\
-      is_sint32(a_1).
+      is_sint64(u.F4_U_b) /\ is_sint16(a_5) /\ is_sint32(a_1) /\
+      is_sint32(a_4).
   (* Heap *)
   Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
       IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
   (* Initializer *)
-  Init: (u.F4_U_a) = (-1).
+  Init: t[0] = 1.
   (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_a) = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+  (* Initializer *)
+  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+  (* Initializer *)
+  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+  (* Initializer *)
+  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
   (* Initializer *)
-  Init: a_3[0] = 2.
+  Init: a_3[0] = 1.
   (* Initializer *)
-  Init: a_3[1] = 3.
+  Init: a_3[1] = 2.
+  (* Initializer *)
+  Init: a_3[2] = 3.
   (* Initializer *)
   Init: a_4 = 4.
   (* Initializer *)
-  Init: (sc3_0.F3_Sc_c) = 0.
+  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a_3[i] = 0))).
   (* Initializer *)
   Init: (sc2_0.F3_Sc_a) = 1.
   (* Initializer *)
@@ -764,27 +772,19 @@ Assume {
   (* Initializer *)
   Init: x = 4.
   (* Initializer *)
-  Init: a[0] = 1.
+  Init: (sc3_0.F3_Sc_a) = 1.
   (* Initializer *)
-  Init: a[1] = 2.
+  Init: a[0] = 2.
   (* Initializer *)
-  Init: a[2] = 3.
+  Init: a[1] = 3.
   (* Initializer *)
   Init: a_1 = 4.
   (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
-  (* Initializer *)
-  Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
-  (* Initializer *)
-  Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
-  (* Initializer *)
-  Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+  Init: (sc3_0.F3_Sc_c) = 0.
   (* Initializer *)
-  Init: t[0] = 1.
+  Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
   (* Initializer *)
-  Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+  Init: (u.F4_U_a) = (-1).
 }
 Prove: a_5 = 0.
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
index 6a67ba4d6fd3c686b990e942e4f7cdbb8bfc8e5a..f178831e9fbcf9a8cdc501abce8026ce0b56fdfe 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
@@ -14,13 +14,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_20) <= 0.
   (* Initializer *)
-  Init: (w.F1_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F1_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F1_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F1_St_b) = 2.
 }
 Prove: EqS1_St(a_1, w).
 
@@ -34,13 +34,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_20) <= 0.
   (* Initializer *)
-  Init: (w.F1_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F1_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F1_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F1_St_b) = 2.
 }
 Prove: EqS1_St(a_1, w).
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle
index b7feef815a3f905fcf725705b5d54d9097d0d695..5ff5a66df2b2c7bd3f6ac3608a7770e2cb248b79 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle
@@ -11,13 +11,13 @@ Goal Post-condition 'P' in 'main':
 Assume {
   Type: IsS1_St(v) /\ IsS1_St(w).
   (* Initializer *)
-  Init: (w.F1_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F1_St_b) = 2.
-  (* Initializer *)
   Init: (v.F1_St_a) = 1.
   (* Initializer *)
   Init: (v.F1_St_b) = 2.
+  (* Initializer *)
+  Init: (w.F1_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F1_St_b) = 2.
 }
 Prove: EqS1_St(v, w).
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/global_const_dependencies.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/global_const_dependencies.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3f93a0b972d943c83255f82232a366eece6c4205
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/global_const_dependencies.res.oracle
@@ -0,0 +1,12 @@
+# frama-c -wp [...]
+[kernel] Parsing global_const_dependencies.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Qed] Goal typed_main_assert : Valid
+[wp] Proved goals:    1 / 1
+  Qed:             1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  main                      1        -        1       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
index d2f2f233aafc0dc24fff1c207211196eefd4a84c..fbd7dd33f4182ae76bd0674381b43b41ee30c402 100644
--- a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
@@ -49,13 +49,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_30) <= 0.
   (* Initializer *)
-  Init: (w.F2_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F2_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F2_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F2_St_b) = 2.
 }
 Prove: EqS2_St(a_1, w).
 
@@ -69,13 +69,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_30) <= 0.
   (* Initializer *)
-  Init: (w.F2_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F2_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F2_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F2_St_b) = 2.
 }
 Prove: EqS2_St(a_1, w).
 
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
index 3a4d728759d7fbac2e6fb0a7a334c2c8cb815ebb..b9835cc22a8412ac09aa3e0f44de86e136e914f9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
@@ -30,108 +30,6 @@ Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 499).
   (* Initializer *)
-  Init: h2_0[0] = 0.
-  (* Initializer *)
-  Init: h2_0[1] = 1.
-  (* Initializer *)
-  Init: h2_0[2] = 2.
-  (* Initializer *)
-  Init: h2_0[3] = 3.
-  (* Initializer *)
-  Init: h2_0[4] = 4.
-  (* Initializer *)
-  Init: h2_0[5] = 5.
-  (* Initializer *)
-  Init: h2_0[6] = 6.
-  (* Initializer *)
-  Init: h2_0[7] = 7.
-  (* Initializer *)
-  Init: h2_0[8] = 8.
-  (* Initializer *)
-  Init: h2_0[9] = 9.
-  (* Initializer *)
-  Init: h2_0[10] = 10.
-  (* Initializer *)
-  Init: h2_0[11] = 11.
-  (* Initializer *)
-  Init: h2_0[12] = 12.
-  (* Initializer *)
-  Init: h2_0[13] = 13.
-  (* Initializer *)
-  Init: h2_0[14] = 14.
-  (* Initializer *)
-  Init: h2_0[15] = 15.
-  (* Initializer *)
-  Init: h2_0[16] = 16.
-  (* Initializer *)
-  Init: h2_0[17] = 17.
-  (* Initializer *)
-  Init: h2_0[18] = 18.
-  (* Initializer *)
-  Init: h2_0[19] = 19.
-  (* Initializer *)
-  Init: h2_0[20] = 20.
-  (* Initializer *)
-  Init: h2_0[21] = 21.
-  (* Initializer *)
-  Init: h2_0[22] = 22.
-  (* Initializer *)
-  Init: h2_0[23] = 23.
-  (* Initializer *)
-  Init: h2_0[24] = 24.
-  (* Initializer *)
-  Init: h2_0[25] = 25.
-  (* Initializer *)
-  Init: h2_0[26] = 26.
-  (* Initializer *)
-  Init: h2_0[27] = 27.
-  (* Initializer *)
-  Init: h2_0[28] = 28.
-  (* Initializer *)
-  Init: h2_0[29] = 29.
-  (* Initializer *)
-  Init: h2_0[30] = 30.
-  (* Initializer *)
-  Init: h2_0[31] = 31.
-  (* Initializer *)
-  Init: h2_0[32] = 32.
-  (* Initializer *)
-  Init: h2_0[33] = 33.
-  (* Initializer *)
-  Init: h2_0[34] = 34.
-  (* Initializer *)
-  Init: h2_0[35] = 35.
-  (* Initializer *)
-  Init: h2_0[36] = 36.
-  (* Initializer *)
-  Init: h2_0[37] = 37.
-  (* Initializer *)
-  Init: h2_0[38] = 38.
-  (* Initializer *)
-  Init: h2_0[39] = 39.
-  (* Initializer *)
-  Init: h2_0[40] = 40.
-  (* Initializer *)
-  Init: h2_0[41] = 41.
-  (* Initializer *)
-  Init: h2_0[42] = 42.
-  (* Initializer *)
-  Init: h2_0[43] = 43.
-  (* Initializer *)
-  Init: h2_0[44] = 44.
-  (* Initializer *)
-  Init: h2_0[45] = 45.
-  (* Initializer *)
-  Init: h2_0[46] = 46.
-  (* Initializer *)
-  Init: h2_0[47] = 47.
-  (* Initializer *)
-  Init: h2_0[48] = 48.
-  (* Initializer *)
-  Init: h2_0[49] = 49.
-  (* Initializer *)
-  Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) -> (h2_0[i_1] = 0))).
-  (* Initializer *)
   Init: h1_0[0] = 0.
   (* Initializer *)
   Init: h1_0[1] = 1.
@@ -233,6 +131,108 @@ Assume {
   Init: h1_0[49] = 49.
   (* Initializer *)
   Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) -> (h1_0[i_1] = 0))).
+  (* Initializer *)
+  Init: h2_0[0] = 0.
+  (* Initializer *)
+  Init: h2_0[1] = 1.
+  (* Initializer *)
+  Init: h2_0[2] = 2.
+  (* Initializer *)
+  Init: h2_0[3] = 3.
+  (* Initializer *)
+  Init: h2_0[4] = 4.
+  (* Initializer *)
+  Init: h2_0[5] = 5.
+  (* Initializer *)
+  Init: h2_0[6] = 6.
+  (* Initializer *)
+  Init: h2_0[7] = 7.
+  (* Initializer *)
+  Init: h2_0[8] = 8.
+  (* Initializer *)
+  Init: h2_0[9] = 9.
+  (* Initializer *)
+  Init: h2_0[10] = 10.
+  (* Initializer *)
+  Init: h2_0[11] = 11.
+  (* Initializer *)
+  Init: h2_0[12] = 12.
+  (* Initializer *)
+  Init: h2_0[13] = 13.
+  (* Initializer *)
+  Init: h2_0[14] = 14.
+  (* Initializer *)
+  Init: h2_0[15] = 15.
+  (* Initializer *)
+  Init: h2_0[16] = 16.
+  (* Initializer *)
+  Init: h2_0[17] = 17.
+  (* Initializer *)
+  Init: h2_0[18] = 18.
+  (* Initializer *)
+  Init: h2_0[19] = 19.
+  (* Initializer *)
+  Init: h2_0[20] = 20.
+  (* Initializer *)
+  Init: h2_0[21] = 21.
+  (* Initializer *)
+  Init: h2_0[22] = 22.
+  (* Initializer *)
+  Init: h2_0[23] = 23.
+  (* Initializer *)
+  Init: h2_0[24] = 24.
+  (* Initializer *)
+  Init: h2_0[25] = 25.
+  (* Initializer *)
+  Init: h2_0[26] = 26.
+  (* Initializer *)
+  Init: h2_0[27] = 27.
+  (* Initializer *)
+  Init: h2_0[28] = 28.
+  (* Initializer *)
+  Init: h2_0[29] = 29.
+  (* Initializer *)
+  Init: h2_0[30] = 30.
+  (* Initializer *)
+  Init: h2_0[31] = 31.
+  (* Initializer *)
+  Init: h2_0[32] = 32.
+  (* Initializer *)
+  Init: h2_0[33] = 33.
+  (* Initializer *)
+  Init: h2_0[34] = 34.
+  (* Initializer *)
+  Init: h2_0[35] = 35.
+  (* Initializer *)
+  Init: h2_0[36] = 36.
+  (* Initializer *)
+  Init: h2_0[37] = 37.
+  (* Initializer *)
+  Init: h2_0[38] = 38.
+  (* Initializer *)
+  Init: h2_0[39] = 39.
+  (* Initializer *)
+  Init: h2_0[40] = 40.
+  (* Initializer *)
+  Init: h2_0[41] = 41.
+  (* Initializer *)
+  Init: h2_0[42] = 42.
+  (* Initializer *)
+  Init: h2_0[43] = 43.
+  (* Initializer *)
+  Init: h2_0[44] = 44.
+  (* Initializer *)
+  Init: h2_0[45] = 45.
+  (* Initializer *)
+  Init: h2_0[46] = 46.
+  (* Initializer *)
+  Init: h2_0[47] = 47.
+  (* Initializer *)
+  Init: h2_0[48] = 48.
+  (* Initializer *)
+  Init: h2_0[49] = 49.
+  (* Initializer *)
+  Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) -> (h2_0[i_1] = 0))).
 }
 Prove: h2_0[i] = h1_0[i].
 
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
index 1d49cea0334d1f281168481586d71e7f6fce8067..9ed2550277e65773a6788deb6913ae35d6a00f29 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
@@ -24,8 +24,8 @@ Prove: Mint_0[shift_sint32(a, i)] = 0.
 ------------------------------------------------------------
 
 Goal Assertion (file array_initialized.c, line 185):
-Let a = global(K_h1_26).
-Let a_1 = global(K_h2_27).
+Let a = global(K_h2_27).
+Let a_1 = global(K_h1_26).
 Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 499).
@@ -236,7 +236,7 @@ Assume {
   Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) ->
       (Mint_0[shift_sint32(a, i_1)] = 0))).
 }
-Prove: Mint_0[shift_sint32(a_1, i)] = Mint_0[shift_sint32(a, i)].
+Prove: Mint_0[shift_sint32(a, i)] = Mint_0[shift_sint32(a_1, i)].
 
 ------------------------------------------------------------
 ------------------------------------------------------------