diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
index 1d083a1c84154a7c112a4f25e84cdf468ac7bbbf..81e4f54353158d275b6387b5a97dd8447577d736 100644
--- a/tests/value/auto_loop_unroll.c
+++ b/tests/value/auto_loop_unroll.c
@@ -159,7 +159,19 @@ void complex_loops () {
i = 0;
while (i < 64) {
for (int j = 0; j < i; j++) {
- i++;
+ if (undet && i < 64)
+ i++; // The outer loop could be unrolled, as this speeds up convergence.
+ }
+ res++;
+ i++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ i = 0;
+ while (i < 64) {
+ for (int j = 0; j < i; j++) {
+ if (undet && i > 0)
+ i--; // The outer loop cannot be unrolled.
}
res++;
i++;
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
index f34b2d3391c550082ac44d8e02e57b4b4b1e1dc7..485d1f41d3be3aba44e9b92bc38ab195c6ca6809 100644
--- a/tests/value/oracle/auto_loop_unroll.0.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle
@@ -6,7 +6,7 @@
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
- Called from tests/value/auto_loop_unroll.c:416.
+ Called from tests/value/auto_loop_unroll.c:428.
[eva] tests/value/auto_loop_unroll.c:24: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:25: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -27,7 +27,7 @@
[eva] Recording results for simple_loops
[eva] Done for function simple_loops
[eva] computing for function various_loops <- main.
- Called from tests/value/auto_loop_unroll.c:417.
+ Called from tests/value/auto_loop_unroll.c:429.
[eva] tests/value/auto_loop_unroll.c:57: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:58: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -146,7 +146,7 @@
[eva] Recording results for various_loops
[eva] Done for function various_loops
[eva] computing for function complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:418.
+ Called from tests/value/auto_loop_unroll.c:430.
[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:154: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -154,201 +154,203 @@
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:160: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:162: Warning:
- signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
- signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:167:
+[eva] tests/value/auto_loop_unroll.c:168:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
+[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:176: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:176:
+[eva] tests/value/auto_loop_unroll.c:179:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:183: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:186: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:188:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-[eva:alarm] tests/value/auto_loop_unroll.c:183: Warning:
+[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:195: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:185:
+[eva] tests/value/auto_loop_unroll.c:197:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:190: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+[eva] tests/value/auto_loop_unroll.c:202: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:194:
+[eva] tests/value/auto_loop_unroll.c:206:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:198: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+[eva] tests/value/auto_loop_unroll.c:210: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:199: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:211: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:202:
+[eva] tests/value/auto_loop_unroll.c:214:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] Recording results for complex_loops
[eva] Done for function complex_loops
[eva] computing for function various_conditions <- main.
- Called from tests/value/auto_loop_unroll.c:419.
-[eva] tests/value/auto_loop_unroll.c:211: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
+ Called from tests/value/auto_loop_unroll.c:431.
+[eva] tests/value/auto_loop_unroll.c:223: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:224: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:216: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
+[eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:228: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:229: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:222: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+[eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:234: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:222: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:234: Warning:
signed overflow. assert -2147483648 ≤ i_0 - 1;
-[eva] tests/value/auto_loop_unroll.c:225:
+[eva] tests/value/auto_loop_unroll.c:237:
Frama_C_show_each_0_13: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:227: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+[eva] tests/value/auto_loop_unroll.c:239: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:227: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:239: Warning:
signed overflow. assert -2147483648 ≤ i_1 - 1;
-[eva] tests/value/auto_loop_unroll.c:230:
+[eva] tests/value/auto_loop_unroll.c:242:
Frama_C_show_each_0_14: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:233: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
+[eva] tests/value/auto_loop_unroll.c:245: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:248: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:238:
+[eva] tests/value/auto_loop_unroll.c:250:
Frama_C_show_each_0_15: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:240: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
+[eva] tests/value/auto_loop_unroll.c:252: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:253: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:245:
+[eva] tests/value/auto_loop_unroll.c:257:
Frama_C_show_each_11_111: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:250: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:251: Warning:
+[eva] tests/value/auto_loop_unroll.c:262: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [0..2147483647]
[eva] Recording results for various_conditions
[eva] Done for function various_conditions
[eva] computing for function temporary_variables <- main.
- Called from tests/value/auto_loop_unroll.c:420.
-[eva] tests/value/auto_loop_unroll.c:262: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:262: Warning:
+ Called from tests/value/auto_loop_unroll.c:432.
+[eva] tests/value/auto_loop_unroll.c:274: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:274: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:275: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:267: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
+[eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:279: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:280: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:279: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:272: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:274: Warning:
+[eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:284: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:286: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:272: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:279: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:282: Warning:
+[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:291: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:294: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:279: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:291: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:287: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:290: Warning:
+[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:299: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:302: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647]
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] computing for function loops_with_goto <- main.
- Called from tests/value/auto_loop_unroll.c:421.
-[eva] tests/value/auto_loop_unroll.c:298: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
+ Called from tests/value/auto_loop_unroll.c:433.
+[eva] tests/value/auto_loop_unroll.c:310: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:311: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:308: Warning:
+[eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:320: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:312: Frama_C_show_each_top: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:315: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:316: Warning:
+[eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:324: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:327: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:328: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:325: Warning:
+[eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:337: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:324: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:329:
+[eva] tests/value/auto_loop_unroll.c:336: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:341:
Frama_C_show_each_33_inf: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:333: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:345: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:332: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:332: Warning:
+[eva] tests/value/auto_loop_unroll.c:344: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:344: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:337: Frama_C_show_each_top: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:340: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:343: Warning:
+[eva] tests/value/auto_loop_unroll.c:349: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:352: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:355: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:345:
+[eva] tests/value/auto_loop_unroll.c:357:
Frama_C_show_each_0_35: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:348: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+[eva] tests/value/auto_loop_unroll.c:360: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:355: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:358: Warning:
+[eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:367: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:370: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: [0..2147483647]
[eva] Recording results for loops_with_goto
[eva] Done for function loops_with_goto
[eva] computing for function non_natural_loops <- main.
- Called from tests/value/auto_loop_unroll.c:422.
-[eva:alarm] tests/value/auto_loop_unroll.c:371: Warning:
+ Called from tests/value/auto_loop_unroll.c:434.
+[eva:alarm] tests/value/auto_loop_unroll.c:383: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:379: Warning:
+[eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: [1..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:391: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:380: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:383:
+[eva] tests/value/auto_loop_unroll.c:395:
Frama_C_show_each_1_51: [1..2147483647]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
[eva] computing for function following_loops <- main.
- Called from tests/value/auto_loop_unroll.c:423.
-[eva] tests/value/auto_loop_unroll.c:390: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
+ Called from tests/value/auto_loop_unroll.c:435.
+[eva] tests/value/auto_loop_unroll.c:402: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:404: Warning:
signed overflow. assert j + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:396: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:408: Warning:
signed overflow. assert j + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:394: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:401: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:403: Warning:
+[eva] tests/value/auto_loop_unroll.c:406: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:413: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:415: Warning:
signed overflow. assert j + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:407: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:419: Warning:
signed overflow. assert j + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:405: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:417: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [0..2147483647]
[eva] Recording results for following_loops
[eva] Done for function following_loops
[eva] Recording results for main
@@ -471,7 +473,7 @@
[inout] Inputs for function incr_g:
g
[inout] Out (internal) for function complex_loops:
- g; res; i; j; p; j_0; t[0..9]
+ g; res; i; j; p; j_0; j_1; t[0..9]
[inout] Inputs for function complex_loops:
undet; g
[inout] Out (internal) for function loops_with_goto:
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 1826be4c45b15e28b686ca1477a15430deaba845..1a4b5f83bab11263da5a047cb211f4f69164591a 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -6,7 +6,7 @@
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
- Called from tests/value/auto_loop_unroll.c:416.
+ Called from tests/value/auto_loop_unroll.c:428.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:24: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:24:
Trace partitioning superposing up to 100 states
@@ -25,7 +25,7 @@
[eva] Recording results for simple_loops
[eva] Done for function simple_loops
[eva] computing for function various_loops <- main.
- Called from tests/value/auto_loop_unroll.c:417.
+ Called from tests/value/auto_loop_unroll.c:429.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:57: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:62: Automatic loop unrolling.
@@ -287,7 +287,7 @@
[eva] Recording results for various_loops
[eva] Done for function various_loops
[eva] computing for function complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:418.
+ Called from tests/value/auto_loop_unroll.c:430.
[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:154: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -295,143 +295,145 @@
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:160: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:162: Warning:
- signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
- signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:167:
+[eva] tests/value/auto_loop_unroll.c:168:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
+[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:176: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:179:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:183: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:186: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:176:
+[eva] tests/value/auto_loop_unroll.c:188:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:181.
+ Called from tests/value/auto_loop_unroll.c:193.
[eva] Recording results for incr_g
[eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-[eva:alarm] tests/value/auto_loop_unroll.c:183: Warning:
+[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:195: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:185:
+[eva] tests/value/auto_loop_unroll.c:197:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:190: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+[eva] tests/value/auto_loop_unroll.c:202: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:194:
+[eva] tests/value/auto_loop_unroll.c:206:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:198: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+[eva] tests/value/auto_loop_unroll.c:210: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:199: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:211: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:202:
+[eva] tests/value/auto_loop_unroll.c:214:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] Recording results for complex_loops
[eva] Done for function complex_loops
[eva] computing for function various_conditions <- main.
- Called from tests/value/auto_loop_unroll.c:419.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:211: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:216: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:222: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:225: Frama_C_show_each_0_13: [0..13]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:227: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:230: Frama_C_show_each_0_14: [0..14]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:233: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_0_15: [0..15]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:240:
+ Called from tests/value/auto_loop_unroll.c:431.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:223: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: {11}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:228: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: {12}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:234: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:237: Frama_C_show_each_0_13: [0..13]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:239: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:242: Frama_C_show_each_0_14: [0..14]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:245: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:250: Frama_C_show_each_0_15: [0..15]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:252: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:252:
Trace partitioning superposing up to 100 states
-[eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:250: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: {16}
+[eva] tests/value/auto_loop_unroll.c:257: Frama_C_show_each_11_111: [11..111]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:262: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: {16}
[eva] Recording results for various_conditions
[eva] Done for function various_conditions
[eva] computing for function temporary_variables <- main.
- Called from tests/value/auto_loop_unroll.c:420.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:262: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: {20}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:267: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:272: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: {22}
+ Called from tests/value/auto_loop_unroll.c:432.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:274: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: {20}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:279: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: {23}
-[eva] tests/value/auto_loop_unroll.c:287: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:290: Warning:
+[eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: {21}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:284: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: {22}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:291: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: {23}
+[eva] tests/value/auto_loop_unroll.c:299: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:302: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647]
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] computing for function loops_with_goto <- main.
- Called from tests/value/auto_loop_unroll.c:421.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:298: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:307: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:308: Warning:
+ Called from tests/value/auto_loop_unroll.c:433.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:310: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: {30}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:319: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:320: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:307:
+[eva] tests/value/auto_loop_unroll.c:319:
Trace partitioning superposing up to 100 states
-[eva] tests/value/auto_loop_unroll.c:312:
+[eva] tests/value/auto_loop_unroll.c:324:
Frama_C_show_each_top: [31..2147483647]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:315: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: {32}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:324: Automatic loop unrolling.
-[eva:alarm] tests/value/auto_loop_unroll.c:325: Warning:
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:327: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: {32}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:336: Automatic loop unrolling.
+[eva:alarm] tests/value/auto_loop_unroll.c:337: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:329:
+[eva] tests/value/auto_loop_unroll.c:341:
Frama_C_show_each_33_inf: [33..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:333: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:345: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:332: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:332: Warning:
+[eva] tests/value/auto_loop_unroll.c:344: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:344: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:337: Frama_C_show_each_top: [0..2147483647]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:340: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:345: Frama_C_show_each_0_35: [0..35]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:348: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: {36}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:355: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: {27}
+[eva] tests/value/auto_loop_unroll.c:349: Frama_C_show_each_top: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:352: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:357: Frama_C_show_each_0_35: [0..35]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:360: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: {36}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:367: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: {27}
[eva] Recording results for loops_with_goto
[eva] Done for function loops_with_goto
[eva] computing for function non_natural_loops <- main.
- Called from tests/value/auto_loop_unroll.c:422.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:370: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:379: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:383: Frama_C_show_each_1_51: [1..51]
+ Called from tests/value/auto_loop_unroll.c:434.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:382: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: {50}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:391: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:395: Frama_C_show_each_1_51: [1..51]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
[eva] computing for function following_loops <- main.
- Called from tests/value/auto_loop_unroll.c:423.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:390: Automatic loop unrolling.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:394: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:401: Automatic loop unrolling.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:405: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45]
+ Called from tests/value/auto_loop_unroll.c:435.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:402: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:406: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: {30}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:413: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:417: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [15..45]
[eva] Recording results for following_loops
[eva] Done for function following_loops
[eva] Recording results for main
@@ -554,7 +556,7 @@
[inout] Inputs for function incr_g:
g
[inout] Out (internal) for function complex_loops:
- g; res; i; j; p; j_0; t[0..9]
+ g; res; i; j; p; j_0; j_1; t[0..9]
[inout] Inputs for function complex_loops:
undet; g
[inout] Out (internal) for function loops_with_goto:
diff --git a/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle b/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle
index a327adacc6b58b32c198364c25748edc883450ae..1fb1e4da2fc9a40d8f8e546dc3b3d7a33a9b9348 100644
--- a/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle
+++ b/tests/value/oracle_apron/auto_loop_unroll.0.res.oracle
@@ -120,206 +120,214 @@
< [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [0..2147483647]
---
> [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [3..2147483647]
-161,162d145
-< [eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
+157,160c142
+< [eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-169c152
+< [eva] tests/value/auto_loop_unroll.c:168:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:168: Frama_C_show_each_imprecise: [0..65]
+166c148
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> Frama_C_show_each_imprecise: [64..2147483647]
+171c153
< Frama_C_show_each_imprecise: [0..2147483647]
---
> Frama_C_show_each_imprecise: [10..2147483647]
-187,192c170,178
-< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-< [eva:alarm] tests/value/auto_loop_unroll.c:183: Warning:
+189,194c171,179
+< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+< [eva:alarm] tests/value/auto_loop_unroll.c:195: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:185:
+< [eva] tests/value/auto_loop_unroll.c:197:
< Frama_C_show_each_imprecise: [0..2147483647]
---
> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:181.
+> Called from tests/value/auto_loop_unroll.c:193.
> [eva] Recording results for incr_g
> [eva] Done for function incr_g
> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:181.
+> Called from tests/value/auto_loop_unroll.c:193.
> [eva] Recording results for incr_g
> [eva] Done for function incr_g
-> [eva] tests/value/auto_loop_unroll.c:185: Frama_C_show_each_imprecise: [0..64]
-194,197c180
-< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+> [eva] tests/value/auto_loop_unroll.c:197: Frama_C_show_each_imprecise: [0..64]
+196,199c181
+< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:194:
+< [eva] tests/value/auto_loop_unroll.c:206:
< Frama_C_show_each_imprecise: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [0..9]
-199,200d181
-< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [0..9]
+201,202d182
+< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-204c185
+206c186
< Frama_C_show_each_imprecise: [0..2147483647]
---
> Frama_C_show_each_imprecise: [64..2147483647]
-210,212c191
-< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
+212,214c192
+< [eva:alarm] tests/value/auto_loop_unroll.c:224: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11}
-214,216c193
-< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
+> [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: {11}
+216,218c194
+< [eva:alarm] tests/value/auto_loop_unroll.c:229: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12}
-218,219d194
-< [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+> [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: {12}
+220,221d195
+< [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-221a197,198
-> [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+223a198,199
+> [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-225,226d201
-< [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+227,228d202
+< [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-228a204,205
-> [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+230a205,206
+> [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-232,233d208
-< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
+234,235d209
+< [eva:alarm] tests/value/auto_loop_unroll.c:248: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-237,240c212
-< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
+239,242c213
+< [eva:alarm] tests/value/auto_loop_unroll.c:253: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:245:
+< [eva] tests/value/auto_loop_unroll.c:257:
< Frama_C_show_each_11_111: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111]
-242,244c214
-< [eva:alarm] tests/value/auto_loop_unroll.c:251: Warning:
+> [eva] tests/value/auto_loop_unroll.c:257: Frama_C_show_each_11_111: [11..111]
+244,246c215
+< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [16..2147483647]
-252,254c222
-< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
+> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [16..2147483647]
+254,256c223
+< [eva:alarm] tests/value/auto_loop_unroll.c:275: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [20..2147483646]
-256,257d223
-< [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
+> [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [20..2147483646]
+258,259d224
+< [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-260,262c226
-< [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647]
-< [eva] tests/value/auto_loop_unroll.c:272: starting to merge loop iterations
-< [eva:alarm] tests/value/auto_loop_unroll.c:274: Warning:
----
-> [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
-264,266c228,230
-< [eva:alarm] tests/value/auto_loop_unroll.c:272: Warning:
+262,264c227
+< [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:284: starting to merge loop iterations
+< [eva:alarm] tests/value/auto_loop_unroll.c:286: Warning:
+---
+> [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning:
+266,268c229,231
+< [eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
< signed overflow. assert i + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21}
-> [eva] tests/value/auto_loop_unroll.c:272: starting to merge loop iterations
-> [eva] tests/value/auto_loop_unroll.c:276: Frama_C_show_each_22: {21; 22}
-268,272c232
-< [eva:alarm] tests/value/auto_loop_unroll.c:282: Warning:
+> [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: {21}
+> [eva] tests/value/auto_loop_unroll.c:284: starting to merge loop iterations
+> [eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_22: {21; 22}
+270,274c233
+< [eva:alarm] tests/value/auto_loop_unroll.c:294: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning:
+< [eva:alarm] tests/value/auto_loop_unroll.c:291: Warning:
< signed overflow. assert i + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:284: Frama_C_show_each_23: {22; 23}
-276,278c236,237
-< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
+> [eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_23: {22; 23}
+278,280c237,238
+< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
< signed overflow. assert i + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:292:
+> [eva] tests/value/auto_loop_unroll.c:304:
> Frama_C_show_each_top: [23..2147483647]
-284,286c243,244
-< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
+286,288c244,245
+< [eva:alarm] tests/value/auto_loop_unroll.c:311: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30}
-> [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-289,290c247,248
-< [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-< [eva] tests/value/auto_loop_unroll.c:312: Frama_C_show_each_top: [0..2147483647]
+> [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: {30}
+> [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations
+291,292c248,249
+< [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations
+< [eva] tests/value/auto_loop_unroll.c:324: Frama_C_show_each_top: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:312:
+> [eva] tests/value/auto_loop_unroll.c:324:
> Frama_C_show_each_top: [31..2147483647]
-292,294c250
-< [eva:alarm] tests/value/auto_loop_unroll.c:316: Warning:
+294,296c251
+< [eva:alarm] tests/value/auto_loop_unroll.c:328: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: {32}
-299c255
+> [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: {32}
+301c256
< Frama_C_show_each_33_inf: [0..2147483647]
---
> Frama_C_show_each_33_inf: [33..2147483647]
-303,304d258
-< [eva:alarm] tests/value/auto_loop_unroll.c:332: Warning:
+305,306d259
+< [eva:alarm] tests/value/auto_loop_unroll.c:344: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-307,310c261
-< [eva:alarm] tests/value/auto_loop_unroll.c:343: Warning:
+309,312c262
+< [eva:alarm] tests/value/auto_loop_unroll.c:355: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:345:
+< [eva] tests/value/auto_loop_unroll.c:357:
< Frama_C_show_each_0_35: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:345: Frama_C_show_each_0_35: [0..35]
-313,314d263
+> [eva] tests/value/auto_loop_unroll.c:357: Frama_C_show_each_0_35: [0..35]
+315,316d264
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
-316,318c265
-< [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: [0..2147483647]
-< [eva] tests/value/auto_loop_unroll.c:355: starting to merge loop iterations
-< [eva:alarm] tests/value/auto_loop_unroll.c:358: Warning:
----
-> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
-320c267,269
-< [eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: {36}
-> [eva] tests/value/auto_loop_unroll.c:355: starting to merge loop iterations
-> [eva] tests/value/auto_loop_unroll.c:360: Frama_C_show_each_27: [0..37]
-325,327c274
-< [eva:alarm] tests/value/auto_loop_unroll.c:371: Warning:
+< [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
+318,320c266
+< [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:367: starting to merge loop iterations
+< [eva:alarm] tests/value/auto_loop_unroll.c:370: Warning:
+---
+> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
+322c268,270
+< [eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: {36}
+> [eva] tests/value/auto_loop_unroll.c:367: starting to merge loop iterations
+> [eva] tests/value/auto_loop_unroll.c:372: Frama_C_show_each_27: [0..37]
+327,329c275
+< [eva:alarm] tests/value/auto_loop_unroll.c:383: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: [1..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50}
-330,331d276
-< [eva:alarm] tests/value/auto_loop_unroll.c:380: Warning:
-< signed overflow. assert -2147483648 ≤ i - 1;
-339,342d283
+> [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: {50}
+332,333d277
< [eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
+< signed overflow. assert -2147483648 ≤ i - 1;
+341,344d284
+< [eva:alarm] tests/value/auto_loop_unroll.c:404: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-< [eva:alarm] tests/value/auto_loop_unroll.c:396: Warning:
+< [eva:alarm] tests/value/auto_loop_unroll.c:408: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-344c285
-< [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647]
+346c286
+< [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30}
-346,349d286
-< [eva:alarm] tests/value/auto_loop_unroll.c:403: Warning:
+> [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: {30}
+348,351d287
+< [eva:alarm] tests/value/auto_loop_unroll.c:415: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-< [eva:alarm] tests/value/auto_loop_unroll.c:407: Warning:
+< [eva:alarm] tests/value/auto_loop_unroll.c:419: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-351c288
-< [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647]
+353c289
+< [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: {30}
-361c298
+> [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: {30}
+363c299
< __retres ∈ [1..2147483647]
---
> __retres ∈ [1..25]
-363c300
+365c301
< g ∈ [1..2147483647]
---
> g ∈ [1..126]
-391c328
+393c329
< k ∈ [22..2147483647]
---
> k ∈ {22}
diff --git a/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle b/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle
index 702df814fedff678c3b0b1c0cf8476d6a588c359..6094367647e11eab9abe112c53a07a27ed4c8837 100644
--- a/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle_apron/auto_loop_unroll.1.res.oracle
@@ -191,120 +191,128 @@
< [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [0..2147483647]
---
> [eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [3..2147483647]
-302,303d370
-< [eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
+298,301c367
+< [eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-310c377
+< [eva] tests/value/auto_loop_unroll.c:168:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:168: Frama_C_show_each_imprecise: [0..65]
+307c373
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> Frama_C_show_each_imprecise: [64..2147483647]
+312c378
< Frama_C_show_each_imprecise: [0..2147483647]
---
> Frama_C_show_each_imprecise: [10..2147483647]
-328,333c395,403
-< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-< [eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
-< [eva:alarm] tests/value/auto_loop_unroll.c:183: Warning:
+330,335c396,404
+< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+< [eva] tests/value/auto_loop_unroll.c:193: Reusing old results for call to incr_g
+< [eva:alarm] tests/value/auto_loop_unroll.c:195: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:185:
+< [eva] tests/value/auto_loop_unroll.c:197:
< Frama_C_show_each_imprecise: [0..2147483647]
---
> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:181.
+> Called from tests/value/auto_loop_unroll.c:193.
> [eva] Recording results for incr_g
> [eva] Done for function incr_g
> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:181.
+> Called from tests/value/auto_loop_unroll.c:193.
> [eva] Recording results for incr_g
> [eva] Done for function incr_g
-> [eva] tests/value/auto_loop_unroll.c:185: Frama_C_show_each_imprecise: [0..64]
-335,338c405
-< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+> [eva] tests/value/auto_loop_unroll.c:197: Frama_C_show_each_imprecise: [0..64]
+337,340c406
+< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:194:
+< [eva] tests/value/auto_loop_unroll.c:206:
< Frama_C_show_each_imprecise: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [0..9]
-340,341d406
-< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [0..9]
+342,343d407
+< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-345c410
+347c411
< Frama_C_show_each_imprecise: [0..2147483647]
---
> Frama_C_show_each_imprecise: [64..2147483647]
-350c415
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:211: Automatic loop unrolling.
----
-> [eva] tests/value/auto_loop_unroll.c:211: starting to merge loop iterations
-352c417
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:216: Automatic loop unrolling.
----
-> [eva] tests/value/auto_loop_unroll.c:216: starting to merge loop iterations
-354,359c419,435
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:222: Automatic loop unrolling.
-< [eva] tests/value/auto_loop_unroll.c:225: Frama_C_show_each_0_13: [0..13]
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:227: Automatic loop unrolling.
-< [eva] tests/value/auto_loop_unroll.c:230: Frama_C_show_each_0_14: [0..14]
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:233: Automatic loop unrolling.
-< [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_0_15: [0..15]
----
-> [eva] tests/value/auto_loop_unroll.c:222: starting to merge loop iterations
-> [eva:alarm] tests/value/auto_loop_unroll.c:222: Warning:
+352c416
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:223: Automatic loop unrolling.
+---
+> [eva] tests/value/auto_loop_unroll.c:223: starting to merge loop iterations
+354c418
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:228: Automatic loop unrolling.
+---
+> [eva] tests/value/auto_loop_unroll.c:228: starting to merge loop iterations
+356,361c420,436
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:234: Automatic loop unrolling.
+< [eva] tests/value/auto_loop_unroll.c:237: Frama_C_show_each_0_13: [0..13]
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:239: Automatic loop unrolling.
+< [eva] tests/value/auto_loop_unroll.c:242: Frama_C_show_each_0_14: [0..14]
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:245: Automatic loop unrolling.
+< [eva] tests/value/auto_loop_unroll.c:250: Frama_C_show_each_0_15: [0..15]
+---
+> [eva] tests/value/auto_loop_unroll.c:234: starting to merge loop iterations
+> [eva:alarm] tests/value/auto_loop_unroll.c:234: Warning:
> signed overflow. assert -2147483648 ≤ i_0 - 1;
-> [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+> [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:225:
+> [eva] tests/value/auto_loop_unroll.c:237:
> Frama_C_show_each_0_13: [0..2147483647]
-> [eva] tests/value/auto_loop_unroll.c:227: starting to merge loop iterations
-> [eva:alarm] tests/value/auto_loop_unroll.c:227: Warning:
+> [eva] tests/value/auto_loop_unroll.c:239: starting to merge loop iterations
+> [eva:alarm] tests/value/auto_loop_unroll.c:239: Warning:
> signed overflow. assert -2147483648 ≤ i_1 - 1;
-> [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+> [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:230:
+> [eva] tests/value/auto_loop_unroll.c:242:
> Frama_C_show_each_0_14: [0..2147483647]
-> [eva] tests/value/auto_loop_unroll.c:233: starting to merge loop iterations
-> [eva] tests/value/auto_loop_unroll.c:238:
+> [eva] tests/value/auto_loop_unroll.c:245: starting to merge loop iterations
+> [eva] tests/value/auto_loop_unroll.c:250:
> Frama_C_show_each_0_15: [0..2147483647]
-372c448,452
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:267: Automatic loop unrolling.
+374c449,453
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:279: Automatic loop unrolling.
---
-> [eva] tests/value/auto_loop_unroll.c:267: starting to merge loop iterations
-> [eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
+> [eva] tests/value/auto_loop_unroll.c:279: starting to merge loop iterations
+> [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning:
> signed overflow. assert -2147483648 ≤ i - 1;
-> [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
+> [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-381,383c461,462
-< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
+383,385c462,463
+< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
< signed overflow. assert i + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:292: Frama_C_show_each_top: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_top: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:292:
+> [eva] tests/value/auto_loop_unroll.c:304:
> Frama_C_show_each_top: [23..2147483647]
-408,409d486
-< [eva:alarm] tests/value/auto_loop_unroll.c:332: Warning:
+410,411d487
+< [eva:alarm] tests/value/auto_loop_unroll.c:344: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-413c490,494
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:348: Automatic loop unrolling.
+415c491,495
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:360: Automatic loop unrolling.
---
-> [eva] tests/value/auto_loop_unroll.c:348: starting to merge loop iterations
-> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+> [eva] tests/value/auto_loop_unroll.c:360: starting to merge loop iterations
+> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
> signed overflow. assert -2147483648 ≤ i - 1;
-> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-423,424c504,507
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:379: Automatic loop unrolling.
-< [eva] tests/value/auto_loop_unroll.c:383: Frama_C_show_each_1_51: [1..51]
+425,426c505,508
+< [eva:loop-unroll] tests/value/auto_loop_unroll.c:391: Automatic loop unrolling.
+< [eva] tests/value/auto_loop_unroll.c:395: Frama_C_show_each_1_51: [1..51]
---
-> [eva:alarm] tests/value/auto_loop_unroll.c:379: Warning:
+> [eva:alarm] tests/value/auto_loop_unroll.c:391: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:383:
+> [eva] tests/value/auto_loop_unroll.c:395:
> Frama_C_show_each_1_51: [1..2147483647]
-434c517
-< [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45]
+436c518
+< [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [15..45]
---
-> [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: {30}
-442c525
+> [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: {30}
+444c526
< j ∈ [15..45]
---
> j ∈ [15..30]
-467c550
+469c551
< i ∈ [-1..50]
---
> i ∈ [-2147483648..50]
diff --git a/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle b/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle
index b53899a72738a7c9f35605d4cba511a0cb611d45..acb3b936b41fb972ec550113fd21dcb346e961f3 100644
--- a/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle
+++ b/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle
@@ -57,139 +57,139 @@
< Frama_C_show_each_32_64: [0..2147483647]
---
> [eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..65]
-194,197c172
-< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+196,199c174
+< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:194:
+< [eva] tests/value/auto_loop_unroll.c:206:
< Frama_C_show_each_imprecise: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [1..9]
-199,200d173
-< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [1..9]
+201,202d175
+< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-204c177
+206c179
< Frama_C_show_each_imprecise: [0..2147483647]
---
> Frama_C_show_each_imprecise: [64..2147483647]
-210,212c183
-< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
+212,214c185
+< [eva:alarm] tests/value/auto_loop_unroll.c:224: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11}
-214,216c185
-< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
+> [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11: {11}
+216,218c187
+< [eva:alarm] tests/value/auto_loop_unroll.c:229: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12}
-218,219d186
-< [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+> [eva] tests/value/auto_loop_unroll.c:231: Frama_C_show_each_12: {12}
+220,221d188
+< [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-221a189,190
-> [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+223a191,192
+> [eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-225,226d193
-< [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+227,228d195
+< [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-228a196,197
-> [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+230a198,199
+> [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-232,233d200
-< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
+234,235d202
+< [eva:alarm] tests/value/auto_loop_unroll.c:248: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-237,240c204
-< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
+239,242c206
+< [eva:alarm] tests/value/auto_loop_unroll.c:253: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:245:
+< [eva] tests/value/auto_loop_unroll.c:257:
< Frama_C_show_each_11_111: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111]
-242,244c206
-< [eva:alarm] tests/value/auto_loop_unroll.c:251: Warning:
+> [eva] tests/value/auto_loop_unroll.c:257: Frama_C_show_each_11_111: [11..111]
+244,246c208
+< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [16..2147483647]
-252,254c214
-< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
+> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_16: [16..2147483647]
+254,256c216
+< [eva:alarm] tests/value/auto_loop_unroll.c:275: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [20..2147483646]
-256,257d215
-< [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
+> [eva] tests/value/auto_loop_unroll.c:277: Frama_C_show_each_20: [20..2147483646]
+258,259d217
+< [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-260c218,220
-< [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647]
+262c220,222
+< [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: [0..2147483647]
---
-> [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
+> [eva:alarm] tests/value/auto_loop_unroll.c:280: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21}
-264,265d223
-< [eva:alarm] tests/value/auto_loop_unroll.c:272: Warning:
+> [eva] tests/value/auto_loop_unroll.c:282: Frama_C_show_each_21: {21}
+266,267d225
+< [eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
< signed overflow. assert i + 1 ≤ 2147483647;
-270,271d227
-< [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning:
+272,273d229
+< [eva:alarm] tests/value/auto_loop_unroll.c:291: Warning:
< signed overflow. assert i + 1 ≤ 2147483647;
-276,277d231
-< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
-< signed overflow. assert i + 1 ≤ 2147483647;
-284,286c238,239
+278,279d233
< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
+< signed overflow. assert i + 1 ≤ 2147483647;
+286,288c240,241
+< [eva:alarm] tests/value/auto_loop_unroll.c:311: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30}
-> [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-289d241
-< [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-292,294c244
-< [eva:alarm] tests/value/auto_loop_unroll.c:316: Warning:
+> [eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_30: {30}
+> [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations
+291d243
+< [eva] tests/value/auto_loop_unroll.c:319: starting to merge loop iterations
+294,296c246
+< [eva:alarm] tests/value/auto_loop_unroll.c:328: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: {32}
-307,310c257
-< [eva:alarm] tests/value/auto_loop_unroll.c:343: Warning:
+> [eva] tests/value/auto_loop_unroll.c:333: Frama_C_show_each_32: {32}
+309,312c259
+< [eva:alarm] tests/value/auto_loop_unroll.c:355: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:345:
+< [eva] tests/value/auto_loop_unroll.c:357:
< Frama_C_show_each_0_35: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:345: Frama_C_show_each_0_35: [0..35]
-313,314d259
+> [eva] tests/value/auto_loop_unroll.c:357: Frama_C_show_each_0_35: [0..35]
+315,316d261
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
-316c261,263
-< [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: [0..2147483647]
+< [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
+318c263,265
+< [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: [0..2147483647]
---
-> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+> [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: {36}
-325,327c272
-< [eva:alarm] tests/value/auto_loop_unroll.c:371: Warning:
+> [eva] tests/value/auto_loop_unroll.c:364: Frama_C_show_each_36: {36}
+327,329c274
+< [eva:alarm] tests/value/auto_loop_unroll.c:383: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: [1..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50}
-330,331d274
-< [eva:alarm] tests/value/auto_loop_unroll.c:380: Warning:
-< signed overflow. assert -2147483648 ≤ i - 1;
-339,342d281
+> [eva] tests/value/auto_loop_unroll.c:387: Frama_C_show_each_50: {50}
+332,333d276
< [eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
+< signed overflow. assert -2147483648 ≤ i - 1;
+341,344d283
+< [eva:alarm] tests/value/auto_loop_unroll.c:404: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-< [eva:alarm] tests/value/auto_loop_unroll.c:396: Warning:
+< [eva:alarm] tests/value/auto_loop_unroll.c:408: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-344c283
-< [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647]
+346c285
+< [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30}
-346,349d284
-< [eva:alarm] tests/value/auto_loop_unroll.c:403: Warning:
+> [eva] tests/value/auto_loop_unroll.c:410: Frama_C_show_each_30: {30}
+348,351d286
+< [eva:alarm] tests/value/auto_loop_unroll.c:415: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-< [eva:alarm] tests/value/auto_loop_unroll.c:407: Warning:
+< [eva:alarm] tests/value/auto_loop_unroll.c:419: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-351c286
-< [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647]
+353c288
+< [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45]
+> [eva] tests/value/auto_loop_unroll.c:424: Frama_C_show_each_30: [15..45]
diff --git a/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle b/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle
index 69c5d75fdc9b168fb5e84a39b225b0e6a9ac2f9f..59ea5970bd9b665e9f627703a65474a83aeff80a 100644
--- a/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle
@@ -12,20 +12,20 @@
< Frama_C_show_each_imprecise: [0..2147483647]
---
> [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
-335,338c329
-< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+337,340c331
+< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:194:
+< [eva] tests/value/auto_loop_unroll.c:206:
< Frama_C_show_each_imprecise: [0..2147483647]
---
-> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [1..9]
-340,341d330
-< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+> [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_imprecise: [1..9]
+342,343d332
+< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
< signed overflow. assert res + 1 ≤ 2147483647;
-345c334
+347c336
< Frama_C_show_each_imprecise: [0..2147483647]
---
> Frama_C_show_each_imprecise: [64..2147483647]
-381,382d369
-< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
+383,384d371
+< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
< signed overflow. assert i + 1 ≤ 2147483647;
diff --git a/tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle b/tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle
index 88c7352194e032c8c77c2feede550015b0d8113a..04f9ac7adc919a19e2bc43d4dd89b823377227e3 100644
--- a/tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle
+++ b/tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle
@@ -1,23 +1,23 @@
-220,221d219
-< [eva:alarm] tests/value/auto_loop_unroll.c:222: Warning:
+222,223d221
+< [eva:alarm] tests/value/auto_loop_unroll.c:234: Warning:
< signed overflow. assert -2147483648 ≤ i_0 - 1;
-227,228d224
-< [eva:alarm] tests/value/auto_loop_unroll.c:227: Warning:
+229,230d226
+< [eva:alarm] tests/value/auto_loop_unroll.c:239: Warning:
< signed overflow. assert -2147483648 ≤ i_1 - 1;
-258,259d253
-< [eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
+260,261d255
+< [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning:
< signed overflow. assert -2147483648 ≤ i - 1;
-314,315d307
-< [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+316,317d309
+< [eva:alarm] tests/value/auto_loop_unroll.c:360: Warning:
< signed overflow. assert -2147483648 ≤ i - 1;
-330,331d321
-< [eva:alarm] tests/value/auto_loop_unroll.c:380: Warning:
+332,333d323
+< [eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
< signed overflow. assert -2147483648 ≤ i - 1;
-384c374
+386c376
< i ∈ [-2147483648..50]
---
> i ∈ [-1..50]
-389,391c379,381
+391,393c381,383
< i ∈ [0..2147483647]
< j ∈ [23..2147483647]
< k ∈ [22..2147483647]
diff --git a/tests/value/oracle_octagons/auto_loop_unroll.1.res.oracle b/tests/value/oracle_octagons/auto_loop_unroll.1.res.oracle
index a4f29dd3292a4588e4f0cd036a44807e4997ff3b..43d97821cb3587d8876d9f2ed32b3ea55cdaca44 100644
--- a/tests/value/oracle_octagons/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle_octagons/auto_loop_unroll.1.res.oracle
@@ -1,4 +1,4 @@
-472,473c472,473
+474,475c474,475
< i ∈ [0..2147483647]
< j ∈ [23..2147483647]
---