diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index d26a185359c63000bc649fb424409153b1b211b0..f1c9fe315723eb5a9fb1907a677c0ec941ae086f 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -343,7 +343,7 @@ struct
     include Datatype.Pair (Memory) (References)
     let pretty_debug = pretty
     let top = Memory.top, References.empty
-    let _istop (m,r) = Memory.is_top m && References.is_empty r
+    let is_top (m,r) = Memory.is_top m && References.is_empty r
   end
 
   module BaseMap =
@@ -356,15 +356,17 @@ struct
     let find_or_top (state : t) (b : Base.t) =
       try find b state with Not_found -> V.top
 
+    (* Update or remove if top *)
+    let add (b : Base.t) (v : V.t) (state : t) =
+      if V.is_top v
+      then remove b state
+      else add b v state
+
     let remove_var (state : t) (v : Cil_types.varinfo) =
       remove (Base.of_varinfo v) state
 
     let remove_vars (state : t) (l : Cil_types.varinfo list) =
       List.fold_left remove_var state l
-
-    let remove_loc (state : t) (loc : Precise_locs.precise_location) =
-      let loc = Precise_locs.imprecise_location loc in
-      Locations.(Location_Bits.fold_bases remove loc.loc state)
   end
 
   include Datatype.Pair_with_collections
@@ -512,10 +514,13 @@ struct
       let oracle = convert_oracle oracle in
       write (fun m off -> Memory.overwrite ~oracle ~weak m off value) state dst
 
-  let erase ~oracle
+  let erase ~oracle ?(weak: bool option)
       (state : state) (dst : mdlocation) (b : Abstract_memory.bit): state =
-    let weak = not (Location.is_singleton dst)
-    and oracle = convert_oracle oracle in
+    let oracle = convert_oracle oracle
+    and weak = match weak with
+      | None -> not (Location.is_singleton dst)
+      | Some weak -> weak
+    in
     write (fun m off -> Memory.erase ~oracle ~weak m off b) state dst
 
   let reinforce
@@ -764,18 +769,18 @@ struct
     let (base_map,tracked) = state in
     BaseMap.remove_vars base_map vars, tracked
 
-  let logic_assign assign location (base_map,tracked as state) =
-    match assign with
-    | None -> BaseMap.remove_loc base_map location, tracked
-    | Some ((Frees _ | Allocates _), _) -> state
-    | Some (Assigns (_dest, sources), _pre_state) ->
-      match sources with
-      | [] ->
-        let dst = Location.of_precise_loc location in
-        let oracle = mk_oracle state in
-        erase ~oracle state dst Abstract_memory.Bit.numerical
-      | _ ->
-        BaseMap.remove_loc base_map location, tracked
+  let logic_assign assign location state =
+    let oracle = mk_oracle state
+    and dst = Location.of_precise_loc location
+    and b =
+      match assign with
+      | None
+      | Some (Frees _, _)
+      | Some (Allocates _, _)
+      | Some (Assigns (_, _ :: _), _) -> Abstract_memory.Bit.top
+      | Some (Assigns (_, []), _) -> Abstract_memory.Bit.numerical
+    in
+    erase ~oracle ~weak:true state dst b
 
   let reduce_by_papp env li _labels args positive state =
     match li.l_var_info.lv_name, args with
diff --git a/tests/builtins/oracle_multidim/alloc-vla.res.oracle b/tests/builtins/oracle_multidim/alloc-vla.res.oracle
deleted file mode 100644
index 2ce8b2b15361330cc266f0eb6e2ff76ec1f9db50..0000000000000000000000000000000000000000
--- a/tests/builtins/oracle_multidim/alloc-vla.res.oracle
+++ /dev/null
@@ -1,50 +0,0 @@
-12,19d11
-< [eva] alloc-vla.c:7: Call to builtin free
-< [eva:alarm] alloc-vla.c:7: Warning: 
-<   function free: precondition 'freeable' got status invalid.
-< [eva] alloc-vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] alloc-vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva:alarm] alloc-vla.c:8: Warning: 
-<   accessing left-value that contains escaping addresses.
-<   assert ¬\dangling(&a);
-24d15
-< [eva] alloc-vla.c:8: assertion 'Eva,dangling_pointer' got final status invalid.
-27,29c18
-<   __fc_heap_status ∈ [--..--]
-<   a ∈ ESCAPINGADDR
-<   __lengthof_a ∈ {4}
----
->   NON TERMINATING FUNCTION
-35,38c24
-< [from] Computing for function free <-f
-< [from] Done for function free
-< [from] Computing for function __fc_vla_free <-f
-< [from] Done for function __fc_vla_free
----
-> [from] Non-terminating function f (no dependencies)
-47,50d32
-< [from] Function __fc_vla_free:
-<   NO EFFECTS
-< [from] Function free:
-<   __fc_heap_status FROM __fc_heap_status (and SELF)
-52,53c34
-<   __fc_heap_status FROM __fc_heap_status; nondet (and SELF)
-<   \result FROM \nothing
----
->   NON TERMINATING - NO EFFECTS
-58c39
-<     __fc_heap_status; a; __lengthof_a
----
->     a; __lengthof_a
-60c41
-<     __fc_heap_status; nondet
----
->     \nothing
-62c43
-<     __fc_heap_status; t
----
->     t
-64c45
-<     __fc_heap_status; nondet
----
->     \nothing
diff --git a/tests/builtins/oracle_multidim/allocated.0.res.oracle b/tests/builtins/oracle_multidim/allocated.0.res.oracle
deleted file mode 100644
index 0424999e5132a337aefcdc31b48e8e45bf4008f2..0000000000000000000000000000000000000000
--- a/tests/builtins/oracle_multidim/allocated.0.res.oracle
+++ /dev/null
@@ -1,94 +0,0 @@
-96a97
-> [eva] allocated.c:73: Call to builtin malloc
-159,200d159
-< [eva] allocated.c:131: Frama_C_show_each: {0}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva:malloc] allocated.c:127: 
-<   resizing variable `__malloc_main_l127' (0..31) to fit 0..63
-< [eva] allocated.c:128: starting to merge loop iterations
-< [eva:alarm] allocated.c:129: Warning: out of bounds write. assert \valid(a + j);
-< [eva] allocated.c:131: Frama_C_show_each: {0; 1}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-< [eva] allocated.c:126: starting to merge loop iterations
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva:malloc] allocated.c:127: 
-<   resizing variable `__malloc_main_l127' (0..31/63) to fit 0..63/95
-< [eva] allocated.c:131: Frama_C_show_each: {0; 1; 2}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva:malloc] allocated.c:127: 
-<   resizing variable `__malloc_main_l127' (0..31/95) to fit 0..63/127
-< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva:malloc] allocated.c:127: 
-<   resizing variable `__malloc_main_l127' (0..31/127) to fit 0..63/159
-< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva:malloc] allocated.c:127: 
-<   resizing variable `__malloc_main_l127' (0..31/159) to fit 0..63/191
-< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva:malloc] allocated.c:127: 
-<   resizing variable `__malloc_main_l127' (0..31/191) to fit 0..63/319
-< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-208,217c167
-<   __fc_heap_status ∈ [--..--]
-<   i ∈ {10}
-<   j ∈ [1..2147483647]
-<   p ∈ ESCAPINGADDR
-<   k ∈ {8; 12}
-<   size ∈ [1..100]
-<   pb ∈ ESCAPINGADDR
-<   __retres ∈ {0}
-<   __malloc_w_main_l82[0..1] ∈ [7..2147483647] or UNINITIALIZED
-<                      [2] ∈ [7..27] or UNINITIALIZED
----
->   NON TERMINATING FUNCTION
-225,226c175
-< [from] Computing for function __fc_vla_free <-main
-< [from] Done for function __fc_vla_free
----
-> [from] Non-terminating function main (no dependencies)
-232,233d180
-< [from] Function __fc_vla_free:
-<   NO EFFECTS
-240,250c187
-<   __fc_heap_status FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l25 FROM __fc_heap_status
-<   __malloc_main_l36[0..1] FROM __fc_heap_status; nondet
-<   __malloc_main_l50[0..2] FROM __fc_heap_status; nondet
-<   __malloc_main_l63 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l73 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_w_main_l82[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l97[0] FROM __fc_heap_status; nondet
-<   __malloc_main_l114[0..3] FROM __fc_heap_status; nondet
-<   __malloc_main_l127[0..9] FROM \nothing (and SELF)
-<   \result FROM \nothing
----
->   NON TERMINATING - NO EFFECTS
-254,257c191,193
-<     __retres; __malloc_main_l25; __malloc_main_l36[0..1];
-<     __malloc_main_l50[0..2]; __malloc_main_l63; __malloc_main_l73;
-<     __malloc_w_main_l82[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
-<     __malloc_main_l127[0..9]
----
->     __malloc_main_l25; __malloc_main_l36[0..1]; __malloc_main_l50[0..2];
->     __malloc_main_l63; __malloc_main_l73; __malloc_w_main_l82[0..2];
->     __malloc_main_l97[0]; __malloc_main_l114[0..3]
-261,262c197
-<     __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0];
-<     __malloc_main_l127[0..9]
----
->     __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0]
diff --git a/tests/builtins/oracle_multidim/allocated.1.res.oracle b/tests/builtins/oracle_multidim/allocated.1.res.oracle
index 815e9e2aa583977a6c28a001bc36c0ee384a82f5..07f6b70bfde49280d8694fcf62a4517fa2e177d6 100644
--- a/tests/builtins/oracle_multidim/allocated.1.res.oracle
+++ b/tests/builtins/oracle_multidim/allocated.1.res.oracle
@@ -165,275 +165,58 @@
 < [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
 ---
 > [eva] allocated.c:81: Trace partitioning superposing up to 500 states
-646,693d763
-< [eva] allocated.c:131: Frama_C_show_each: {0}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_0
-< [eva] allocated.c:131: Frama_C_show_each: {1}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_0}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_1
-< [eva] allocated.c:131: Frama_C_show_each: {2}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_1}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_2
-< [eva] allocated.c:131: Frama_C_show_each: {3}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_2}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_3
-< [eva] allocated.c:131: Frama_C_show_each: {4}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_3}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_4
-< [eva] allocated.c:131: Frama_C_show_each: {5}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_4}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_5
-< [eva] allocated.c:131: Frama_C_show_each: {6}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_5}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_6
-< [eva] allocated.c:131: Frama_C_show_each: {7}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_6}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_7
-< [eva] allocated.c:131: Frama_C_show_each: {8}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_7}
-< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
-< [eva] allocated.c:127: allocating variable __malloc_main_l127_8
-< [eva] allocated.c:131: Frama_C_show_each: {9}
-< [eva] allocated.c:127: Call to builtin __fc_vla_free
-< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_8}
-701,792c771
-<   __fc_heap_status ∈ [--..--]
-<   i ∈ {10}
-<   j ∈ {10}
-<   p ∈ ESCAPINGADDR
-<   k ∈ {12}
-<   size ∈ [1..100]
-<   pb ∈ ESCAPINGADDR
-<   __retres ∈ {0}
-<   __malloc_main_l82_0 ∈ {7} or UNINITIALIZED
-<   __malloc_main_l82_1 ∈ {7} or UNINITIALIZED
-<   __malloc_main_l82_2[0] ∈ {14} or UNINITIALIZED
-<                      [1] ∈ {17} or UNINITIALIZED
-<   __malloc_main_l82_3[0] ∈ {14} or UNINITIALIZED
-<                      [1] ∈ {17} or UNINITIALIZED
-<   __malloc_main_l82_4[0] ∈ {14} or UNINITIALIZED
-<                      [1] ∈ {17} or UNINITIALIZED
-<   __malloc_main_l82_5[0] ∈ {14} or UNINITIALIZED
-<                      [1] ∈ {17} or UNINITIALIZED
-<   __malloc_main_l82_6[0] ∈ {14} or UNINITIALIZED
-<                      [1] ∈ {17} or UNINITIALIZED
+721,723c839,840
 <   __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
 <                      [1] ∈ {24} or UNINITIALIZED
 <                      [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_8[0] ∈ {21} or UNINITIALIZED
-<                      [1] ∈ {24} or UNINITIALIZED
-<                      [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_9[0] ∈ {21} or UNINITIALIZED
-<                      [1] ∈ {24} or UNINITIALIZED
-<                      [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_10[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_11[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_12[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_13[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_14[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_15[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_16[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_17[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_18[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_19[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_20[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_21[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_22[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_23[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_24[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_25[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_26[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_27[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_28[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_29[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
-<   __malloc_main_l82_30[0] ∈ {21} or UNINITIALIZED
-<                       [1] ∈ {24} or UNINITIALIZED
-<                       [2] ∈ {27} or UNINITIALIZED
 ---
->   NON TERMINATING FUNCTION
-800,801c779
-< [from] Computing for function __fc_vla_free <-main
-< [from] Done for function __fc_vla_free
----
-> [from] Non-terminating function main (no dependencies)
-807,808d784
-< [from] Function __fc_vla_free:
-<   NO EFFECTS
-815,872c791
-<   __fc_heap_status FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l25 FROM __fc_heap_status
-<   __malloc_main_l36[0..1] FROM __fc_heap_status; nondet
-<   __malloc_main_l50[0..1] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l50_0[0..1] FROM __fc_heap_status; nondet (and SELF)
-<                      [2] FROM __fc_heap_status; nondet
-<   __malloc_main_l63 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l63_0 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l63_1 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l63_2 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l73 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l73_0 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l73_1 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l73_2 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_0 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_1 FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_2[0..1] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_3[0..1] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_4[0..1] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_5[0..1] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_6[0..1] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
+>                      [1] ∈ {17} or UNINITIALIZED
+792a910,930
+>   __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_32[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_33[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_34[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_35[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_36[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+836c974
 <   __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_8[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_9[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_10[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_11[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_12[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_13[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_14[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_15[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_16[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_17[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_18[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_19[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_20[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_21[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_22[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_23[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_24[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_25[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_26[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_27[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_28[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_29[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l82_30[0..2] FROM __fc_heap_status; nondet (and SELF)
-<   __malloc_main_l97[0] FROM __fc_heap_status; nondet
-<   __malloc_main_l114[0..3] FROM __fc_heap_status; nondet
-<   __malloc_main_l127 FROM \nothing (and SELF)
-<   __malloc_main_l127_0[0..1] FROM \nothing (and SELF)
-<   __malloc_main_l127_1[0..2] FROM \nothing (and SELF)
-<   __malloc_main_l127_2[0..3] FROM \nothing (and SELF)
-<   __malloc_main_l127_3[0..4] FROM \nothing (and SELF)
-<   __malloc_main_l127_4[0..5] FROM \nothing (and SELF)
-<   __malloc_main_l127_5[0..6] FROM \nothing (and SELF)
-<   __malloc_main_l127_6[0..7] FROM \nothing (and SELF)
-<   __malloc_main_l127_7[0..8] FROM \nothing (and SELF)
-<   __malloc_main_l127_8[0..9] FROM \nothing (and SELF)
-<   \result FROM \nothing
 ---
->   NON TERMINATING - NO EFFECTS
-876,900c795,817
-<     __retres; __malloc_main_l25; __malloc_main_l36[0..1];
-<     __malloc_main_l50[0..1]; __malloc_main_l50_0[0..2]; __malloc_main_l63;
-<     __malloc_main_l63_0; __malloc_main_l63_1; __malloc_main_l63_2;
-<     __malloc_main_l73; __malloc_main_l73_0; __malloc_main_l73_1;
-<     __malloc_main_l73_2; __malloc_main_l82_0; __malloc_main_l82_1;
-<     __malloc_main_l82_2[0..1]; __malloc_main_l82_3[0..1];
-<     __malloc_main_l82_4[0..1]; __malloc_main_l82_5[0..1];
+>   __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
+859a998,1004
+>   __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_34[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
+883c1028
 <     __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
-<     __malloc_main_l82_8[0..2]; __malloc_main_l82_9[0..2];
-<     __malloc_main_l82_10[0..2]; __malloc_main_l82_11[0..2];
-<     __malloc_main_l82_12[0..2]; __malloc_main_l82_13[0..2];
-<     __malloc_main_l82_14[0..2]; __malloc_main_l82_15[0..2];
-<     __malloc_main_l82_16[0..2]; __malloc_main_l82_17[0..2];
-<     __malloc_main_l82_18[0..2]; __malloc_main_l82_19[0..2];
-<     __malloc_main_l82_20[0..2]; __malloc_main_l82_21[0..2];
-<     __malloc_main_l82_22[0..2]; __malloc_main_l82_23[0..2];
-<     __malloc_main_l82_24[0..2]; __malloc_main_l82_25[0..2];
-<     __malloc_main_l82_26[0..2]; __malloc_main_l82_27[0..2];
-<     __malloc_main_l82_28[0..2]; __malloc_main_l82_29[0..2];
-<     __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
-<     __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
-<     __malloc_main_l127_2[0..3]; __malloc_main_l127_3[0..4];
-<     __malloc_main_l127_4[0..5]; __malloc_main_l127_5[0..6];
-<     __malloc_main_l127_6[0..7]; __malloc_main_l127_7[0..8];
-<     __malloc_main_l127_8[0..9]
 ---
->     __malloc_main_l25; __malloc_main_l36[0..1]; __malloc_main_l50[0..1];
->     __malloc_main_l50_0[0..2]; __malloc_main_l63; __malloc_main_l63_0;
->     __malloc_main_l63_1; __malloc_main_l63_2; __malloc_main_l73;
->     __malloc_main_l73_0; __malloc_main_l73_1; __malloc_main_l73_2;
->     __malloc_main_l82_0; __malloc_main_l82_1; __malloc_main_l82_2[0..1];
->     __malloc_main_l82_3[0..1]; __malloc_main_l82_4[0..1];
->     __malloc_main_l82_5[0..1]; __malloc_main_l82_6[0..1];
->     __malloc_main_l82_7[0..1]; __malloc_main_l82_8[0..2];
->     __malloc_main_l82_9[0..2]; __malloc_main_l82_10[0..2];
->     __malloc_main_l82_11[0..2]; __malloc_main_l82_12[0..2];
->     __malloc_main_l82_13[0..2]; __malloc_main_l82_14[0..2];
->     __malloc_main_l82_15[0..2]; __malloc_main_l82_16[0..2];
->     __malloc_main_l82_17[0..2]; __malloc_main_l82_18[0..2];
->     __malloc_main_l82_19[0..2]; __malloc_main_l82_20[0..2];
->     __malloc_main_l82_21[0..2]; __malloc_main_l82_22[0..2];
->     __malloc_main_l82_23[0..2]; __malloc_main_l82_24[0..2];
->     __malloc_main_l82_25[0..2]; __malloc_main_l82_26[0..2];
->     __malloc_main_l82_27[0..2]; __malloc_main_l82_28[0..2];
->     __malloc_main_l82_29[0..2]; __malloc_main_l82_30[0..2];
->     __malloc_main_l82_31[0..2]; __malloc_main_l82_32[0..2];
->     __malloc_main_l82_33[0..2]; __malloc_main_l82_34[0..2];
->     __malloc_main_l82_35[0..2]; __malloc_main_l82_36[0..2];
->     __malloc_main_l82_37[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3]
-906,911c823
-<     __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0];
+>     __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
+895,896c1040,1045
+<     __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
 <     __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
-<     __malloc_main_l127_2[0..3]; __malloc_main_l127_3[0..4];
-<     __malloc_main_l127_4[0..5]; __malloc_main_l127_5[0..6];
-<     __malloc_main_l127_6[0..7]; __malloc_main_l127_7[0..8];
-<     __malloc_main_l127_8[0..9]
 ---
->     __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0]
+>     __malloc_main_l82_30[0..2]; __malloc_main_l82_31[0..2];
+>     __malloc_main_l82_32[0..2]; __malloc_main_l82_33[0..2];
+>     __malloc_main_l82_34[0..2]; __malloc_main_l82_35[0..2];
+>     __malloc_main_l82_36[0..2]; __malloc_main_l82_37[0..2];
+>     __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
+>     __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
diff --git a/tests/builtins/oracle_multidim/malloc-optimistic.res.oracle b/tests/builtins/oracle_multidim/malloc-optimistic.res.oracle
deleted file mode 100644
index 79eb036eb1ce329fa80e6de3db5a903bb7870692..0000000000000000000000000000000000000000
--- a/tests/builtins/oracle_multidim/malloc-optimistic.res.oracle
+++ /dev/null
@@ -1,3655 +0,0 @@
-16,19d15
-< [eva] malloc-optimistic.c:18: Frama_C_show_each_1_2: {0}
-< [eva] malloc-optimistic.c:18: Frama_C_show_each_1_2: {1}
-< [eva:alarm] malloc-optimistic.c:19: Warning: 
-<   out of bounds write. assert \valid(p + i);
-22,3402d17
-< [eva] malloc-optimistic.c:136: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:136: strong free on bases: {__malloc_main1_l17}
-< [eva] computing for function main2 <- main.
-<   Called from malloc-optimistic.c:137.
-< [eva] malloc-optimistic.c:26: Frama_C_show_each_2_1: {2}
-< [eva] malloc-optimistic.c:26: Frama_C_show_each_2_1: {1}
-< [eva] malloc-optimistic.c:27: Call to builtin malloc
-< [eva] malloc-optimistic.c:27: allocating variable __malloc_main2_l27
-< [eva] malloc-optimistic.c:27: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:27: 
-<   resizing variable `__malloc_main2_l27' (0..95) to fit 0..63
-< [eva] malloc-optimistic.c:28: Frama_C_show_each_2_2: {2}
-< [eva] malloc-optimistic.c:28: Frama_C_show_each_2_2: {1}
-< [eva:alarm] malloc-optimistic.c:29: Warning: 
-<   out of bounds write. assert \valid(p + i);
-< [eva] Recording results for main2
-< [eva] Done for function main2
-< [eva] malloc-optimistic.c:138: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:138: strong free on bases: {__malloc_main2_l27}
-< [eva] computing for function main3 <- main.
-<   Called from malloc-optimistic.c:139.
-< [eva] computing for function main_3_aux <- main3 <- main.
-<   Called from malloc-optimistic.c:48.
-< [eva] malloc-optimistic.c:34: Call to builtin malloc
-< [eva] malloc-optimistic.c:34: allocating variable __malloc_main_3_aux_l34
-< [eva] Recording results for main_3_aux
-< [eva] Done for function main_3_aux
-< [eva] computing for function main_3_aux <- main3 <- main.
-<   Called from malloc-optimistic.c:48.
-< [eva] malloc-optimistic.c:34: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:34: 
-<   resizing variable `__malloc_main_3_aux_l34' (0..31) to fit 0..63
-< [eva:alarm] malloc-optimistic.c:35: Warning: 
-<   out of bounds write. assert \valid(p + i);
-< [eva] Recording results for main_3_aux
-< [eva] Done for function main_3_aux
-< [eva] Recording results for main3
-< [eva] Done for function main3
-< [eva] malloc-optimistic.c:140: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:140: 
-<   strong free on bases: {__malloc_main_3_aux_l34}
-< [eva] computing for function main4 <- main.
-<   Called from malloc-optimistic.c:141.
-< [eva] computing for function main_4_aux <- main4 <- main.
-<   Called from malloc-optimistic.c:56.
-< [eva] malloc-optimistic.c:40: Call to builtin malloc
-< [eva] malloc-optimistic.c:40: allocating variable __malloc_main_4_aux_l40
-< [eva] Recording results for main_4_aux
-< [eva] Done for function main_4_aux
-< [eva] computing for function main_4_aux <- main4 <- main.
-<   Called from malloc-optimistic.c:56.
-< [eva] malloc-optimistic.c:40: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:40: 
-<   resizing variable `__malloc_main_4_aux_l40' (0..95) to fit 0..63
-< [eva] Recording results for main_4_aux
-< [eva] Done for function main_4_aux
-< [eva] Recording results for main4
-< [eva] Done for function main4
-< [eva] malloc-optimistic.c:142: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:142: 
-<   strong free on bases: {__malloc_main_4_aux_l40}
-< [eva] computing for function main5 <- main.
-<   Called from malloc-optimistic.c:144.
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva] malloc-optimistic.c:64: allocating variable __malloc_main5_l64
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31) to fit 0..63
-< [eva:alarm] malloc-optimistic.c:65: Warning: 
-<   out of bounds write. assert \valid(p + i);
-< [eva:alarm] malloc-optimistic.c:66: Warning: 
-<   out of bounds read. assert \valid_read(p + i);
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {0}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0] ∈ UNINITIALIZED
-<                     [1] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/63) to fit 0..63
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/63) to fit 0..95
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {1}
-<   k ∈ {-1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0] ∈ UNINITIALIZED
-<                     [1] ∈ {1}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {1}
-<   k ∈ {-1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..1] ∈ UNINITIALIZED
-<                     [2] ∈ {1}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/95) to fit 0..95
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/95) to fit 0..127
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {2}
-<   k ∈ {0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..1] ∈ UNINITIALIZED
-<                     [2] ∈ {2}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {2}
-<   k ∈ {0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..2] ∈ UNINITIALIZED
-<                     [3] ∈ {2}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/127) to fit 0..127
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/127) to fit 0..159
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {3}
-<   k ∈ {1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..2] ∈ UNINITIALIZED
-<                     [3] ∈ {3}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {3}
-<   k ∈ {1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..3] ∈ UNINITIALIZED
-<                     [4] ∈ {3}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/159) to fit 0..159
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/159) to fit 0..191
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {4}
-<   k ∈ {2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..3] ∈ UNINITIALIZED
-<                     [4] ∈ {4}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {4}
-<   k ∈ {2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..4] ∈ UNINITIALIZED
-<                     [5] ∈ {4}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/191) to fit 0..191
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/191) to fit 0..223
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {5}
-<   k ∈ {3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..4] ∈ UNINITIALIZED
-<                     [5] ∈ {5}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {5}
-<   k ∈ {3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..5] ∈ UNINITIALIZED
-<                     [6] ∈ {5}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/223) to fit 0..223
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/223) to fit 0..255
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {6}
-<   k ∈ {4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..5] ∈ UNINITIALIZED
-<                     [6] ∈ {6}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {6}
-<   k ∈ {4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..6] ∈ UNINITIALIZED
-<                     [7] ∈ {6}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/255) to fit 0..255
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/255) to fit 0..287
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {7}
-<   k ∈ {5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..6] ∈ UNINITIALIZED
-<                     [7] ∈ {7}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {7}
-<   k ∈ {5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..7] ∈ UNINITIALIZED
-<                     [8] ∈ {7}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/287) to fit 0..287
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/287) to fit 0..319
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {8}
-<   k ∈ {6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..7] ∈ UNINITIALIZED
-<                     [8] ∈ {8}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {8}
-<   k ∈ {6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..8] ∈ UNINITIALIZED
-<                     [9] ∈ {8}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/319) to fit 0..319
-< [eva] malloc-optimistic.c:64: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:64: 
-<   resizing variable `__malloc_main5_l64' (0..31/319) to fit 0..351
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {9}
-<   k ∈ {7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..8] ∈ UNINITIALIZED
-<                     [9] ∈ {9}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:67: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {10}
-<   p ∈ {{ &__malloc_main5_l64[0] }}
-<   j ∈ {9}
-<   k ∈ {7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main5_l64[0..9] ∈ UNINITIALIZED
-<                     [10] ∈ {9}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] malloc-optimistic.c:68: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:68: strong free on bases: {__malloc_main5_l64}
-< [eva] Recording results for main5
-< [eva] Done for function main5
-< [eva] computing for function main6 <- main.
-<   Called from malloc-optimistic.c:145.
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva] malloc-optimistic.c:77: allocating variable __malloc_main6_l77
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_main6_l77' (0..31) to fit 0..63
-< [eva:alarm] malloc-optimistic.c:78: Warning: 
-<   out of bounds write. assert \valid(p + i);
-< [eva:alarm] malloc-optimistic.c:79: Warning: 
-<   out of bounds read. assert \valid_read(p + i);
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {0}
-<   p ∈ {{ &__malloc_main6_l77[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main6_l77[0] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_main6_l77[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_main6_l77[0] ∈ UNINITIALIZED
-<                     [1] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: strong free on bases: {__malloc_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc:weak] malloc-optimistic.c:77: 
-<   marking variable `__malloc_main6_l77' as weak
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/63) to fit 0..63
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/63) to fit 0..95
-< [eva:alarm] malloc-optimistic.c:79: Warning: 
-<   accessing uninitialized left-value. assert \initialized(p + i);
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {1}
-<   k ∈ {-2; -1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {1}
-<   k ∈ {-1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0} or UNINITIALIZED
-<                       [2] ∈ {1} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/95) to fit 0..95
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/95) to fit 0..127
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {2}
-<   k ∈ {-1; 0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {2}
-<   k ∈ {0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1} or UNINITIALIZED
-<                       [3] ∈ {2} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/127) to fit 0..127
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/127) to fit 0..159
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {3}
-<   k ∈ {0; 1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {3}
-<   k ∈ {1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2} or UNINITIALIZED
-<                       [4] ∈ {3} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/159) to fit 0..159
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/159) to fit 0..191
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {4}
-<   k ∈ {1; 2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {4}
-<   k ∈ {2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3} or UNINITIALIZED
-<                       [5] ∈ {4} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/191) to fit 0..191
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/191) to fit 0..223
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {5}
-<   k ∈ {2; 3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {5}
-<   k ∈ {3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4} or UNINITIALIZED
-<                       [6] ∈ {5} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/223) to fit 0..223
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/223) to fit 0..255
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {6}
-<   k ∈ {3; 4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {6}
-<   k ∈ {4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5} or UNINITIALIZED
-<                       [7] ∈ {6} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/255) to fit 0..255
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/255) to fit 0..287
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {7}
-<   k ∈ {4; 5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {7}
-<   k ∈ {5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6} or UNINITIALIZED
-<                       [8] ∈ {7} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/287) to fit 0..287
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/287) to fit 0..319
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {8}
-<   k ∈ {5; 6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {8}
-<   k ∈ {6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7} or UNINITIALIZED
-<                       [9] ∈ {8} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/319) to fit 0..319
-< [eva] malloc-optimistic.c:77: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:77: 
-<   resizing variable `__malloc_w_main6_l77' (0..31/319) to fit 0..351
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {9}
-<   k ∈ {6; 7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:80: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {10}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }}
-<   j ∈ {9}
-<   k ∈ {7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:81: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:81: weak free on bases: {__malloc_w_main6_l77}
-< [eva] Recording results for main6
-< [eva] Done for function main6
-< [eva] computing for function main7 <- main.
-<   Called from malloc-optimistic.c:148.
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva] malloc-optimistic.c:90: allocating variable __malloc_main7_l90
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31) to fit 0..63
-< [eva:alarm] malloc-optimistic.c:91: Warning: 
-<   out of bounds write. assert \valid(p + i);
-< [eva:alarm] malloc-optimistic.c:92: Warning: 
-<   out of bounds read. assert \valid_read(p + i);
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {0}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0] ∈ UNINITIALIZED
-<                     [1] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/63) to fit 0..63
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/63) to fit 0..95
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {1}
-<   k ∈ {-1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0] ∈ UNINITIALIZED
-<                     [1] ∈ {1}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {1}
-<   k ∈ {-1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..1] ∈ UNINITIALIZED
-<                     [2] ∈ {1}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/95) to fit 0..95
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/95) to fit 0..127
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {2}
-<   k ∈ {0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..1] ∈ UNINITIALIZED
-<                     [2] ∈ {2}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {2}
-<   k ∈ {0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..2] ∈ UNINITIALIZED
-<                     [3] ∈ {2}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/127) to fit 0..127
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/127) to fit 0..159
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {3}
-<   k ∈ {1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..2] ∈ UNINITIALIZED
-<                     [3] ∈ {3}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {3}
-<   k ∈ {1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..3] ∈ UNINITIALIZED
-<                     [4] ∈ {3}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/159) to fit 0..159
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/159) to fit 0..191
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {4}
-<   k ∈ {2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..3] ∈ UNINITIALIZED
-<                     [4] ∈ {4}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {4}
-<   k ∈ {2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..4] ∈ UNINITIALIZED
-<                     [5] ∈ {4}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/191) to fit 0..191
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/191) to fit 0..223
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {5}
-<   k ∈ {3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..4] ∈ UNINITIALIZED
-<                     [5] ∈ {5}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {5}
-<   k ∈ {3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..5] ∈ UNINITIALIZED
-<                     [6] ∈ {5}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/223) to fit 0..223
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/223) to fit 0..255
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {6}
-<   k ∈ {4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..5] ∈ UNINITIALIZED
-<                     [6] ∈ {6}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {6}
-<   k ∈ {4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..6] ∈ UNINITIALIZED
-<                     [7] ∈ {6}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/255) to fit 0..255
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/255) to fit 0..287
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {7}
-<   k ∈ {5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..6] ∈ UNINITIALIZED
-<                     [7] ∈ {7}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {7}
-<   k ∈ {5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..7] ∈ UNINITIALIZED
-<                     [8] ∈ {7}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/287) to fit 0..287
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/287) to fit 0..319
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {8}
-<   k ∈ {6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..7] ∈ UNINITIALIZED
-<                     [8] ∈ {8}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {8}
-<   k ∈ {6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..8] ∈ UNINITIALIZED
-<                     [9] ∈ {8}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/319) to fit 0..319
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/319) to fit 0..351
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {9}
-<   k ∈ {7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..8] ∈ UNINITIALIZED
-<                     [9] ∈ {9}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {10}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {9}
-<   k ∈ {7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..9] ∈ UNINITIALIZED
-<                     [10] ∈ {9}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/351) to fit 0..351
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/351) to fit 0..383
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {10}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {10}
-<   k ∈ {8}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..9] ∈ UNINITIALIZED
-<                     [10] ∈ {10}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {11}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {10}
-<   k ∈ {8}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..10] ∈ UNINITIALIZED
-<                     [11] ∈ {10}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/383) to fit 0..383
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/383) to fit 0..415
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {11}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {11}
-<   k ∈ {9}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..10] ∈ UNINITIALIZED
-<                     [11] ∈ {11}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {12}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {11}
-<   k ∈ {9}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..11] ∈ UNINITIALIZED
-<                     [12] ∈ {11}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/415) to fit 0..415
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/415) to fit 0..447
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {12}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {12}
-<   k ∈ {10}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..11] ∈ UNINITIALIZED
-<                     [12] ∈ {12}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {13}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {12}
-<   k ∈ {10}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..12] ∈ UNINITIALIZED
-<                     [13] ∈ {12}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/447) to fit 0..447
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/447) to fit 0..479
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {13}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {13}
-<   k ∈ {11}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..12] ∈ UNINITIALIZED
-<                     [13] ∈ {13}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {14}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {13}
-<   k ∈ {11}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..13] ∈ UNINITIALIZED
-<                     [14] ∈ {13}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/479) to fit 0..479
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/479) to fit 0..511
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {14}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {14}
-<   k ∈ {12}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..13] ∈ UNINITIALIZED
-<                     [14] ∈ {14}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {14}
-<   k ∈ {12}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..14] ∈ UNINITIALIZED
-<                     [15] ∈ {14}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/511) to fit 0..511/543
-< [eva:alarm] malloc-optimistic.c:92: Warning: 
-<   accessing uninitialized left-value. assert \initialized(p + i);
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15; 16}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {15}
-<   k ∈ {13}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..14] ∈ UNINITIALIZED
-<                     [15..16] ∈ {15} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:88: starting to merge loop iterations
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/543) to fit 0..511/575
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15; 16; 17}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {15; 16}
-<   k ∈ {13; 14}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..14] ∈ UNINITIALIZED
-<                     [15..17] ∈ {15; 16} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/575) to fit 0..511/607
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15; 16; 17; 18}
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ {15; 16; 17}
-<   k ∈ {13; 14; 15}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..14] ∈ UNINITIALIZED
-<                     [15..18] ∈ {15; 16; 17} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] malloc-optimistic.c:90: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:90: 
-<   resizing variable `__malloc_main7_l90' (0..31/607) to fit 0..511/3231
-< [eva] malloc-optimistic.c:93: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ [15..100]
-<   p ∈ {{ &__malloc_main7_l90[0] }}
-<   j ∈ [15..99]
-<   k ∈ [13..97]
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main7_l90[0..14] ∈ UNINITIALIZED
-<                     [15..100] ∈ [15..99] or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:94: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:94: strong free on bases: {__malloc_main7_l90}
-< [eva] Recording results for main7
-< [eva] Done for function main7
-< [eva] computing for function main8 <- main.
-<   Called from malloc-optimistic.c:149.
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva] malloc-optimistic.c:103: allocating variable __malloc_main8_l103
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_main8_l103' (0..31) to fit 0..63
-< [eva:alarm] malloc-optimistic.c:104: Warning: 
-<   out of bounds write. assert \valid(p + i);
-< [eva:alarm] malloc-optimistic.c:105: Warning: 
-<   out of bounds read. assert \valid_read(p + i);
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {0}
-<   p ∈ {{ &__malloc_main8_l103[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main8_l103[0] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_main8_l103[0] }}
-<   j ∈ {0}
-<   k ∈ {-2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_main8_l103[0] ∈ UNINITIALIZED
-<                      [1] ∈ {0}
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   strong free on bases: {__malloc_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc:weak] malloc-optimistic.c:103: 
-<   marking variable `__malloc_main8_l103' as weak
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/63) to fit 0..63
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/63) to fit 0..95
-< [eva:alarm] malloc-optimistic.c:105: Warning: 
-<   accessing uninitialized left-value. assert \initialized(p + i);
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {1}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {1}
-<   k ∈ {-2; -1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {1}
-<   k ∈ {-1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0} or UNINITIALIZED
-<                        [2] ∈ {1} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/95) to fit 0..95
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/95) to fit 0..127
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {2}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {2}
-<   k ∈ {-1; 0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {2}
-<   k ∈ {0}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1} or UNINITIALIZED
-<                        [3] ∈ {2} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/127) to fit 0..127
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/127) to fit 0..159
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {3}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {3}
-<   k ∈ {0; 1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {3}
-<   k ∈ {1}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2} or UNINITIALIZED
-<                        [4] ∈ {3} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/159) to fit 0..159
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/159) to fit 0..191
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {4}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {4}
-<   k ∈ {1; 2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {4}
-<   k ∈ {2}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3} or UNINITIALIZED
-<                        [5] ∈ {4} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/191) to fit 0..191
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/191) to fit 0..223
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {5}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {5}
-<   k ∈ {2; 3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {5}
-<   k ∈ {3}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4} or UNINITIALIZED
-<                        [6] ∈ {5} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/223) to fit 0..223
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/223) to fit 0..255
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {6}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {6}
-<   k ∈ {3; 4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {6}
-<   k ∈ {4}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5} or UNINITIALIZED
-<                        [7] ∈ {6} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/255) to fit 0..255
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/255) to fit 0..287
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {7}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {7}
-<   k ∈ {4; 5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {7}
-<   k ∈ {5}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6} or UNINITIALIZED
-<                        [8] ∈ {7} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/287) to fit 0..287
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/287) to fit 0..319
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {8}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {8}
-<   k ∈ {5; 6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {8}
-<   k ∈ {6}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7} or UNINITIALIZED
-<                        [9] ∈ {8} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/319) to fit 0..319
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/319) to fit 0..351
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {9}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {9}
-<   k ∈ {6; 7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {10}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {9}
-<   k ∈ {7}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8} or UNINITIALIZED
-<                        [10] ∈ {9} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/351) to fit 0..351
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/351) to fit 0..383
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {10}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {10}
-<   k ∈ {7; 8}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {11}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {10}
-<   k ∈ {8}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9} or UNINITIALIZED
-<                        [11] ∈ {10} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/383) to fit 0..383
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/383) to fit 0..415
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {11}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {11}
-<   k ∈ {8; 9}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {12}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {11}
-<   k ∈ {9}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10} or UNINITIALIZED
-<                        [12] ∈ {11} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/415) to fit 0..415
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/415) to fit 0..447
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {12}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {12}
-<   k ∈ {9; 10}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {13}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {12}
-<   k ∈ {10}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11} or UNINITIALIZED
-<                        [13] ∈ {12} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/447) to fit 0..447
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/447) to fit 0..479
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {13}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {13}
-<   k ∈ {10; 11}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {14}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {13}
-<   k ∈ {11}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12} or UNINITIALIZED
-<                        [14] ∈ {13} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/479) to fit 0..479
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/479) to fit 0..511
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {14}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {14}
-<   k ∈ {11; 12}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13; 14} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {14}
-<   k ∈ {12}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13} or UNINITIALIZED
-<                        [15] ∈ {14} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/511) to fit 0..511/543
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15; 16}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {15}
-<   k ∈ {12; 13}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13; 14} or UNINITIALIZED
-<                        [15] ∈ {14; 15} or UNINITIALIZED
-<                        [16] ∈ {15} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:101: starting to merge loop iterations
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/543) to fit 0..511/575
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15; 16; 17}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {15; 16}
-<   k ∈ {12; 13; 14}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13; 14} or UNINITIALIZED
-<                        [15] ∈ {14; 15; 16} or UNINITIALIZED
-<                        [16..17] ∈ {15; 16} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/575) to fit 0..511/607
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ {15; 16; 17; 18}
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ {15; 16; 17}
-<   k ∈ {12; 13; 14; 15}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13; 14} or UNINITIALIZED
-<                        [15] ∈ {14; 15; 16; 17} or UNINITIALIZED
-<                        [16..18] ∈ {15; 16; 17} or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/607) to fit 0..511/3231
-< [eva] malloc-optimistic.c:106: 
-<   Frama_C_dump_each:
-<   # cvalue:
-<   v ∈ [--..--]
-<   i ∈ [15..100]
-<   p ∈ {{ &__malloc_w_main8_l103[0] }}
-<   j ∈ [15..99]
-<   k ∈ [12..97]
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ UNINITIALIZED
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13; 14} or UNINITIALIZED
-<                        [15] ∈ [14..99] or UNINITIALIZED
-<                        [16..100] ∈ [15..99] or UNINITIALIZED
-<   ==END OF DUMP==
-< [eva] malloc-optimistic.c:107: Call to builtin free
-< [eva:malloc] malloc-optimistic.c:107: 
-<   weak free on bases: {__malloc_w_main8_l103}
-< [eva] malloc-optimistic.c:103: Call to builtin malloc
-< [eva:malloc] malloc-optimistic.c:103: 
-<   resizing variable `__malloc_w_main8_l103' (0..31/3231) to fit 0..511/3231
-< [eva] Recording results for main8
-< [eva] Done for function main8
-< [eva] computing for function main9 <- main.
-<   Called from malloc-optimistic.c:150.
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:119: allocating variable __malloc_main9_l119
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {0}, {{ &__malloc_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {0}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva:malloc:weak] malloc-optimistic.c:119: 
-<   marking variable `__malloc_main9_l119' as weak
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {1}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {-20; 1}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {2}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {-20; 1; 2}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {3}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {-20; 1; 2; 3}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {4}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {-20; 1; 2; 3; 4}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {5}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {-20; 1; 2; 3; 4; 5}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {6}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {-20; 1; 2; 3; 4; 5; 6}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {7}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: {-20; 1; 2; 3; 4; 5; 6; 7}
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {8}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..8]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {9}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..9]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {10}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..10]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {11}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..11]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {12}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..12]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {13}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..13]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {14}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..14]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {15}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..15]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {16}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..16]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {17}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..17]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {18}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..18]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {19}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..19]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {20}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..20]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {21}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..21]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {22}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..22]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {23}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..23]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {24}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..24]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {25}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..25]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {26}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..26]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {27}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..27]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {28}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..28]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {29}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..29]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {30}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..30]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:118: starting to merge loop iterations
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {30; 31}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..31]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: {30; 31; 32}, {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..32]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: [30..99], {{ &__malloc_w_main9_l119 }}
-< [eva] malloc-optimistic.c:122: Frama_C_show_each: [-20..99]
-< [eva] computing for function main9_aux <- main9 <- main.
-<   Called from malloc-optimistic.c:123.
-< [eva] Recording results for main9_aux
-< [eva] Done for function main9_aux
-< [eva] malloc-optimistic.c:119: Call to builtin malloc
-< [eva] malloc-optimistic.c:120: 
-<   Frama_C_show_each: [30..99], {{ &__malloc_w_main9_l119 }}
-< [eva] Recording results for main9
-< [eva] Done for function main9
-3406,3407d20
-< [eva:final-states] Values at end of function main9_aux:
-<   __malloc_w_main9_l119 ∈ [-20..99] or UNINITIALIZED
-3409,3492c22
-<   i ∈ {0; 1}
-<   p ∈ {{ &__malloc_main1_l17[0] }}
-<   __retres ∈ {{ (void *)&__malloc_main1_l17 }}
-<   __malloc_main1_l17[0] ∈ {0} or UNINITIALIZED
-<                     [1] ∈ {1}
-< [eva:final-states] Values at end of function main2:
-<   i ∈ {1; 2}
-<   p ∈ {{ &__malloc_main2_l27[0] }}
-<   __retres ∈ {{ (void *)&__malloc_main2_l27 }}
-<   __malloc_main2_l27[0] ∈ UNINITIALIZED
-<                     [1] ∈ {1} or UNINITIALIZED
-<                     [2] ∈ {2}
-< [eva:final-states] Values at end of function main5:
-<   i ∈ {9; 10}
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ {0}
-< [eva:final-states] Values at end of function main6:
-<   i ∈ {9; 10}
-<   p ∈ {{ &__malloc_w_main6_l77[0] }} or ESCAPINGADDR
-<   __retres ∈ {0}
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-< [eva:final-states] Values at end of function main7:
-<   i ∈ [14..100]
-<   p ∈ ESCAPINGADDR
-<   __retres ∈ {0}
-< [eva:final-states] Values at end of function main8:
-<   i ∈ [14..100]
-<   p ∈ {{ &__malloc_w_main8_l103[0] }} or ESCAPINGADDR
-<   __retres ∈ {0}
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13; 14} or UNINITIALIZED
-<                        [15] ∈ [14..99] or UNINITIALIZED
-<                        [16..100] ∈ [15..99] or UNINITIALIZED
-< [eva:final-states] Values at end of function main9:
-<   p ∈ {{ &__malloc_w_main9_l119 }}
-<   __retres ∈ {0}
-<   __malloc_w_main9_l119 ∈ [-20..99] or UNINITIALIZED
-< [eva:final-states] Values at end of function main_3_aux:
-<   p ∈ {{ &__malloc_main_3_aux_l34[0] }}
-<   __retres ∈ {{ (void *)&__malloc_main_3_aux_l34 }}
-<   __malloc_main_3_aux_l34[0] ∈ {0} or UNINITIALIZED
-<                          [1] ∈ {1}
-< [eva:final-states] Values at end of function main3:
-<   i ∈ {0; 1}
-<   p ∈ {{ &__malloc_main_3_aux_l34[0] }}
-<   __retres ∈ {{ (void *)&__malloc_main_3_aux_l34 }}
-<   __malloc_main_3_aux_l34[0] ∈ {0} or UNINITIALIZED
-<                          [1] ∈ {1}
-< [eva:final-states] Values at end of function main_4_aux:
-<   p ∈ {{ &__malloc_main_4_aux_l40[0] }}
-<   __retres ∈ {{ (void *)&__malloc_main_4_aux_l40 }}
-<   __malloc_main_4_aux_l40[0] ∈ UNINITIALIZED
-<                          [1] ∈ {1} or UNINITIALIZED
-<                          [2] ∈ {2}
-< [eva:final-states] Values at end of function main4:
-<   i ∈ {1; 2}
-<   p ∈ {{ &__malloc_main_4_aux_l40[0] }}
-<   __retres ∈ {{ (void *)&__malloc_main_4_aux_l40 }}
-<   __malloc_main_4_aux_l40[0] ∈ UNINITIALIZED
-<                          [1] ∈ {1} or UNINITIALIZED
-<                          [2] ∈ {2}
----
->   NON TERMINATING FUNCTION
-3494,3525c24
-<   p ∈ ESCAPINGADDR
-<   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
-<                       [1] ∈ {0; 1} or UNINITIALIZED
-<                       [2] ∈ {1; 2} or UNINITIALIZED
-<                       [3] ∈ {2; 3} or UNINITIALIZED
-<                       [4] ∈ {3; 4} or UNINITIALIZED
-<                       [5] ∈ {4; 5} or UNINITIALIZED
-<                       [6] ∈ {5; 6} or UNINITIALIZED
-<                       [7] ∈ {6; 7} or UNINITIALIZED
-<                       [8] ∈ {7; 8} or UNINITIALIZED
-<                       [9] ∈ {8; 9} or UNINITIALIZED
-<                       [10] ∈ {9} or UNINITIALIZED
-<   __malloc_w_main8_l103[0] ∈ UNINITIALIZED
-<                        [1] ∈ {0; 1} or UNINITIALIZED
-<                        [2] ∈ {1; 2} or UNINITIALIZED
-<                        [3] ∈ {2; 3} or UNINITIALIZED
-<                        [4] ∈ {3; 4} or UNINITIALIZED
-<                        [5] ∈ {4; 5} or UNINITIALIZED
-<                        [6] ∈ {5; 6} or UNINITIALIZED
-<                        [7] ∈ {6; 7} or UNINITIALIZED
-<                        [8] ∈ {7; 8} or UNINITIALIZED
-<                        [9] ∈ {8; 9} or UNINITIALIZED
-<                        [10] ∈ {9; 10} or UNINITIALIZED
-<                        [11] ∈ {10; 11} or UNINITIALIZED
-<                        [12] ∈ {11; 12} or UNINITIALIZED
-<                        [13] ∈ {12; 13} or UNINITIALIZED
-<                        [14] ∈ {13; 14} or UNINITIALIZED
-<                        [15] ∈ [14..99] or UNINITIALIZED
-<                        [16..100] ∈ [15..99] or UNINITIALIZED
-<   __malloc_w_main9_l119 ∈ [-20..99] or UNINITIALIZED
-< [from] Computing for function main9_aux
-< [from] Done for function main9_aux
----
->   NON TERMINATING FUNCTION
-3528a28
-> [from] Non-terminating function main1 (no dependencies)
-3530,3551d29
-< [from] Computing for function main2
-< [from] Done for function main2
-< [from] Computing for function main5
-< [from] Computing for function free <-main5
-< [from] Done for function free
-< [from] Done for function main5
-< [from] Computing for function main6
-< [from] Done for function main6
-< [from] Computing for function main7
-< [from] Done for function main7
-< [from] Computing for function main8
-< [from] Done for function main8
-< [from] Computing for function main9
-< [from] Done for function main9
-< [from] Computing for function main_3_aux
-< [from] Done for function main_3_aux
-< [from] Computing for function main3
-< [from] Done for function main3
-< [from] Computing for function main_4_aux
-< [from] Done for function main_4_aux
-< [from] Computing for function main4
-< [from] Done for function main4
-3552a31
-> [from] Non-terminating function main (no dependencies)
-3556,3559d34
-< [from] Function free:
-<   NO EFFECTS
-< [from] Function main9_aux:
-<   __malloc_w_main9_l119 FROM p (and SELF)
-3563,3594c38
-<   __malloc_main1_l17[0..1] FROM v (and SELF)
-<   \result FROM \nothing
-< [from] Function main2:
-<   __malloc_main2_l27[1..2] FROM v (and SELF)
-<   \result FROM \nothing
-< [from] Function main5:
-<   __malloc_main5_l64[0..10] FROM v (and SELF)
-<   \result FROM \nothing
-< [from] Function main6:
-<   __malloc_w_main6_l77[0..10] FROM v (and SELF)
-<   \result FROM \nothing
-< [from] Function main7:
-<   __malloc_main7_l90[0..100] FROM v (and SELF)
-<   \result FROM \nothing
-< [from] Function main8:
-<   __malloc_w_main8_l103[0..100] FROM v (and SELF)
-<   \result FROM \nothing
-< [from] Function main9:
-<   __malloc_w_main9_l119 FROM \nothing (and SELF)
-<   \result FROM \nothing
-< [from] Function main_3_aux:
-<   __malloc_main_3_aux_l34[0..1] FROM i (and SELF)
-<   \result FROM \nothing
-< [from] Function main3:
-<   __malloc_main_3_aux_l34[0..1] FROM v (and SELF)
-<   \result FROM \nothing
-< [from] Function main_4_aux:
-<   __malloc_main_4_aux_l40[1..2] FROM i (and SELF)
-<   \result FROM \nothing
-< [from] Function main4:
-<   __malloc_main_4_aux_l40[1..2] FROM v (and SELF)
-<   \result FROM \nothing
----
->   NON TERMINATING - NO EFFECTS
-3596,3604c40
-<   __malloc_main1_l17[0..1] FROM v (and SELF)
-<   __malloc_main2_l27[1..2] FROM v (and SELF)
-<   __malloc_main_3_aux_l34[0..1] FROM v (and SELF)
-<   __malloc_main_4_aux_l40[1..2] FROM v (and SELF)
-<   __malloc_main5_l64[0..10] FROM v (and SELF)
-<   __malloc_w_main6_l77[0..10] FROM v (and SELF)
-<   __malloc_main7_l90[0..100] FROM v (and SELF)
-<   __malloc_w_main8_l103[0..100] FROM v (and SELF)
-<   __malloc_w_main9_l119 FROM \nothing (and SELF)
----
->   NON TERMINATING - NO EFFECTS
-3606,3609d41
-< [inout] Out (internal) for function main9_aux:
-<     __malloc_w_main9_l119
-< [inout] Inputs for function main9_aux:
-<     \nothing
-3611c43
-<     i; p; __retres; __malloc_main1_l17[0..1]
----
->     i; p
-3614,3653d45
-< [inout] Out (internal) for function main2:
-<     i; p; __retres; __malloc_main2_l27[1..2]
-< [inout] Inputs for function main2:
-<     v
-< [inout] Out (internal) for function main5:
-<     i; p; j; k; __retres; __malloc_main5_l64[0..10]
-< [inout] Inputs for function main5:
-<     v; __malloc_main5_l64[0..10]
-< [inout] Out (internal) for function main6:
-<     i; p; j; k; __retres; __malloc_w_main6_l77[0..10]
-< [inout] Inputs for function main6:
-<     v; __malloc_w_main6_l77[0..10]
-< [inout] Out (internal) for function main7:
-<     i; p; j; k; __retres; __malloc_main7_l90[0..100]
-< [inout] Inputs for function main7:
-<     v; __malloc_main7_l90[0..100]
-< [inout] Out (internal) for function main8:
-<     i; p; j; k; __retres; __malloc_w_main8_l103[0..100]
-< [inout] Inputs for function main8:
-<     v; __malloc_w_main8_l103[0..100]
-< [inout] Out (internal) for function main9:
-<     p; j; __retres; __malloc_w_main9_l119
-< [inout] Inputs for function main9:
-<     __malloc_w_main9_l119
-< [inout] Out (internal) for function main_3_aux:
-<     p; __retres; __malloc_main_3_aux_l34[0..1]
-< [inout] Inputs for function main_3_aux:
-<     \nothing
-< [inout] Out (internal) for function main3:
-<     i; p; __retres; __malloc_main_3_aux_l34[0..1]
-< [inout] Inputs for function main3:
-<     v
-< [inout] Out (internal) for function main_4_aux:
-<     p; __retres; __malloc_main_4_aux_l40[1..2]
-< [inout] Inputs for function main_4_aux:
-<     \nothing
-< [inout] Out (internal) for function main4:
-<     i; p; __retres; __malloc_main_4_aux_l40[1..2]
-< [inout] Inputs for function main4:
-<     v
-3655,3659c47
-<     p; __malloc_main1_l17[0..1]; __malloc_main2_l27[1..2];
-<     __malloc_main_3_aux_l34[0..1]; __malloc_main_4_aux_l40[1..2];
-<     __malloc_main5_l64[0..10]; __malloc_w_main6_l77[0..10];
-<     __malloc_main7_l90[0..100]; __malloc_w_main8_l103[0..100];
-<     __malloc_w_main9_l119
----
->     p
-3661,3663c49
-<     v; __malloc_main5_l64[0..10]; __malloc_w_main6_l77[0..10];
-<     __malloc_main7_l90[0..100]; __malloc_w_main8_l103[0..100];
-<     __malloc_w_main9_l119
----
->     v
diff --git a/tests/builtins/oracle_multidim/vla.res.oracle b/tests/builtins/oracle_multidim/vla.res.oracle
deleted file mode 100644
index f058f8854e0abca9a895e4b66ed244b46013ce8c..0000000000000000000000000000000000000000
--- a/tests/builtins/oracle_multidim/vla.res.oracle
+++ /dev/null
@@ -1,138 +0,0 @@
-12,14d11
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-17,106d13
-< [eva] vla.c:20: freeing automatic bases: {__malloc_f_l6}
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: resizing variable `__malloc_f_l6' (0..63) to fit 0..95
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva:alarm] vla.c:8: Warning: out of bounds write. assert \valid(t + i);
-< [eva:alarm] vla.c:9: Warning: out of bounds read. assert \valid_read(t + i);
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: resizing variable `__malloc_f_l6' (0..63/95) to fit 0..127
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: 
-<   resizing variable `__malloc_f_l6' (0..63/127) to fit 0..159
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: 
-<   resizing variable `__malloc_f_l6' (0..63/159) to fit 0..191
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: 
-<   resizing variable `__malloc_f_l6' (0..63/191) to fit 0..223
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: 
-<   resizing variable `__malloc_f_l6' (0..63/223) to fit 0..255
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: 
-<   resizing variable `__malloc_f_l6' (0..63/255) to fit 0..287
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-< [eva] computing for function f <- main.
-<   Called from vla.c:20.
-< [eva] vla.c:6: Call to builtin __fc_vla_alloc
-< [eva:malloc] vla.c:6: 
-<   resizing variable `__malloc_f_l6' (0..63/287) to fit 0..319
-< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
-< [eva] vla.c:6: Call to builtin __fc_vla_free
-< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
-< [eva] Recording results for f
-< [eva] Done for function f
-< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
-111,112c18
-<   t ∈ ESCAPINGADDR
-<   __lengthof_t ∈ [2..10]
----
->   NON TERMINATING FUNCTION
-114c20
-<   i ∈ {10}
----
->   NON TERMINATING FUNCTION
-118,119c24
-< [from] Computing for function __fc_vla_free <-f
-< [from] Done for function __fc_vla_free
----
-> [from] Non-terminating function f (no dependencies)
-121a27
-> [from] Non-terminating function main (no dependencies)
-127,128d32
-< [from] Function __fc_vla_free:
-<   NO EFFECTS
-130c34
-<   __malloc_f_l6[1..9] FROM i (and SELF)
----
->   NON TERMINATING - NO EFFECTS
-132c36
-<   __malloc_f_l6[1..9] FROM \nothing (and SELF)
----
->   NON TERMINATING - NO EFFECTS
-135c39
-<     t; __lengthof_t; __malloc_f_l6[1..9]
----
->     t; __lengthof_t
-137c41
-<     __malloc_f_l6[1..9]
----
->     \nothing
-139c43
-<     i; __malloc_f_l6[1..9]
----
->     i
-141c45
-<     __malloc_f_l6[1..9]
----
->     \nothing
diff --git a/tests/value/oracle_multidim/multidim.res.oracle b/tests/value/oracle_multidim/multidim.res.oracle
index 1002afddb9f7cdb7e089830942e80ae6d9262255..89bd56baa46f5d074acf97874916faac570f71d0 100644
--- a/tests/value/oracle_multidim/multidim.res.oracle
+++ b/tests/value/oracle_multidim/multidim.res.oracle
@@ -1,2 +1,2 @@
-4d3
+2d1
 < [eva:experimental] Warning: The multidim domain is experimental.