diff --git a/tests/builtins/oracle/alloc_weak.res.oracle b/tests/builtins/oracle/alloc_weak.res.oracle
index 8a75c2737771cbf31721f82e0c5357668bcef26f..14c99ac21dce40ed9e7ac58e24aa5776d23bcb9c 100644
--- a/tests/builtins/oracle/alloc_weak.res.oracle
+++ b/tests/builtins/oracle/alloc_weak.res.oracle
@@ -41,14 +41,22 @@
   Called from tests/builtins/alloc_weak.c:73.
 [eva] tests/builtins/alloc_weak.c:37: Call to builtin malloc
 [eva] tests/builtins/alloc_weak.c:37: allocating variable __malloc_main2_l37
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 100 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 200 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 300 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 400 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 500 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 600 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 700 states
+[eva] tests/builtins/alloc_weak.c:40: 
+  Semantic level unrolling superposing up to 800 states
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
diff --git a/tests/builtins/oracle/allocated.1.res.oracle b/tests/builtins/oracle/allocated.1.res.oracle
index 7369e0f0ee70bff238f2ffa8f3112bfd4fef5ac0..0d4702a132229cc2c69b9b8ae06fb02ddf1d7786 100644
--- a/tests/builtins/oracle/allocated.1.res.oracle
+++ b/tests/builtins/oracle/allocated.1.res.oracle
@@ -191,64 +191,64 @@
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_6
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_6}
+  strong free on bases: {__malloc_main_l82_2}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_5}
+  strong free on bases: {__malloc_main_l82_3}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_4}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_3}
+  strong free on bases: {__malloc_main_l82_5}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_2}
+  strong free on bases: {__malloc_main_l82_6}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_6}
+  strong free on bases: {__malloc_main_l82_2}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_5}
+  strong free on bases: {__malloc_main_l82_3}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_4}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_3}
+  strong free on bases: {__malloc_main_l82_5}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_2}
+  strong free on bases: {__malloc_main_l82_6}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_6}
+  strong free on bases: {__malloc_main_l82_2}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_5}
+  strong free on bases: {__malloc_main_l82_3}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_4}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_3}
+  strong free on bases: {__malloc_main_l82_5}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_2}
+  strong free on bases: {__malloc_main_l82_6}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_6}
+  strong free on bases: {__malloc_main_l82_2}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_5}
+  strong free on bases: {__malloc_main_l82_3}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_4}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_3}
+  strong free on bases: {__malloc_main_l82_5}
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
-  strong free on bases: {__malloc_main_l82_2}
+  strong free on bases: {__malloc_main_l82_6}
 [eva] tests/builtins/allocated.c:82: 
   Call to builtin Frama_C_malloc_fresh for function malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
@@ -321,10 +321,13 @@
 [eva] tests/builtins/allocated.c:82: 
   Call to builtin Frama_C_malloc_fresh for function malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_30
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
+[eva] tests/builtins/allocated.c:84: 
+  Semantic level unrolling superposing up to 100 states
+[eva] tests/builtins/allocated.c:84: 
+  Semantic level unrolling superposing up to 200 states
+[eva] :0: Semantic level unrolling superposing up to 300 states
+[eva] tests/builtins/allocated.c:84: 
+  Semantic level unrolling superposing up to 400 states
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_30}
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 649c1f67a8f6a0006d1ee7a14c2927b14c3e86d6..6976af91e177e1561a61388b9e0d12e64314e244 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -78,7 +78,8 @@
 [eva] Done for function many
 [eva] computing for function init <- main <- main_all.
   Called from tests/builtins/memcpy.c:65.
-[eva] Semantic level unrolling superposing up to 100 states
+[eva] tests/builtins/memcpy.c:20: 
+  Semantic level unrolling superposing up to 100 states
 [eva] Recording results for init
 [from] Computing for function init
 [from] Done for function init
diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle
index 7f2845785857295d82991f7f7c3606adf573ba0f..facf3d7f3a3a3e0b1b85fec505165e2a5f702320 100644
--- a/tests/builtins/oracle/realloc_multiple.1.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle
@@ -81,16 +81,20 @@
   __fc_mbtowc_state âˆˆ [--..--]
   __fc_wctomb_state âˆˆ [--..--]
   Frama_C_entropy_source âˆˆ [--..--]
-  q âˆˆ {{ &__malloc_main1_l9[0] }}
-  r âˆˆ {{ &__malloc_main1_l12[0] }}
-  p âˆˆ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }}
+  q âˆˆ {{ &__malloc_main1_l9[0] }} or ESCAPINGADDR
+  r âˆˆ {{ &__malloc_main1_l12[0] }} or ESCAPINGADDR
+  p âˆˆ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }} or ESCAPINGADDR
   x âˆˆ {0; 1}
-  s âˆˆ {0}
+  s âˆˆ {{ &__realloc_main1_l23[0] ; &__realloc_main1_l23_0[0] }}
   v âˆˆ {1}
   S_0___fc_env[0..1] âˆˆ [--..--]
   S_1___fc_env[0..1] âˆˆ [--..--]
   __malloc_main1_l9[0..4] âˆˆ {5}
   __malloc_main1_l12[0..5] âˆˆ {6}
+  __realloc_main1_l23[0..5] âˆˆ {6}
+                     [6] âˆˆ UNINITIALIZED
+  __realloc_main1_l23_0[0..4] âˆˆ {5}
+                       [5..6] âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva] tests/builtins/realloc_multiple.c:25: 
   Frama_C_dump_each:
@@ -108,28 +112,24 @@
   __fc_mbtowc_state âˆˆ [--..--]
   __fc_wctomb_state âˆˆ [--..--]
   Frama_C_entropy_source âˆˆ [--..--]
-  q âˆˆ {{ &__malloc_main1_l9[0] }} or ESCAPINGADDR
-  r âˆˆ {{ &__malloc_main1_l12[0] }} or ESCAPINGADDR
-  p âˆˆ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }} or ESCAPINGADDR
+  q âˆˆ {{ &__malloc_main1_l9[0] }}
+  r âˆˆ {{ &__malloc_main1_l12[0] }}
+  p âˆˆ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }}
   x âˆˆ {0; 1}
-  s âˆˆ {{ &__realloc_main1_l23[0] ; &__realloc_main1_l23_0[0] }}
+  s âˆˆ {0}
   v âˆˆ {1}
   S_0___fc_env[0..1] âˆˆ [--..--]
   S_1___fc_env[0..1] âˆˆ [--..--]
   __malloc_main1_l9[0..4] âˆˆ {5}
   __malloc_main1_l12[0..5] âˆˆ {6}
-  __realloc_main1_l23[0..5] âˆˆ {6}
-                     [6] âˆˆ UNINITIALIZED
-  __realloc_main1_l23_0[0..4] âˆˆ {5}
-                       [5..6] âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva] tests/builtins/realloc_multiple.c:26: Call to builtin free
 [eva] tests/builtins/realloc_multiple.c:26: 
   function free: precondition 'freeable' got status valid.
-[eva:malloc] tests/builtins/realloc_multiple.c:26: strong free on bases: {}
-[eva] tests/builtins/realloc_multiple.c:26: Call to builtin free
 [eva:malloc] tests/builtins/realloc_multiple.c:26: 
   weak free on bases: {__realloc_main1_l23, __realloc_main1_l23_0}
+[eva] tests/builtins/realloc_multiple.c:26: Call to builtin free
+[eva:malloc] tests/builtins/realloc_multiple.c:26: strong free on bases: {}
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
@@ -212,16 +212,24 @@
   __fc_mbtowc_state âˆˆ [--..--]
   __fc_wctomb_state âˆˆ [--..--]
   Frama_C_entropy_source âˆˆ [--..--]
-  q âˆˆ {{ &__malloc_main2_l30[0] }}
-  r âˆˆ {{ &__malloc_main2_l33[0] }}
-  p âˆˆ {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }}
+  q âˆˆ {{ &__malloc_main2_l30[0] }} or ESCAPINGADDR
+  r âˆˆ {{ &__malloc_main2_l33[0] }} or ESCAPINGADDR
+  p âˆˆ
+   {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }} or ESCAPINGADDR
   x âˆˆ {0; 1; 2}
-  s âˆˆ {0}
+  s âˆˆ
+   {{ &__realloc_main2_l45[0] ; &__realloc_main2_l45_0[0] ;
+      &__realloc_main2_l45_1[0] }}
   v âˆˆ {2}
   S_0___fc_env[0..1] âˆˆ [--..--]
   S_1___fc_env[0..1] âˆˆ [--..--]
   __malloc_main2_l30[0..4] âˆˆ {7}
   __malloc_main2_l33[0..5] âˆˆ {8}
+  __realloc_main2_l45[0..5] âˆˆ {8}
+                     [6] âˆˆ UNINITIALIZED
+  __realloc_main2_l45_0[0..4] âˆˆ {7}
+                       [5..6] âˆˆ UNINITIALIZED
+  __realloc_main2_l45_1[0..6] âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva] tests/builtins/realloc_multiple.c:47: 
   Frama_C_dump_each:
@@ -239,33 +247,25 @@
   __fc_mbtowc_state âˆˆ [--..--]
   __fc_wctomb_state âˆˆ [--..--]
   Frama_C_entropy_source âˆˆ [--..--]
-  q âˆˆ {{ &__malloc_main2_l30[0] }} or ESCAPINGADDR
-  r âˆˆ {{ &__malloc_main2_l33[0] }} or ESCAPINGADDR
-  p âˆˆ
-   {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }} or ESCAPINGADDR
+  q âˆˆ {{ &__malloc_main2_l30[0] }}
+  r âˆˆ {{ &__malloc_main2_l33[0] }}
+  p âˆˆ {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }}
   x âˆˆ {0; 1; 2}
-  s âˆˆ
-   {{ &__realloc_main2_l45[0] ; &__realloc_main2_l45_0[0] ;
-      &__realloc_main2_l45_1[0] }}
+  s âˆˆ {0}
   v âˆˆ {2}
   S_0___fc_env[0..1] âˆˆ [--..--]
   S_1___fc_env[0..1] âˆˆ [--..--]
   __malloc_main2_l30[0..4] âˆˆ {7}
   __malloc_main2_l33[0..5] âˆˆ {8}
-  __realloc_main2_l45[0..5] âˆˆ {8}
-                     [6] âˆˆ UNINITIALIZED
-  __realloc_main2_l45_0[0..4] âˆˆ {7}
-                       [5..6] âˆˆ UNINITIALIZED
-  __realloc_main2_l45_1[0..6] âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva] tests/builtins/realloc_multiple.c:48: Call to builtin free
 [eva] tests/builtins/realloc_multiple.c:48: 
   function free: precondition 'freeable' got status valid.
-[eva:malloc] tests/builtins/realloc_multiple.c:48: strong free on bases: {}
-[eva] tests/builtins/realloc_multiple.c:48: Call to builtin free
 [eva:malloc] tests/builtins/realloc_multiple.c:48: 
   weak free on bases: {__realloc_main2_l45, __realloc_main2_l45_0,
                        __realloc_main2_l45_1}
+[eva] tests/builtins/realloc_multiple.c:48: Call to builtin free
+[eva:malloc] tests/builtins/realloc_multiple.c:48: strong free on bases: {}
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
@@ -312,8 +312,8 @@
   __fc_wctomb_state âˆˆ [--..--]
   Frama_C_entropy_source âˆˆ [--..--]
   p âˆˆ {{ &__malloc_main3_l52 }}
-  q âˆˆ {{ &__malloc_main3_l53_0 }}
-  r âˆˆ {{ NULL ; &__malloc_main3_l52 ; &__malloc_main3_l53_0 }}
+  q âˆˆ {{ &__malloc_main3_l53 }}
+  r âˆˆ {{ NULL ; &__malloc_main3_l52 ; &__malloc_main3_l53 }}
   s âˆˆ UNINITIALIZED
   x âˆˆ UNINITIALIZED
   y âˆˆ UNINITIALIZED
@@ -322,13 +322,13 @@
   S_0___fc_env[0..1] âˆˆ [--..--]
   S_1___fc_env[0..1] âˆˆ [--..--]
   __malloc_main3_l52 âˆˆ {{ &x }}
-  __malloc_main3_l53_0 âˆˆ {{ &y }}
+  __malloc_main3_l53 âˆˆ {{ &y }}
   ==END OF DUMP==
 [eva] tests/builtins/realloc_multiple.c:65: 
   Call to builtin Frama_C_realloc_multiple for function realloc
 [eva] tests/builtins/realloc_multiple.c:65: 
   function realloc: precondition 'freeable' got status valid.
-[eva:malloc] bases_to_realloc: {__malloc_main3_l53_0}
+[eva:malloc] bases_to_realloc: {__malloc_main3_l53}
 [eva] tests/builtins/realloc_multiple.c:65: 
   allocating variable __realloc_main3_l65
 [eva:malloc] bases_to_realloc: {__malloc_main3_l52}
@@ -338,13 +338,13 @@
 [eva] tests/builtins/realloc_multiple.c:65: 
   allocating variable __realloc_main3_l65_1
 [eva:malloc] tests/builtins/realloc_multiple.c:65: 
-  weak free on bases: {__malloc_main3_l52, __malloc_main3_l53_0}
+  weak free on bases: {__malloc_main3_l52, __malloc_main3_l53}
+[eva:alarm] tests/builtins/realloc_multiple.c:66: Warning: 
+  accessing uninitialized left-value. assert \initialized(s);
 [eva:alarm] tests/builtins/realloc_multiple.c:66: Warning: 
   out of bounds read. assert \valid_read(s);
 [kernel] tests/builtins/realloc_multiple.c:66: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva:alarm] tests/builtins/realloc_multiple.c:66: Warning: 
-  accessing uninitialized left-value. assert \initialized(s);
 [eva] tests/builtins/realloc_multiple.c:67: 
   Frama_C_dump_each:
   # Cvalue domain:
@@ -362,9 +362,8 @@
   __fc_wctomb_state âˆˆ [--..--]
   Frama_C_entropy_source âˆˆ [--..--]
   p âˆˆ {{ &__malloc_main3_l52 }} or ESCAPINGADDR
-  q âˆˆ {{ &__malloc_main3_l53_0 }} or ESCAPINGADDR
-  r âˆˆ
-   {{ NULL ; &__malloc_main3_l52 ; &__malloc_main3_l53_0 }} or ESCAPINGADDR
+  q âˆˆ {{ &__malloc_main3_l53 }} or ESCAPINGADDR
+  r âˆˆ {{ NULL ; &__malloc_main3_l52 ; &__malloc_main3_l53 }} or ESCAPINGADDR
   s âˆˆ {{ &__realloc_main3_l65[0] ; &__realloc_main3_l65_0[0] }}
   x âˆˆ {17} or UNINITIALIZED
   y âˆˆ {17} or UNINITIALIZED
@@ -373,7 +372,7 @@
   S_0___fc_env[0..1] âˆˆ [--..--]
   S_1___fc_env[0..1] âˆˆ [--..--]
   __malloc_main3_l52 âˆˆ {{ &x }}
-  __malloc_main3_l53_0 âˆˆ {{ &y }}
+  __malloc_main3_l53 âˆˆ {{ &y }}
   __realloc_main3_l65[0] âˆˆ {{ &y }}
                      [1] âˆˆ UNINITIALIZED
   __realloc_main3_l65_0[0] âˆˆ {{ &x }}
@@ -383,7 +382,7 @@
 [eva:locals-escaping] tests/builtins/realloc_multiple.c:67: Warning: 
   locals {x} escaping the scope of a block of main3 through __malloc_main3_l52
 [eva:locals-escaping] tests/builtins/realloc_multiple.c:67: Warning: 
-  locals {y} escaping the scope of a block of main3 through __malloc_main3_l53_0
+  locals {y} escaping the scope of a block of main3 through __malloc_main3_l53
 [eva:locals-escaping] tests/builtins/realloc_multiple.c:67: Warning: 
   locals {y} escaping the scope of a block of main3 through __realloc_main3_l65
 [eva:locals-escaping] tests/builtins/realloc_multiple.c:67: Warning: 
@@ -405,15 +404,14 @@
   __fc_wctomb_state âˆˆ [--..--]
   Frama_C_entropy_source âˆˆ [--..--]
   p âˆˆ {{ &__malloc_main3_l52 }} or ESCAPINGADDR
-  q âˆˆ {{ &__malloc_main3_l53_0 }} or ESCAPINGADDR
-  r âˆˆ
-   {{ NULL ; &__malloc_main3_l52 ; &__malloc_main3_l53_0 }} or ESCAPINGADDR
+  q âˆˆ {{ &__malloc_main3_l53 }} or ESCAPINGADDR
+  r âˆˆ {{ NULL ; &__malloc_main3_l52 ; &__malloc_main3_l53 }} or ESCAPINGADDR
   s âˆˆ {{ &__realloc_main3_l65[0] ; &__realloc_main3_l65_0[0] }}
   v âˆˆ {3}
   S_0___fc_env[0..1] âˆˆ [--..--]
   S_1___fc_env[0..1] âˆˆ [--..--]
   __malloc_main3_l52 âˆˆ ESCAPINGADDR
-  __malloc_main3_l53_0 âˆˆ ESCAPINGADDR
+  __malloc_main3_l53 âˆˆ ESCAPINGADDR
   __realloc_main3_l65[0] âˆˆ ESCAPINGADDR
                      [1] âˆˆ UNINITIALIZED
   __realloc_main3_l65_0[0] âˆˆ ESCAPINGADDR
@@ -427,7 +425,7 @@
 [eva] tests/builtins/realloc_multiple.c:70: 
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/realloc_multiple.c:70: 
-  strong free on bases: {__malloc_main3_l53_0}
+  strong free on bases: {__malloc_main3_l53}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] Recording results for main
@@ -516,7 +514,7 @@
   __fc_heap_status FROM __fc_heap_status (and SELF)
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   __malloc_main3_l52 FROM __fc_heap_status
-  __malloc_main3_l53_0 FROM __fc_heap_status
+  __malloc_main3_l53 FROM __fc_heap_status
 [from] Function main:
   __fc_heap_status FROM __fc_heap_status; v (and SELF)
   Frama_C_entropy_source FROM Frama_C_entropy_source; v (and SELF)
@@ -525,7 +523,7 @@
   __malloc_main2_l30[0..4] FROM __fc_heap_status; v (and SELF)
   __malloc_main2_l33[0..5] FROM __fc_heap_status; v (and SELF)
   __malloc_main3_l52 FROM __fc_heap_status; v (and SELF)
-  __malloc_main3_l53_0 FROM __fc_heap_status; v (and SELF)
+  __malloc_main3_l53 FROM __fc_heap_status; v (and SELF)
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main1:
     __fc_heap_status; Frama_C_entropy_source; q; i; r; i_0; p; x; s;
@@ -539,14 +537,14 @@
     __fc_heap_status; Frama_C_entropy_source
 [inout] Out (internal) for function main3:
     __fc_heap_status; Frama_C_entropy_source; p; q; r; s; x; y; c;
-    __malloc_main3_l52; __malloc_main3_l53_0
+    __malloc_main3_l52; __malloc_main3_l53
 [inout] Inputs for function main3:
     __fc_heap_status; Frama_C_entropy_source; __realloc_main3_l65[0];
     __realloc_main3_l65_0[0]; __realloc_main3_l65_1[0]
 [inout] Out (internal) for function main:
     __fc_heap_status; Frama_C_entropy_source; __malloc_main1_l9[0..4];
     __malloc_main1_l12[0..5]; __malloc_main2_l30[0..4];
-    __malloc_main2_l33[0..5]; __malloc_main3_l52; __malloc_main3_l53_0
+    __malloc_main2_l33[0..5]; __malloc_main3_l52; __malloc_main3_l53
 [inout] Inputs for function main:
     __fc_heap_status; Frama_C_entropy_source; __realloc_main3_l65[0];
     __realloc_main3_l65_0[0]; __realloc_main3_l65_1[0]
diff --git a/tests/float/oracle/some.0.res.oracle b/tests/float/oracle/some.0.res.oracle
index 31cdda446cb47f563405ef20b689a040f7594357..919ce1d7a0f9da2fd337a9de6c61e08f2693397d 100644
--- a/tests/float/oracle/some.0.res.oracle
+++ b/tests/float/oracle/some.0.res.oracle
@@ -6,11 +6,16 @@
   t[0] âˆˆ {1.0000000000000000}
    [1..54] âˆˆ {0}
   y âˆˆ {1.0000000000000000*2^-1}
-[eva] Semantic level unrolling superposing up to 10 states
-[eva] Semantic level unrolling superposing up to 20 states
-[eva] Semantic level unrolling superposing up to 30 states
-[eva] Semantic level unrolling superposing up to 40 states
-[eva] Semantic level unrolling superposing up to 50 states
+[eva] tests/float/some.c:11: 
+  Semantic level unrolling superposing up to 10 states
+[eva] tests/float/some.c:11: 
+  Semantic level unrolling superposing up to 20 states
+[eva] tests/float/some.c:11: 
+  Semantic level unrolling superposing up to 30 states
+[eva] tests/float/some.c:11: 
+  Semantic level unrolling superposing up to 40 states
+[eva] tests/float/some.c:11: 
+  Semantic level unrolling superposing up to 50 states
 [eva] tests/float/some.c:16: 
   Frama_C_dump_each:
   # Cvalue domain:
diff --git a/tests/libc/oracle/string_c_strchr.res.oracle b/tests/libc/oracle/string_c_strchr.res.oracle
index b6841160a62d6391d82c933f7b782fecfda6250e..cd933cfd49fed6dc7715135b255f735021193df9 100644
--- a/tests/libc/oracle/string_c_strchr.res.oracle
+++ b/tests/libc/oracle/string_c_strchr.res.oracle
@@ -4,8 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
+[eva] tests/libc/string_c_strchr.c:57: 
+  Semantic level unrolling superposing up to 100 states
+[eva] tests/libc/string_c_strchr.c:59: 
+  Semantic level unrolling superposing up to 200 states
 [eva] computing for function strchr <- main.
   Called from tests/libc/string_c_strchr.c:62.
 [eva] tests/libc/string_c_strchr.c:62: 
@@ -44,6 +46,8 @@
   Called from tests/libc/string_c_strchr.c:67.
 [eva] tests/libc/string_c_strchr.c:67: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.c:229: 
+  Semantic level unrolling superposing up to 100 states
 [eva] Recording results for strchr
 [eva] Done for function strchr
 [eva] computing for function strchr <- main.
@@ -168,6 +172,8 @@
   Called from tests/libc/string_c_strchr.c:87.
 [eva] tests/libc/string_c_strchr.c:87: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.c:229: 
+  Semantic level unrolling superposing up to 200 states
 [eva] Recording results for strchr
 [eva] Done for function strchr
 [eva] computing for function strchr <- main.
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 913d0fe0a7cdfcf9445e1512f68a3a9491fc5e65..731e3e522c0941ee99099b17fb0e2ccfe22a7e53 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -59,7 +59,8 @@
 [eva] Done for function test_strstr
 [eva] computing for function test_strncat <- main.
   Called from tests/libc/string_h.c:115.
-[eva] Semantic level unrolling superposing up to 100 states
+[eva] tests/libc/string_h.c:34: 
+  Semantic level unrolling superposing up to 100 states
 [eva] computing for function strncat <- test_strncat <- main.
   Called from tests/libc/string_h.c:36.
 [eva] using specification for function strncat
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 78a30b4a80af8682c477b5bdbdb42c3aababec9f..601aea128cd1b0dfe1a2be81ffebe18c3f91a743 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -222,12 +222,6 @@
 [eva] computing for function getresgid <- main.
   Called from tests/libc/unistd_h.c:57.
 [eva] Done for function getresgid
-[eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
-[eva] Done for function getresgid
-[eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
-[eva] Done for function getresgid
 [eva] computing for function setresgid <- main.
   Called from tests/libc/unistd_h.c:59.
 [eva] using specification for function setresgid
@@ -235,12 +229,6 @@
 [eva] computing for function setresgid <- main.
   Called from tests/libc/unistd_h.c:59.
 [eva] Done for function setresgid
-[eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
-[eva] Done for function setresgid
-[eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
-[eva] Done for function setresgid
 [eva] tests/libc/unistd_h.c:60: assertion got status valid.
 [eva] computing for function getpid <- main.
   Called from tests/libc/unistd_h.c:62.
@@ -255,18 +243,6 @@
 [eva] computing for function getpid <- main.
   Called from tests/libc/unistd_h.c:62.
 [eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
 [eva] computing for function getppid <- main.
   Called from tests/libc/unistd_h.c:63.
 [eva] using specification for function getppid
@@ -280,18 +256,6 @@
 [eva] computing for function getppid <- main.
   Called from tests/libc/unistd_h.c:63.
 [eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
 [eva] computing for function getsid <- main.
   Called from tests/libc/unistd_h.c:64.
 [eva] using specification for function getsid
@@ -305,18 +269,6 @@
 [eva] computing for function getsid <- main.
   Called from tests/libc/unistd_h.c:64.
 [eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
 [eva] computing for function getuid <- main.
   Called from tests/libc/unistd_h.c:65.
 [eva] using specification for function getuid
@@ -330,18 +282,6 @@
 [eva] computing for function getuid <- main.
   Called from tests/libc/unistd_h.c:65.
 [eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
 [eva] computing for function getgid <- main.
   Called from tests/libc/unistd_h.c:66.
 [eva] using specification for function getgid
@@ -355,18 +295,6 @@
 [eva] computing for function getgid <- main.
   Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
 [eva] computing for function geteuid <- main.
   Called from tests/libc/unistd_h.c:67.
 [eva] using specification for function geteuid
@@ -380,18 +308,6 @@
 [eva] computing for function geteuid <- main.
   Called from tests/libc/unistd_h.c:67.
 [eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
 [eva] computing for function getegid <- main.
   Called from tests/libc/unistd_h.c:68.
 [eva] using specification for function getegid
@@ -405,18 +321,6 @@
 [eva] computing for function getegid <- main.
   Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
 [eva] computing for function setegid <- main.
   Called from tests/libc/unistd_h.c:69.
 [eva] using specification for function setegid
@@ -430,22 +334,19 @@
 [eva] computing for function setegid <- main.
   Called from tests/libc/unistd_h.c:69.
 [eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
 [eva] computing for function seteuid <- main.
   Called from tests/libc/unistd_h.c:70.
 [eva] using specification for function seteuid
 [eva] Done for function seteuid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] Done for function seteuid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] Done for function seteuid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] Done for function seteuid
 [eva] computing for function setgid <- main.
   Called from tests/libc/unistd_h.c:71.
 [eva] using specification for function setgid
@@ -453,6 +354,12 @@
 [eva] computing for function setgid <- main.
   Called from tests/libc/unistd_h.c:71.
 [eva] Done for function setgid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] Done for function setgid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] Done for function setgid
 [eva] computing for function setuid <- main.
   Called from tests/libc/unistd_h.c:72.
 [eva] using specification for function setuid
@@ -460,6 +367,12 @@
 [eva] computing for function setuid <- main.
   Called from tests/libc/unistd_h.c:72.
 [eva] Done for function setuid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] Done for function setuid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] Done for function setuid
 [eva] computing for function setregid <- main.
   Called from tests/libc/unistd_h.c:73.
 [eva] using specification for function setregid
@@ -467,6 +380,12 @@
 [eva] computing for function setregid <- main.
   Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setregid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] Done for function setregid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] Done for function setregid
 [eva] computing for function setreuid <- main.
   Called from tests/libc/unistd_h.c:74.
 [eva] using specification for function setreuid
@@ -474,6 +393,12 @@
 [eva] computing for function setreuid <- main.
   Called from tests/libc/unistd_h.c:74.
 [eva] Done for function setreuid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] Done for function setreuid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] Done for function setreuid
 [eva] computing for function getpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] using specification for function getpgid
@@ -481,6 +406,12 @@
 [eva] computing for function getpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] Done for function getpgid
+[eva] computing for function getpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function getpgid
+[eva] computing for function getpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function getpgid
 [eva] computing for function setpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] using specification for function setpgid
@@ -488,6 +419,12 @@
 [eva] computing for function setpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setpgid
+[eva] computing for function setpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function setpgid
+[eva] computing for function setpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function setpgid
 [eva] computing for function getpgrp <- main.
   Called from tests/libc/unistd_h.c:76.
 [eva] using specification for function getpgrp
@@ -495,12 +432,21 @@
 [eva] computing for function getpgrp <- main.
   Called from tests/libc/unistd_h.c:76.
 [eva] Done for function getpgrp
+[eva] computing for function getpgrp <- main.
+  Called from tests/libc/unistd_h.c:76.
+[eva] Done for function getpgrp
+[eva] computing for function getpgrp <- main.
+  Called from tests/libc/unistd_h.c:76.
+[eva] Done for function getpgrp
 [eva] computing for function unlink <- main.
   Called from tests/libc/unistd_h.c:78.
 [eva] using specification for function unlink
 [eva] tests/libc/unistd_h.c:78: 
   function unlink: precondition 'valid_string_path' got status valid.
 [eva] Done for function unlink
+[eva] computing for function unlink <- main.
+  Called from tests/libc/unistd_h.c:78.
+[eva] Done for function unlink
 [eva] computing for function isatty <- main.
   Called from tests/libc/unistd_h.c:80.
 [eva] using specification for function isatty
@@ -508,6 +454,12 @@
 [eva] computing for function isatty <- main.
   Called from tests/libc/unistd_h.c:80.
 [eva] Done for function isatty
+[eva] computing for function isatty <- main.
+  Called from tests/libc/unistd_h.c:80.
+[eva] Done for function isatty
+[eva] computing for function isatty <- main.
+  Called from tests/libc/unistd_h.c:80.
+[eva] Done for function isatty
 [eva] tests/libc/unistd_h.c:81: assertion got status valid.
 [eva] computing for function ttyname <- main.
   Called from tests/libc/unistd_h.c:82.
@@ -516,6 +468,12 @@
 [eva] computing for function ttyname <- main.
   Called from tests/libc/unistd_h.c:82.
 [eva] Done for function ttyname
+[eva] computing for function ttyname <- main.
+  Called from tests/libc/unistd_h.c:82.
+[eva] Done for function ttyname
+[eva] computing for function ttyname <- main.
+  Called from tests/libc/unistd_h.c:82.
+[eva] Done for function ttyname
 [eva] computing for function chown <- main.
   Called from tests/libc/unistd_h.c:84.
 [eva] using specification for function chown
@@ -531,6 +489,18 @@
 [eva] computing for function chown <- main.
   Called from tests/libc/unistd_h.c:84.
 [eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 78e0c0de0e69dd98b7adb4fbd0f5bcf9f8f82c0e..c0be6ee4a9af72fb649805d000c4ac3967d6c467 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -222,12 +222,6 @@
 [eva] computing for function getresgid <- main.
   Called from tests/libc/unistd_h.c:57.
 [eva] Done for function getresgid
-[eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
-[eva] Done for function getresgid
-[eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
-[eva] Done for function getresgid
 [eva] computing for function setresgid <- main.
   Called from tests/libc/unistd_h.c:59.
 [eva] using specification for function setresgid
@@ -235,12 +229,6 @@
 [eva] computing for function setresgid <- main.
   Called from tests/libc/unistd_h.c:59.
 [eva] Done for function setresgid
-[eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
-[eva] Done for function setresgid
-[eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
-[eva] Done for function setresgid
 [eva] tests/libc/unistd_h.c:60: assertion got status valid.
 [eva] computing for function getpid <- main.
   Called from tests/libc/unistd_h.c:62.
@@ -255,18 +243,6 @@
 [eva] computing for function getpid <- main.
   Called from tests/libc/unistd_h.c:62.
 [eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
-[eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
-[eva] Done for function getpid
 [eva] computing for function getppid <- main.
   Called from tests/libc/unistd_h.c:63.
 [eva] using specification for function getppid
@@ -280,18 +256,6 @@
 [eva] computing for function getppid <- main.
   Called from tests/libc/unistd_h.c:63.
 [eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
-[eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
-[eva] Done for function getppid
 [eva] computing for function getsid <- main.
   Called from tests/libc/unistd_h.c:64.
 [eva] using specification for function getsid
@@ -305,18 +269,6 @@
 [eva] computing for function getsid <- main.
   Called from tests/libc/unistd_h.c:64.
 [eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
-[eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
-[eva] Done for function getsid
 [eva] computing for function getuid <- main.
   Called from tests/libc/unistd_h.c:65.
 [eva] using specification for function getuid
@@ -330,18 +282,6 @@
 [eva] computing for function getuid <- main.
   Called from tests/libc/unistd_h.c:65.
 [eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
-[eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
-[eva] Done for function getuid
 [eva] computing for function getgid <- main.
   Called from tests/libc/unistd_h.c:66.
 [eva] using specification for function getgid
@@ -355,18 +295,6 @@
 [eva] computing for function getgid <- main.
   Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
-[eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
-[eva] Done for function getgid
 [eva] computing for function geteuid <- main.
   Called from tests/libc/unistd_h.c:67.
 [eva] using specification for function geteuid
@@ -380,18 +308,6 @@
 [eva] computing for function geteuid <- main.
   Called from tests/libc/unistd_h.c:67.
 [eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
-[eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
-[eva] Done for function geteuid
 [eva] computing for function getegid <- main.
   Called from tests/libc/unistd_h.c:68.
 [eva] using specification for function getegid
@@ -405,18 +321,6 @@
 [eva] computing for function getegid <- main.
   Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
-[eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
-[eva] Done for function getegid
 [eva] computing for function setegid <- main.
   Called from tests/libc/unistd_h.c:69.
 [eva] using specification for function setegid
@@ -430,22 +334,19 @@
 [eva] computing for function setegid <- main.
   Called from tests/libc/unistd_h.c:69.
 [eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
-[eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
-[eva] Done for function setegid
 [eva] computing for function seteuid <- main.
   Called from tests/libc/unistd_h.c:70.
 [eva] using specification for function seteuid
 [eva] Done for function seteuid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] Done for function seteuid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] Done for function seteuid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] Done for function seteuid
 [eva] computing for function setgid <- main.
   Called from tests/libc/unistd_h.c:71.
 [eva] using specification for function setgid
@@ -453,6 +354,12 @@
 [eva] computing for function setgid <- main.
   Called from tests/libc/unistd_h.c:71.
 [eva] Done for function setgid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] Done for function setgid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] Done for function setgid
 [eva] computing for function setuid <- main.
   Called from tests/libc/unistd_h.c:72.
 [eva] using specification for function setuid
@@ -460,6 +367,12 @@
 [eva] computing for function setuid <- main.
   Called from tests/libc/unistd_h.c:72.
 [eva] Done for function setuid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] Done for function setuid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] Done for function setuid
 [eva] computing for function setregid <- main.
   Called from tests/libc/unistd_h.c:73.
 [eva] using specification for function setregid
@@ -467,6 +380,12 @@
 [eva] computing for function setregid <- main.
   Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setregid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] Done for function setregid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] Done for function setregid
 [eva] computing for function setreuid <- main.
   Called from tests/libc/unistd_h.c:74.
 [eva] using specification for function setreuid
@@ -474,6 +393,12 @@
 [eva] computing for function setreuid <- main.
   Called from tests/libc/unistd_h.c:74.
 [eva] Done for function setreuid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] Done for function setreuid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] Done for function setreuid
 [eva] computing for function getpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] using specification for function getpgid
@@ -481,6 +406,12 @@
 [eva] computing for function getpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] Done for function getpgid
+[eva] computing for function getpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function getpgid
+[eva] computing for function getpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function getpgid
 [eva] computing for function setpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] using specification for function setpgid
@@ -488,6 +419,12 @@
 [eva] computing for function setpgid <- main.
   Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setpgid
+[eva] computing for function setpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function setpgid
+[eva] computing for function setpgid <- main.
+  Called from tests/libc/unistd_h.c:75.
+[eva] Done for function setpgid
 [eva] computing for function getpgrp <- main.
   Called from tests/libc/unistd_h.c:76.
 [eva] using specification for function getpgrp
@@ -495,12 +432,21 @@
 [eva] computing for function getpgrp <- main.
   Called from tests/libc/unistd_h.c:76.
 [eva] Done for function getpgrp
+[eva] computing for function getpgrp <- main.
+  Called from tests/libc/unistd_h.c:76.
+[eva] Done for function getpgrp
+[eva] computing for function getpgrp <- main.
+  Called from tests/libc/unistd_h.c:76.
+[eva] Done for function getpgrp
 [eva] computing for function unlink <- main.
   Called from tests/libc/unistd_h.c:78.
 [eva] using specification for function unlink
 [eva] tests/libc/unistd_h.c:78: 
   function unlink: precondition 'valid_string_path' got status valid.
 [eva] Done for function unlink
+[eva] computing for function unlink <- main.
+  Called from tests/libc/unistd_h.c:78.
+[eva] Done for function unlink
 [eva] computing for function isatty <- main.
   Called from tests/libc/unistd_h.c:80.
 [eva] using specification for function isatty
@@ -508,6 +454,12 @@
 [eva] computing for function isatty <- main.
   Called from tests/libc/unistd_h.c:80.
 [eva] Done for function isatty
+[eva] computing for function isatty <- main.
+  Called from tests/libc/unistd_h.c:80.
+[eva] Done for function isatty
+[eva] computing for function isatty <- main.
+  Called from tests/libc/unistd_h.c:80.
+[eva] Done for function isatty
 [eva] tests/libc/unistd_h.c:81: assertion got status valid.
 [eva] computing for function ttyname <- main.
   Called from tests/libc/unistd_h.c:82.
@@ -516,6 +468,12 @@
 [eva] computing for function ttyname <- main.
   Called from tests/libc/unistd_h.c:82.
 [eva] Done for function ttyname
+[eva] computing for function ttyname <- main.
+  Called from tests/libc/unistd_h.c:82.
+[eva] Done for function ttyname
+[eva] computing for function ttyname <- main.
+  Called from tests/libc/unistd_h.c:82.
+[eva] Done for function ttyname
 [eva] computing for function chown <- main.
   Called from tests/libc/unistd_h.c:84.
 [eva] using specification for function chown
@@ -531,6 +489,18 @@
 [eva] computing for function chown <- main.
   Called from tests/libc/unistd_h.c:84.
 [eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+  Called from tests/libc/unistd_h.c:84.
+[eva] Done for function chown
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/slicing/oracle/if_many_values.res.oracle b/tests/slicing/oracle/if_many_values.res.oracle
index 37a2e138f4ebdbf55e64b6a3842906d44b8b2719..b9a574da2ca5015672235bcfc41d788a86eb8d2c 100644
--- a/tests/slicing/oracle/if_many_values.res.oracle
+++ b/tests/slicing/oracle/if_many_values.res.oracle
@@ -5,7 +5,8 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   r âˆˆ {1}
-[eva] Semantic level unrolling superposing up to 100 states
+[eva] tests/slicing/if_many_values.i:8: 
+  Semantic level unrolling superposing up to 100 states
 [eva] tests/slicing/if_many_values.i:8: starting to merge loop iterations
 [eva:alarm] tests/slicing/if_many_values.i:11: Warning: 
   signed overflow. assert r + 1 â‰¤ 2147483647;
diff --git a/tests/value/oracle/bitwise.res.oracle b/tests/value/oracle/bitwise.res.oracle
index 29d9bbe232251a10bb728dfe3c9ea3e635cb8fc0..253b81df5d160895ccce32da57051bbe7701e2f3 100644
--- a/tests/value/oracle/bitwise.res.oracle
+++ b/tests/value/oracle/bitwise.res.oracle
@@ -34,12 +34,12 @@
 [eva] computing for function test4 <- main.
   Called from tests/value/bitwise.i:141.
 [eva] tests/value/bitwise.i:62: assertion got status valid.
-[eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
 [eva] tests/value/bitwise.i:64: 
   Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
-[eva] tests/value/bitwise.i:66: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
+[eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
 [eva] tests/value/bitwise.i:66: 
   Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
+[eva] tests/value/bitwise.i:66: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
 [eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
 [eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
 [eva] Recording results for test4
diff --git a/tests/value/oracle/builtins_split.res.oracle b/tests/value/oracle/builtins_split.res.oracle
index f31146d1deab841c23fd3da0debf8b95953e9639..150538b4442b7a0b08488017b206f8b9cf900e29 100644
--- a/tests/value/oracle/builtins_split.res.oracle
+++ b/tests/value/oracle/builtins_split.res.oracle
@@ -29,8 +29,8 @@
 [eva] tests/value/builtins_split.c:23: Frama_C_show_each_split: {{ &x ; &y }}
 [eva] tests/value/builtins_split.c:25: 
   Call to builtin Frama_C_builtin_split_pointer
-[eva] tests/value/builtins_split.c:26: Frama_C_show_each_split_pointer: {{ &x }}
 [eva] tests/value/builtins_split.c:26: Frama_C_show_each_split_pointer: {{ &y }}
+[eva] tests/value/builtins_split.c:26: Frama_C_show_each_split_pointer: {{ &x }}
 [eva] Recording results for test1
 [eva] Done for function test1
 [eva] computing for function test2 <- main.
@@ -62,40 +62,12 @@
 [eva:alarm] tests/value/builtins_split.c:96: Warning: 
   out of bounds read. assert \valid_read(&(ps->p)->p);
 [eva] tests/value/builtins_split.c:96: Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:96: Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:96: Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:96: Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:96: Call to builtin Frama_C_builtin_split_all
 [eva] tests/value/builtins_split.c:99: 
   Frama_C_show_each_s_3: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s1 }}, {1}
 [eva:alarm] tests/value/builtins_split.c:104: Warning: 
   out of bounds read. assert \valid_read(&(ps->p)->p);
 [eva] tests/value/builtins_split.c:104: 
   Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:104: 
-  Call to builtin Frama_C_builtin_split_all
 [eva:alarm] tests/value/builtins_split.c:106: Warning: 
   assertion got status invalid (stopping propagation).
 [eva] tests/value/builtins_split.c:106: assertion got status valid.
@@ -107,51 +79,22 @@
   Call to builtin Frama_C_builtin_split_all
 [eva] tests/value/builtins_split.c:112: 
   Location ((ps->p)->p)->v points to too many values ([--..--]). Cannot split.
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
-[eva] tests/value/builtins_split.c:112: 
-  Call to builtin Frama_C_builtin_split_all
 [eva] tests/value/builtins_split.c:114: 
-  Frama_C_show_each_s_5:
-  {{ &s6 + {4} }}, {{ &s4 + {4} }}, {{ &s2 }}, [-2147483648..2147483647]
-[eva] tests/value/builtins_split.c:114: 
-  Frama_C_show_each_s_5: {{ &s6 + {4} }}, {{ &s4 + {4} }}, {{ &s0 }}, {0}
-[eva] tests/value/builtins_split.c:114: 
-  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s1 }}, {-1}
-[eva] tests/value/builtins_split.c:114: 
-  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s0 }}, {0}
+  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s4 + {4} }}, {{ &s0 }}, {0}
 [eva] tests/value/builtins_split.c:114: 
   Frama_C_show_each_s_5:
   {{ &s5 + {4} }}, {{ &s4 + {4} }}, {{ &s2 }}, [-2147483648..2147483647]
 [eva] tests/value/builtins_split.c:114: 
-  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s4 + {4} }}, {{ &s0 }}, {0}
+  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s0 }}, {0}
 [eva] tests/value/builtins_split.c:114: 
-  Frama_C_show_each_s_5:
-  {{ &s6 + {4} }}, {{ &s4 + {4} }}, {{ &s2 }}, [-2147483648..2147483647]
+  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s1 }}, {1}
+[eva] tests/value/builtins_split.c:114: 
+  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s1 }}, {-1}
 [eva] tests/value/builtins_split.c:114: 
   Frama_C_show_each_s_5: {{ &s6 + {4} }}, {{ &s4 + {4} }}, {{ &s0 }}, {0}
 [eva] tests/value/builtins_split.c:114: 
-  Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s1 }}, {1}
+  Frama_C_show_each_s_5:
+  {{ &s6 + {4} }}, {{ &s4 + {4} }}, {{ &s2 }}, [-2147483648..2147483647]
 [eva] Recording results for test3
 [eva] Done for function test3
 [eva] computing for function test4 <- main.
@@ -166,35 +109,35 @@
   Location x_0 points to too many values ([-3..25]). Cannot split.
 [eva] tests/value/builtins_split.c:125: Frama_C_show_each_test4_1: [-3..25]
 [eva] tests/value/builtins_split.c:127: Call to builtin Frama_C_builtin_split
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {-3}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {-2}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {-1}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {0}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {1}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {2}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {3}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {4}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {5}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {6}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {7}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {8}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {9}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {10}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {11}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {12}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {13}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {14}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {15}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {16}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {17}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {18}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {19}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {20}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {21}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {22}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {23}
-[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {24}
 [eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {25}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {24}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {23}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {22}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {21}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {20}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {19}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {18}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {17}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {16}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {15}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {14}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {13}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {12}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {11}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {10}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {9}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {8}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {7}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {6}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {5}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {4}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {3}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {2}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {1}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {0}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {-1}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {-2}
+[eva] tests/value/builtins_split.c:128: Frama_C_show_each_test4_2: {-3}
 [eva] Recording results for test4
 [eva] Done for function test4
 [eva] computing for function test5 <- main.
@@ -212,22 +155,22 @@
 [eva] tests/value/builtins_split.c:145: Call to builtin Frama_C_builtin_split
 [eva] tests/value/builtins_split.c:146: 
   Frama_C_domain_show_each_test6:
-  z : # Cvalue domain: {0} or UNINITIALIZED
+  z : # Cvalue domain: {5} or UNINITIALIZED
 [eva] tests/value/builtins_split.c:146: 
   Frama_C_domain_show_each_test6:
-  z : # Cvalue domain: {1} or UNINITIALIZED
+  z : # Cvalue domain: {4} or UNINITIALIZED
 [eva] tests/value/builtins_split.c:146: 
   Frama_C_domain_show_each_test6:
-  z : # Cvalue domain: {2} or UNINITIALIZED
+  z : # Cvalue domain: {3} or UNINITIALIZED
 [eva] tests/value/builtins_split.c:146: 
   Frama_C_domain_show_each_test6:
-  z : # Cvalue domain: {3} or UNINITIALIZED
+  z : # Cvalue domain: {2} or UNINITIALIZED
 [eva] tests/value/builtins_split.c:146: 
   Frama_C_domain_show_each_test6:
-  z : # Cvalue domain: {4} or UNINITIALIZED
+  z : # Cvalue domain: {1} or UNINITIALIZED
 [eva] tests/value/builtins_split.c:146: 
   Frama_C_domain_show_each_test6:
-  z : # Cvalue domain: {5} or UNINITIALIZED
+  z : # Cvalue domain: {0} or UNINITIALIZED
 [eva] Recording results for test6
 [eva] Done for function test6
 [eva] Recording results for main
diff --git a/tests/value/oracle/hierarchical_convergence.res.oracle b/tests/value/oracle/hierarchical_convergence.res.oracle
index 01bce6d8a63ca4926d5ed90e7cd64d67f33e8f4f..6109b4ff087453a6e957da93c1280b8242d274a5 100644
--- a/tests/value/oracle/hierarchical_convergence.res.oracle
+++ b/tests/value/oracle/hierarchical_convergence.res.oracle
@@ -10,21 +10,18 @@
 [eva] tests/value/hierarchical_convergence.c:7: 
   starting to merge loop iterations
 [eva] tests/value/hierarchical_convergence.c:8: Frama_C_show_each: {0; 1}
-[eva] tests/value/hierarchical_convergence.c:10: Frama_C_show_each: {1}, {0}
 [eva] tests/value/hierarchical_convergence.c:9: 
   starting to merge loop iterations
+[eva] tests/value/hierarchical_convergence.c:10: Frama_C_show_each: {1}, {0}
 [eva] tests/value/hierarchical_convergence.c:8: Frama_C_show_each: {0; 1; 2}
-[eva] tests/value/hierarchical_convergence.c:10: Frama_C_show_each: {1; 2}, {0}
-[eva] tests/value/hierarchical_convergence.c:10: 
-  Frama_C_show_each: {1; 2}, {0; 1}
-[eva] tests/value/hierarchical_convergence.c:8: Frama_C_show_each: [0..99]
-[eva] tests/value/hierarchical_convergence.c:10: Frama_C_show_each: [1..99], {0}
 [eva] tests/value/hierarchical_convergence.c:10: 
-  Frama_C_show_each: [1..99], {0; 1}
+  Frama_C_show_each: [1..2147483647], {0; 1}
 [eva] tests/value/hierarchical_convergence.c:10: 
-  Frama_C_show_each: [1..99], {0; 1; 2}
+  Frama_C_show_each: [1..2147483647], {0; 1; 2}
 [eva] tests/value/hierarchical_convergence.c:10: 
-  Frama_C_show_each: [1..99], [0..98]
+  Frama_C_show_each: [1..2147483647], [0..2147483646]
+[eva:alarm] tests/value/hierarchical_convergence.c:7: Warning: 
+  signed overflow. assert i + 1 â‰¤ 2147483647;
 [eva] tests/value/hierarchical_convergence.c:8: Frama_C_show_each: [0..99]
 [eva:alarm] tests/value/hierarchical_convergence.c:15: Warning: 
   accessing uninitialized left-value. assert \initialized(&j);
@@ -48,7 +45,7 @@
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
 [from] Function f:
-  \result FROM \nothing
+  \result FROM n
 [from] Function main:
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index 527b4570d7e3d7e0787e7f2fc372aba0f0bdd453..79cf5c4a3129d812402778bbe4f0ab7ba79dc9d2 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -158,6 +158,8 @@
 [eva] computing for function f <- g3 <- main.
   Called from tests/value/initialized.c:98.
 [eva] tests/value/initialized.c:11: starting to merge loop iterations
+[eva:alarm] tests/value/initialized.c:8: Warning: 
+  function f: postcondition got status invalid.
 [eva:alarm] tests/value/initialized.c:8: Warning: 
   function f: postcondition got status unknown.
 [eva] Recording results for f
diff --git a/tests/value/oracle/local_slevel.res.oracle b/tests/value/oracle/local_slevel.res.oracle
index feccc39bc87d3f9fc9707cb799f89c67b66d3f10..ecb1201e61c7d2bad6588c6b28a35d3c0bb612e2 100644
--- a/tests/value/oracle/local_slevel.res.oracle
+++ b/tests/value/oracle/local_slevel.res.oracle
@@ -88,7 +88,8 @@
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {47}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {48}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {49}
-[eva] Semantic level unrolling superposing up to 100 states
+[eva] tests/value/local_slevel.i:43: 
+  Semantic level unrolling superposing up to 100 states
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {50}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {51}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {52}
@@ -139,7 +140,8 @@
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {97}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {98}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {99}
-[eva] Semantic level unrolling superposing up to 200 states
+[eva] tests/value/local_slevel.i:43: 
+  Semantic level unrolling superposing up to 200 states
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] Recording results for main
@@ -466,7 +468,8 @@ void main(void)
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {47}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {48}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {49}
-[eva] Semantic level unrolling superposing up to 100 states
+[eva] tests/value/local_slevel.i:43: 
+  Semantic level unrolling superposing up to 100 states
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {50}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {51}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {52}
@@ -517,7 +520,8 @@ void main(void)
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {97}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {98}
 [eva] tests/value/local_slevel.i:37: Frama_C_show_each: {99}
-[eva] Semantic level unrolling superposing up to 200 states
+[eva] tests/value/local_slevel.i:43: 
+  Semantic level unrolling superposing up to 200 states
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] Recording results for main
diff --git a/tests/value/oracle/narrow_behaviors.res.oracle b/tests/value/oracle/narrow_behaviors.res.oracle
index 6c5857f3dc1d14a0f7ee97d24a92089951fc2449..387fa60829ad2a32626a6e81b02a13dadd738e11 100644
--- a/tests/value/oracle/narrow_behaviors.res.oracle
+++ b/tests/value/oracle/narrow_behaviors.res.oracle
@@ -11,36 +11,37 @@
 [eva] tests/value/narrow_behaviors.i:56: 
   Frama_C_dump_each:
   # Cvalue domain:
-  nondet âˆˆ {0}
-  p{.x; .y} âˆˆ {1}
+  nondet âˆˆ [--..--]
+  p.x âˆˆ {2}
+   .y âˆˆ {1; 2}
   __retres âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva] tests/value/narrow_behaviors.i:56: 
   Frama_C_dump_each:
   # Cvalue domain:
-  nondet âˆˆ [--..--]
-  p.x âˆˆ {2}
-   .y âˆˆ {1; 2}
+  nondet âˆˆ {0}
+  p{.x; .y} âˆˆ {1}
   __retres âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva] computing for function f2 <- main.
   Called from tests/value/narrow_behaviors.i:57.
 [eva] using specification for function f2
+[eva] Done for function f2
+[eva] computing for function f2 <- main.
+  Called from tests/value/narrow_behaviors.i:57.
 [eva] tests/value/narrow_behaviors.i:57: 
   function f2, behavior b: assumes got status invalid; behavior not evaluated.
 [eva] tests/value/narrow_behaviors.i:57: 
   function f2, behavior c: assumes got status invalid; behavior not evaluated.
 [eva] Done for function f2
-[eva] computing for function f2 <- main.
-  Called from tests/value/narrow_behaviors.i:57.
-[eva] Done for function f2
 [eva] tests/value/narrow_behaviors.i:57: 
   Frama_C_dump_each:
   # Cvalue domain:
-  nondet âˆˆ {0}
-  p{.x; .y} âˆˆ {1}
-  q.x âˆˆ {1; 2}
-   .y âˆˆ {1}
+  nondet âˆˆ [--..--]
+  p.x âˆˆ {2}
+   .y âˆˆ {1; 2}
+  q.x âˆˆ {2}
+   .y âˆˆ {1; 2}
   __retres âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva] tests/value/narrow_behaviors.i:57: 
@@ -56,11 +57,10 @@
 [eva] tests/value/narrow_behaviors.i:57: 
   Frama_C_dump_each:
   # Cvalue domain:
-  nondet âˆˆ [--..--]
-  p.x âˆˆ {2}
-   .y âˆˆ {1; 2}
-  q.x âˆˆ {2}
-   .y âˆˆ {1; 2}
+  nondet âˆˆ {0}
+  p{.x; .y} âˆˆ {1}
+  q.x âˆˆ {1; 2}
+   .y âˆˆ {1}
   __retres âˆˆ UNINITIALIZED
   ==END OF DUMP==
 [eva:alarm] tests/value/narrow_behaviors.i:61: Warning: 
diff --git a/tests/value/oracle/no_results.res.oracle b/tests/value/oracle/no_results.res.oracle
index 2053346504cd37cff5d7eceae5b51ac6b0b9a9ed..b1bab125fb03891dc033443817eabe909a5dd537 100644
--- a/tests/value/oracle/no_results.res.oracle
+++ b/tests/value/oracle/no_results.res.oracle
@@ -6,36 +6,66 @@
   t[0..2999] âˆˆ {0}
 [eva] computing for function init <- main.
   Called from tests/value/no_results.c:19.
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
-[eva] Semantic level unrolling superposing up to 900 states
-[eva] Semantic level unrolling superposing up to 1000 states
-[eva] Semantic level unrolling superposing up to 1100 states
-[eva] Semantic level unrolling superposing up to 1200 states
-[eva] Semantic level unrolling superposing up to 1300 states
-[eva] Semantic level unrolling superposing up to 1400 states
-[eva] Semantic level unrolling superposing up to 1500 states
-[eva] Semantic level unrolling superposing up to 1600 states
-[eva] Semantic level unrolling superposing up to 1700 states
-[eva] Semantic level unrolling superposing up to 1800 states
-[eva] Semantic level unrolling superposing up to 1900 states
-[eva] Semantic level unrolling superposing up to 2000 states
-[eva] Semantic level unrolling superposing up to 2100 states
-[eva] Semantic level unrolling superposing up to 2200 states
-[eva] Semantic level unrolling superposing up to 2300 states
-[eva] Semantic level unrolling superposing up to 2400 states
-[eva] Semantic level unrolling superposing up to 2500 states
-[eva] Semantic level unrolling superposing up to 2600 states
-[eva] Semantic level unrolling superposing up to 2700 states
-[eva] Semantic level unrolling superposing up to 2800 states
-[eva] Semantic level unrolling superposing up to 2900 states
-[eva] Semantic level unrolling superposing up to 3000 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 100 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 200 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 300 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 400 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 500 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 600 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 700 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 800 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 900 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1000 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1100 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1200 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1300 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1400 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1500 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1600 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1700 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1800 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 1900 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2000 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2100 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2200 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2300 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2400 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2500 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2600 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2700 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2800 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 2900 states
+[eva] tests/value/no_results.c:10: 
+  Semantic level unrolling superposing up to 3000 states
 [eva] Recording results for init
 [eva] Done for function init
 [eva] computing for function f <- main.
diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle
index 7b572572277b17bd749877e8b8dc07457a5e70af..85ae6a30dc6ab58ddc54b0844b4a291cc3bc0d48 100644
--- a/tests/value/oracle/partitioning-annots.1.res.oracle
+++ b/tests/value/oracle/partitioning-annots.1.res.oracle
@@ -17,28 +17,28 @@
 [eva] Done for function Frama_C_interval
 [eva] tests/value/partitioning-annots.c:76: 
   Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:79: 
-  Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
 [eva] tests/value/partitioning-annots.c:79: 
   Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
+[eva] tests/value/partitioning-annots.c:79: 
+  Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+  Frama_C_show_each_before_first_merge: {1}, {2}, {1}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {0}, {2}, {0}
+  Frama_C_show_each_before_first_merge: {1}, {1}, {1}
 [eva] tests/value/partitioning-annots.c:81: 
   Frama_C_show_each_before_first_merge: {1}, {0}, {1}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {1}, {1}, {1}
+  Frama_C_show_each_before_first_merge: {0}, {2}, {0}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {1}, {2}, {1}
+  Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:81: 
+  Frama_C_show_each_before_first_merge: {0}, {0}, {0}
 [eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
+  Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
 [eva] tests/value/partitioning-annots.c:83: 
   Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
 [eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
+  Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
 [eva] tests/value/partitioning-annots.c:85: 
   Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
 [eva] Recording results for test_split
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index d4afe5dd536c8700daca39853efb7505fc651a08..343ee7f5639b073186a03ada6005301f6301d08d 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -17,38 +17,38 @@
 [eva] Done for function Frama_C_interval
 [eva] tests/value/partitioning-annots.c:76: 
   Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:79: 
-  Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
 [eva] tests/value/partitioning-annots.c:79: 
   Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
+[eva] tests/value/partitioning-annots.c:79: 
+  Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+  Frama_C_show_each_before_first_merge: {1}, {2}, {1}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {0}, {2}, {0}
+  Frama_C_show_each_before_first_merge: {1}, {1}, {1}
 [eva] tests/value/partitioning-annots.c:81: 
   Frama_C_show_each_before_first_merge: {1}, {0}, {1}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {1}, {1}, {1}
+  Frama_C_show_each_before_first_merge: {0}, {2}, {0}
 [eva] tests/value/partitioning-annots.c:81: 
-  Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_merge: {0}, {0}, {0}
+  Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:81: 
+  Frama_C_show_each_before_first_merge: {0}, {0}, {0}
 [eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_merge: {1}, {0}, {1}
+  Frama_C_show_each_before_second_merge: {1}, {2}, {1}
 [eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_merge: {0}, {1}, {0}
+  Frama_C_show_each_before_second_merge: {0}, {2}, {0}
 [eva] tests/value/partitioning-annots.c:83: 
   Frama_C_show_each_before_second_merge: {1}, {1}, {1}
 [eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_merge: {0}, {2}, {0}
+  Frama_C_show_each_before_second_merge: {0}, {1}, {0}
 [eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:85: 
-  Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
+  Frama_C_show_each_before_second_merge: {1}, {0}, {1}
+[eva] tests/value/partitioning-annots.c:83: 
+  Frama_C_show_each_before_second_merge: {0}, {0}, {0}
 [eva] tests/value/partitioning-annots.c:85: 
   Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
+[eva] tests/value/partitioning-annots.c:85: 
+  Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
 [eva] Recording results for test_split
 [eva] done for function test_split
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index f8931c634422b917da239fda0e225bc98b34af54..f0e69a170fe060780d968638b9a0603a27a3185d 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -28,16 +28,16 @@
 [eva] Done for function Frama_C_interval
 [eva:alarm] tests/value/partitioning-annots.c:110: Warning: 
   accessing uninitialized left-value. assert \initialized(&A[i]);
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {0}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {1}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {2}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {3}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {4}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {5}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {6}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {7}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {8}, {42}
 [eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {9}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {8}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {7}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {6}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {5}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {4}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {3}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {2}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {1}, {42}
+[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {0}, {42}
 [eva] tests/value/partitioning-annots.c:116: assertion got status valid.
 [eva] tests/value/partitioning-annots.c:119: 
   Frama_C_show_each: {{ "Value 42 not found" }}
diff --git a/tests/value/oracle/partitioning-annots.5.res.oracle b/tests/value/oracle/partitioning-annots.5.res.oracle
index d9d5c9427467bd3da95574d59b7c2dc349708ffc..801d0587fd95fdb29ed3c12eaf718725d0ffa352 100644
--- a/tests/value/oracle/partitioning-annots.5.res.oracle
+++ b/tests/value/oracle/partitioning-annots.5.res.oracle
@@ -10,8 +10,8 @@
 [eva] tests/value/partitioning-annots.c:125: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {1}, {1}
 [eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {0}, {0}
+[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {1}, {1}
 [eva] Recording results for test_history
 [eva] done for function test_history
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/postcondition.res.oracle b/tests/value/oracle/postcondition.res.oracle
index 58d0668acc827acac4a8ee62b30cb8261a403d54..5dae70a929bfd0bf441677e0e62435e6f79144da 100644
--- a/tests/value/oracle/postcondition.res.oracle
+++ b/tests/value/oracle/postcondition.res.oracle
@@ -34,10 +34,10 @@
 [eva] computing for function u <- get_index <- main.
   Called from tests/value/postcondition.i:20.
 [eva] Done for function u
-[eva] tests/value/postcondition.i:12: 
-  function get_index: postcondition got status valid.
 [eva:alarm] tests/value/postcondition.i:12: Warning: 
   function get_index: postcondition got status unknown.
+[eva] tests/value/postcondition.i:12: 
+  function get_index: postcondition got status valid.
 [eva] Recording results for get_index
 [eva] Done for function get_index
 [eva] computing for function u <- main.
diff --git a/tests/value/oracle/split_return.3.res.oracle b/tests/value/oracle/split_return.3.res.oracle
index 1ad5a6b949801e802041412d0870ce55b97cb0da..bfdd36469af1c9bd29763697bf1bcdb85c7676d6 100644
--- a/tests/value/oracle/split_return.3.res.oracle
+++ b/tests/value/oracle/split_return.3.res.oracle
@@ -26,12 +26,12 @@
   Called from tests/value/split_return.i:48.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
 [eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
 [eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
 [eva] tests/value/split_return.i:54: assertion got status valid.
 [eva] Recording results for main2
 [eva] Done for function main2
@@ -41,8 +41,8 @@
   Called from tests/value/split_return.i:73.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:76: assertion got status valid.
 [eva] tests/value/split_return.i:78: assertion got status valid.
 [eva] Recording results for main3
@@ -53,8 +53,8 @@
   Called from tests/value/split_return.i:73.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
@@ -63,8 +63,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:97: assertion got status valid.
 [eva] tests/value/split_return.i:99: assertion got status valid.
 [eva] Recording results for main4
@@ -75,8 +75,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
@@ -85,8 +85,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
@@ -95,8 +95,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
@@ -105,8 +105,8 @@
   Called from tests/value/split_return.i:117.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:120: assertion got status valid.
 [eva] tests/value/split_return.i:122: assertion got status valid.
 [eva] Recording results for main5
@@ -155,8 +155,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -165,8 +165,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -175,8 +175,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -185,8 +185,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
diff --git a/tests/value/oracle/split_return.4.res.oracle b/tests/value/oracle/split_return.4.res.oracle
index 46c3281323efa5dbd6f217ae060050721529854c..060b00fe35eb09e09e9aefee9c3feb3495500fa9 100644
--- a/tests/value/oracle/split_return.4.res.oracle
+++ b/tests/value/oracle/split_return.4.res.oracle
@@ -29,12 +29,12 @@
   Called from tests/value/split_return.i:48.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
 [eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
 [eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
 [eva] tests/value/split_return.i:54: assertion got status valid.
 [eva] Recording results for main2
 [eva] Done for function main2
@@ -44,8 +44,8 @@
   Called from tests/value/split_return.i:73.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:76: assertion got status valid.
 [eva] tests/value/split_return.i:78: assertion got status valid.
 [eva] Recording results for main3
@@ -56,8 +56,8 @@
   Called from tests/value/split_return.i:73.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
@@ -66,8 +66,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:97: assertion got status valid.
 [eva] tests/value/split_return.i:99: assertion got status valid.
 [eva] Recording results for main4
@@ -78,8 +78,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
@@ -88,8 +88,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
@@ -98,8 +98,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
@@ -108,8 +108,8 @@
   Called from tests/value/split_return.i:117.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:120: assertion got status valid.
 [eva] tests/value/split_return.i:122: assertion got status valid.
 [eva] Recording results for main5
@@ -158,8 +158,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -168,8 +168,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -178,8 +178,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -188,8 +188,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
@@ -483,8 +483,8 @@
   Called from tests/value/split_return.i:73.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main3 <- main.
@@ -493,8 +493,8 @@
   Called from tests/value/split_return.i:73.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
@@ -503,8 +503,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
@@ -513,8 +513,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
@@ -523,8 +523,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
@@ -533,8 +533,8 @@
   Called from tests/value/split_return.i:94.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
@@ -543,8 +543,8 @@
   Called from tests/value/split_return.i:117.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
 [eva] Recording results for main5
 [eva] Done for function main5
 [eva] computing for function main6 <- main.
@@ -589,8 +589,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -599,8 +599,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -609,8 +609,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
@@ -619,8 +619,8 @@
   Called from tests/value/split_return.i:171.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.