diff --git a/tests/builtins/diff_equalities b/tests/builtins/diff_equalities
index bb058d3aba7ea30f147b46ebc76985b65fe71aa9..653e7459b356bc5630d644cc3bf6d97d0bdc4041 100644
--- a/tests/builtins/diff_equalities
+++ b/tests/builtins/diff_equalities
@@ -11,34 +11,35 @@ diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_equalitie
36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
-900c898
+908c906
< r ∈ [--..--]
---
> r ∈ {42}
diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equalities/allocated.1.res.oracle
-191a192,197
+191a192,194
> [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
-> [eva] tests/builtins/allocated.c:87: Call to builtin free
-> [eva:malloc] tests/builtins/allocated.c:87:
-> strong free on bases: {__malloc_main_l82_7}
-208a215,217
+208a212,214
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-223a233,235
+223a230,232
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-238a251,253
+238a248,250
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-254,256d268
-< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+252,254c264,266
< [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
+---
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_7}
323a336,356
> [eva] tests/builtins/allocated.c:82:
> Call to builtin Frama_C_malloc_fresh for function malloc
@@ -61,9 +62,10 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [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_37
-326d358
-< [eva] Semantic level unrolling superposing up to 300 states
-329a362,382
+329,330d361
+< Trace partitioning superposing up to 300 states
+< [eva] tests/builtins/allocated.c:84:
+333a365,385
> strong free on bases: {__malloc_main_l82_37}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
@@ -85,7 +87,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> strong free on bases: {__malloc_main_l82_31}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-399c452,470
+403c455,473
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -107,7 +109,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-471c542,560
+475c545,563
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -129,7 +131,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-543c632,650
+547c635,653
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -151,7 +153,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-615c722,740
+619c725,743
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -173,7 +175,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-687c812,830
+691c815,833
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -195,7 +197,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-759c902,920
+763c905,923
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -217,7 +219,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-831c992,1010
+835c995,1013
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -239,20 +241,21 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-901,903c1080
+905,907c1083,1084
< [eva] tests/builtins/allocated.c:87: Call to builtin free
< [eva:malloc] tests/builtins/allocated.c:87:
< strong free on bases: {__malloc_main_l82_7}
---
-> [eva] Semantic level unrolling superposing up to 500 states
-1065,1067c1242,1243
+> [eva] tests/builtins/allocated.c:81:
+> Trace partitioning superposing up to 500 states
+1069,1071c1246,1247
< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
---
> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
> [1] ∈ {17} or UNINITIALIZED
-1136a1313,1333
+1140a1317,1337
> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
@@ -274,11 +277,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
-1180c1377
+1184c1381
< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
---
> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
-1203a1401,1407
+1207a1405,1411
> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
@@ -286,11 +289,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
-1227c1431
+1231c1435
< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
---
> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
-1239,1240c1443,1448
+1243,1244c1447,1452
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
---
diff --git a/tests/builtins/diff_gauges b/tests/builtins/diff_gauges
index 5a276d3cf19b4a1cf82407e32b8140c371ca444c..41ef15b15d11f3f6c7e580f7bfbe2cd2801305c1 100644
--- a/tests/builtins/diff_gauges
+++ b/tests/builtins/diff_gauges
@@ -36,10 +36,10 @@ diff tests/builtins/oracle/malloc-size-zero.1.res.oracle tests/builtins/oracle_g
> [eva] Recording results for my_calloc
> [eva] Done for function my_calloc
diff tests/builtins/oracle/memcpy.res.oracle tests/builtins/oracle_gauges/memcpy.res.oracle
-167a168,169
+168a169,170
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
-448a451
+449a452
> [eva] tests/builtins/memcpy.c:230: starting to merge loop iterations
diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/realloc.res.oracle
689a690,1038
diff --git a/tests/builtins/diff_symblocs b/tests/builtins/diff_symblocs
index f82ea2c45a6d1e4d65d053350a4b0eadd1ec1c85..9989eea8b41f2d2d7c5d3e6098d809b8d4fb00ce 100644
--- a/tests/builtins/diff_symblocs
+++ b/tests/builtins/diff_symblocs
@@ -11,7 +11,7 @@ diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_symblocs/
36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
-900c898
+908c906
< r ∈ [--..--]
---
> r ∈ {42}
diff --git a/tests/value/diff_apron b/tests/value/diff_apron
index 7b830e4e3d3a26efcc32f37b2501a9bf7cb06720..2ead3a445bbc76a876c5e89fb0e57325a79f52a0 100644
--- a/tests/value/diff_apron
+++ b/tests/value/diff_apron
@@ -415,11 +415,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_apron/local_s
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-150c142
+152c144
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
-391,393c383,385
+393,395c385,387
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
@@ -427,15 +427,15 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_apron/local_s
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-396c388
+398c390
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
-400c392
+402c394
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
-404,412c396
+406,414c398
< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
< [eva] tests/value/local_slevel.i:18:
< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
@@ -447,11 +447,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_apron/local_s
< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
---
> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
-414c398
+416c400
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-528c512
+532c516
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
@@ -618,10 +618,10 @@ diff tests/value/oracle/memexec.res.oracle tests/value/oracle_apron/memexec.res.
> g_f5_1 ∈ [-2147483648..6]
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.oracle
40a41,64
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
@@ -636,37 +636,37 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.or
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {1; 2; 3; 4; 5; 6; 7},
> {-6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
50a75,98
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {1; 2; 3; 4; 5; 6; 7},
> {-6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
60a109,110
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
@@ -714,6 +714,10 @@ diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_apron/offsetma
> a ∈ {1; 6}
> b ∈ {0; 1}
> a7 ∈ {1}
+diff tests/value/oracle/partitioning-annots.4.res.oracle tests/value/oracle_apron/partitioning-annots.4.res.oracle
+14,15d13
+< [eva:alarm] tests/value/partitioning-annots.c:134: Warning:
+< division by zero. assert j ≢ 0;
diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/precise_locations.res.oracle
32,35c32,47
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
@@ -972,6 +976,9 @@ diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_apron/unroll
< j ∈ [-2147483648..-126]
---
> j ∈ {-250}
+diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_apron/widen_on_non_monotonic.res.oracle
+25a26
+> [eva] tests/value/widen_on_non_monotonic.i:21: starting to merge loop iterations
diff tests/value/oracle/with_comment.res.oracle tests/value/oracle_apron/with_comment.res.oracle
9,10d8
< [eva:alarm] tests/value/with_comment.i:21: Warning:
diff --git a/tests/value/diff_equalities b/tests/value/diff_equalities
index dff0951199db5e7fd420203047add34788d4aa4f..821b7e3c2fc6803fa2584c2b2deedc7692ba8b60 100644
--- a/tests/value/diff_equalities
+++ b/tests/value/diff_equalities
@@ -379,10 +379,10 @@ diff tests/value/oracle/long_const.1.res.oracle tests/value/oracle_equalities/lo
> [eva] Done for function LL_ABS
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.res.oracle
40a41,119
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
@@ -397,10 +397,9 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> {-8; -7; -6; -5; -4; -3; -2; -1},
+> {-7; -6; -5; -4; -3; -2; -1},
+> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
@@ -408,9 +407,10 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1; 0}
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
@@ -426,16 +426,16 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> {-6; -5; -4; -3; -2; -1},
> {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
+> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:41:
@@ -445,13 +445,13 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
+> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {1; 2}, {-1; 0}
@@ -459,28 +459,22 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {-2; -1}, {-1; 0}
50a130,208
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-8; -7; -6; -5; -4; -3; -2; -1},
@@ -493,23 +487,24 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
+> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
+> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-7; -6; -5; -4; -3; -2; -1},
> {-6; -5; -4; -3; -2; -1},
> {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
@@ -517,27 +512,32 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> Frama_C_show_each_2:
> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
+> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
+> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-3; -2; -1}, {1; 2}, {-1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-3; -2; -1}, {-2; -1}, {-1; 0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
60a219,231
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index 26c5b6d4c45adaf15845328b27805fab45e865c8..e0312fea2b92804faca6c4ccae3d2e2afc83fda6 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -447,11 +447,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_gauges/local_
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-150c142
+152c144
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
-391,393c383,385
+393,395c385,387
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
@@ -459,15 +459,15 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_gauges/local_
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-396c388
+398c390
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
-400c392
+402c394
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
-404,412c396
+406,414c398
< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
< [eva] tests/value/local_slevel.i:18:
< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
@@ -479,11 +479,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_gauges/local_
< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
---
> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
-414c398
+416c400
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-528c512
+532c516
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
@@ -516,10 +516,10 @@ diff tests/value/oracle/memexec.res.oracle tests/value/oracle_gauges/memexec.res
> [eva] tests/value/memexec.c:98: starting to merge loop iterations
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.oracle
40a41,123
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
@@ -534,10 +534,9 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> {-8; -7; -6; -5; -4; -3; -2; -1},
+> {-7; -6; -5; -4; -3; -2; -1},
+> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
@@ -545,9 +544,10 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1; 0}
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
@@ -563,16 +563,16 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> {-6; -5; -4; -3; -2; -1},
> {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
-> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
+> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:41:
@@ -582,46 +582,40 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
+> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {1; 2}, {-1; 0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {-2; -1}, {0; 1}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {-2; -1}, {-1; 0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {1}, {0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {-1}, {0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {1}, {0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {-1}, {0}
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {1}, {0}
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {-1}, {0}
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {1}, {0}
50a134,216
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-8; -7; -6; -5; -4; -3; -2; -1},
@@ -634,23 +628,24 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
+> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
+> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-7; -6; -5; -4; -3; -2; -1},
> {-6; -5; -4; -3; -2; -1},
> {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
@@ -658,31 +653,36 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> Frama_C_show_each_2:
> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
+> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
+> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-3; -2; -1}, {1; 2}, {-1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-3; -2; -1}, {-2; -1}, {-1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {1}, {0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {-1}, {0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {-2; -1}, {1}, {0}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {-2; -1}, {-1}, {0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {1}, {0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {-1}, {0}
60a227,240
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
diff --git a/tests/value/diff_symblocs b/tests/value/diff_symblocs
index 66cf8a0b6bf76c5caef27141819a4501e728ec9e..fdad91d414bade1b59b31b4515da631d2e84385e 100644
--- a/tests/value/diff_symblocs
+++ b/tests/value/diff_symblocs
@@ -50,86 +50,6 @@ diff tests/value/oracle/bitwise_reduction.res.oracle tests/value/oracle_symblocs
< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
---
> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
-diff tests/value/oracle/builtins_split.res.oracle tests/value/oracle_symblocs/builtins_split.res.oracle
-68a69,70
-> [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
-98a101,144
-> [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] 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
-133a180,209
-> [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}
-> [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}
diff tests/value/oracle/incompatible_states.res.oracle tests/value/oracle_symblocs/incompatible_states.res.oracle
39,40d38
< [eva:alarm] tests/value/incompatible_states.c:53: Warning: