(0) Obligation:
Need to prove time_complexity of the following program:
public class Test2 {
public static void main(String[] args) {
iter(args.length, args.length % 5, args.length % 4);
}
private static void iter(int x, int y, int z) {
while (x + y + 3 * z >= 0) {
if (x > y)
x--;
else if (y > z) {
x++;
y -= 2;
}
else if (y <= z) {
x = add(x, 1);
y = add(y, 1);
z = z - 1;
}
}
}
private static int add(int v, int w) {
return v + w;
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
Test2.main([Ljava/lang/String;)V: Graph of 101 nodes with 1 SCC.
(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)
Extracted set of 100 edges for the analysis of TIME complexity. Kept leaves.
(4) Obligation:
Set of 100 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: nonterm paths and paths from start to sinks
(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 100 jbc graph edges to a weighted ITS with 100 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.
(6) Obligation:
IntTrs with 100 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: 0 <= i6 && iconst_5 = 5 && i6 < iconst_5 && 0 <= i4 && i6 <= 4 && 0 < a6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && i8 < iconst_4 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_1(
o1,
env,
static) -{26,26}>
iter_Load_1320(
i4',
i6',
i8',
o1,
i4',
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
i4' &&
0 <=
2 &&
-2 <=
i8' &&
-1 <=
i8' &&
0 <
o1 &&
i8' <=
3 &&
static''' <=
static +
2 &&
i6' <=
4 &&
0 <=
static &&
i6' <
5 &&
-1 <=
i6' &&
0 <=
static''' &&
i8' <
4 &&
0 <=
i6' &&
0 <
2 &&
-1 <=
i4' &&
0 <=
1 &&
-2 <=
i6' &&
0 <
1 &&
0 <=
i8' &&
0 <=
static'1 &&
i4' <
o1by chaining
main_Load_1(
o1,
env,
static) -{0,0}>
main_Load_3(
o1,
env,
static) :|:
0 <
o1main_Load_3(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_5(
o1,
env,
static) :|:
0 <
o1langle_clinit_rangle_ConstantStackPush_5(
o1,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_9(
iconst_0,
o1,
env,
static) :|:
iconst_0 =
0 &&
0 <
o1langle_clinit_rangle_ArrayCreate_9(
iconst_0,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_10(
a2,
o1,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2 &&
0 <
o1langle_clinit_rangle_FieldAccess_10(
a2,
o1,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_13(
o1,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2 &&
0 <
o1langle_clinit_rangle_New_13(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_New_15(
o1,
env,
static) :|:
0 <
o1langle_clinit_rangle_New_15(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_New_16(
o1,
env,
static) :|:
0 <=
static &&
0 <
o1langle_clinit_rangle_New_16(
o1,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_18(
o4,
o1,
env,
static) :|:
o4 =
1 &&
0 <
o4 &&
0 <
o1langle_clinit_rangle_Duplicate_18(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_20(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_clinit_rangle_ConstantStackPush_20(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_22(
o4,
NULL,
o1,
env,
static) :|:
NULL =
0 &&
0 <
o4 &&
0 <
o1langle_clinit_rangle_InvokeMethod_22(
o4,
NULL,
o1,
env,
static) -{1,1}>
langle_init_rangle_Load_24(
o4,
o1,
env,
static) :|:
NULL =
0 &&
0 <
o4 &&
0 <
o1langle_init_rangle_Load_24(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_25(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_InvokeMethod_25(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Load_27(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_30(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_InvokeMethod_30(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Return_32(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Return_32(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Return_35(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_37(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_clinit_rangle_FieldAccess_37(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
o1,
env,
static') :|:
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
0 <
o1 &&
static' <=
static +
o4langle_clinit_rangle_Return_40(
o1,
env,
static) -{1,1}>
main_Load_41(
o1,
env,
static) :|:
0 <
o1main_Load_41(
o1,
env,
static) -{0,0}>
main_Load_42(
o1,
env,
static) :|:
0 <
o1main_Load_42(
o1,
env,
static) -{0,0}>
main_Load_43(
o1,
env,
static) :|:
0 <=
static &&
0 <
o1main_Load_43(
o1,
env,
static) -{0,0}>
main_Load_45(
o1,
env,
static) :|:
0 <
o1main_Load_45(
o1,
env,
static) -{0,0}>
main_Load_47(
o1,
env,
static) :|:
0 <
o1main_Load_47(
o1,
env,
static) -{1,1}>
main_ArrayLength_51(
o1,
env,
static) :|:
0 <
o1main_ArrayLength_51(
a6,
env,
static) -{0,0}>
main_ArrayLength_52(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6 &&
i4 <
a6main_ArrayLength_52(
a6,
i4,
env,
static) -{1,1}>
main_Load_54(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_Load_54(
a6,
i4,
env,
static) -{1,1}>
main_ArrayLength_56(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_ArrayLength_56(
a6,
i4,
env,
static) -{1,1}>
main_ConstantStackPush_58(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_ConstantStackPush_58(
a6,
i4,
env,
static) -{1,1}>
main_IntArithmetic_60(
a6,
i4,
iconst_5,
env,
static) :|:
iconst_5 =
5 &&
0 <=
i4 &&
0 <
a6main_IntArithmetic_60(
a6,
i4,
iconst_5,
env,
static) -{1,1}>
main_Load_62(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
iconst_5 =
5 &&
i6 <
iconst_5 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_Load_62(
a6,
i4,
i6,
env,
static) -{1,1}>
main_ArrayLength_64(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_ArrayLength_64(
a6,
i4,
i6,
env,
static) -{1,1}>
main_ConstantStackPush_66(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_ConstantStackPush_66(
a6,
i4,
i6,
env,
static) -{1,1}>
main_IntArithmetic_68(
a6,
i4,
i6,
iconst_4,
env,
static) :|:
0 <=
i6 &&
iconst_4 =
4 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_IntArithmetic_68(
a6,
i4,
i6,
iconst_4,
env,
static) -{1,1}>
main_InvokeMethod_70(
a6,
i4,
i6,
i8,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
i8 <
iconst_4 &&
iconst_4 =
4 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8main_InvokeMethod_70(
a6,
i4,
i6,
i8,
env,
static) -{1,1}>
iter_Load_72(
i4,
i6,
i8,
a6,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8iter_Load_72(
i4,
i6,
i8,
a6,
env,
static) -{0,0}>
iter_Load_577(
i4,
i6,
i8,
a6,
i4,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
-1 <=
i6 &&
0 <=
i4 &&
-1 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8iter_Load_577(
i249,
i250,
i8,
a110,
i69,
env,
static) -{0,0}>
iter_Load_710(
i249,
i250,
i8,
a110,
i69,
env,
static) :|:
i8 <=
3 &&
0 <
a110 &&
-1 <=
i250 &&
-1 <=
i249 &&
-1 <=
i8 &&
0 <=
i8 &&
0 <=
i69iter_Load_710(
i301,
i302,
i303,
a131,
i69,
env,
static) -{0,0}>
iter_Load_762(
i301,
i302,
i303,
a131,
i69,
env,
static) :|:
i303 <=
3 &&
-1 <=
i302 &&
-2 <=
i302 &&
0 <=
i69 &&
-1 <=
i303 &&
-1 <=
i301 &&
0 <
a131iter_Load_762(
i326,
i327,
i303,
a139,
i69,
env,
static) -{0,0}>
iter_Load_796(
i326,
i327,
i303,
a139,
i69,
env,
static) :|:
-1 <=
i326 &&
i303 <=
3 &&
0 <=
i69 &&
-1 <=
i303 &&
-2 <=
i327 &&
0 <
a139iter_Load_796(
i342,
i327,
i303,
a145,
i69,
env,
static) -{0,0}>
iter_Load_899(
i342,
i327,
i303,
a145,
i69,
env,
static) :|:
i303 <=
3 &&
-2 <=
i303 &&
0 <
a145 &&
0 <=
i69 &&
-1 <=
i303 &&
-2 <=
i327iter_Load_899(
i380,
i381,
i382,
a164,
i69,
env,
static) -{0,0}>
iter_Load_1043(
i380,
i381,
i382,
a164,
i69,
env,
static) :|:
-2 <=
i381 &&
i382 <=
3 &&
0 <
a164 &&
-2 <=
i382 &&
0 <=
i69iter_Load_1043(
i426,
i427,
i382,
a176,
i69,
env,
static) -{0,0}>
iter_Load_1320(
i426,
i427,
i382,
a176,
i69,
env,
static) :|:
0 <
a176 &&
i382 <=
3 &&
-2 <=
i382 &&
0 <=
i69obtained
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
by chaining
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
obtained
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
by chaining
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
obtained
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
by chaining
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
(8) Obligation:
IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
(9) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
was transformed to
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
was transformed to
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
(10) Obligation:
IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
(11) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69, env, static) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
(12) Obligation:
IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69, env, static) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
(13) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 100 jbc graph edges to a weighted ITS with 100 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.
(14) Obligation:
IntTrs with 100 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: iconst_5 = 5 && 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6 && i4 % iconst_5 = i6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && iconst_4 = 4 && i4 % iconst_4 = i8 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
(15) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_1(
o1,
env,
static) -{26,26}>
iter_Load_1320(
i4',
i6',
i8',
o1,
i4',
env,
static'1) :|:
i4' %
5 =
i6' &&
0 <=
i4' &&
static'1 <=
static''' +
1 &&
-2 <=
i8' &&
-1 <=
i8' &&
0 <
o1 &&
i8' <=
3 &&
0 <=
2 &&
i6' <=
4 &&
static''' <=
static +
2 &&
0 <=
static &&
-1 <=
i6' &&
i4' %
4 =
i8' &&
0 <=
static''' &&
0 <=
i6' &&
0 <
2 &&
-1 <=
i4' &&
0 <=
1 &&
-2 <=
i6' &&
0 <
1 &&
0 <=
i8' &&
0 <=
static'1 &&
i4' <
o1by chaining
main_Load_1(
o1,
env,
static) -{0,0}>
main_Load_3(
o1,
env,
static) :|:
0 <
o1main_Load_3(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_5(
o1,
env,
static) :|:
0 <
o1langle_clinit_rangle_ConstantStackPush_5(
o1,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_9(
iconst_0,
o1,
env,
static) :|:
iconst_0 =
0 &&
0 <
o1langle_clinit_rangle_ArrayCreate_9(
iconst_0,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_10(
a2,
o1,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2 &&
0 <
o1langle_clinit_rangle_FieldAccess_10(
a2,
o1,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_13(
o1,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2 &&
0 <
o1langle_clinit_rangle_New_13(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_New_15(
o1,
env,
static) :|:
0 <
o1langle_clinit_rangle_New_15(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_New_16(
o1,
env,
static) :|:
0 <=
static &&
0 <
o1langle_clinit_rangle_New_16(
o1,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_18(
o4,
o1,
env,
static) :|:
o4 =
1 &&
0 <
o4 &&
0 <
o1langle_clinit_rangle_Duplicate_18(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_20(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_clinit_rangle_ConstantStackPush_20(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_22(
o4,
NULL,
o1,
env,
static) :|:
NULL =
0 &&
0 <
o4 &&
0 <
o1langle_clinit_rangle_InvokeMethod_22(
o4,
NULL,
o1,
env,
static) -{1,1}>
langle_init_rangle_Load_24(
o4,
o1,
env,
static) :|:
NULL =
0 &&
0 <
o4 &&
0 <
o1langle_init_rangle_Load_24(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_25(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_InvokeMethod_25(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Load_27(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_30(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_InvokeMethod_30(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Return_32(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Return_32(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Return_35(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_37(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_clinit_rangle_FieldAccess_37(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
o1,
env,
static') :|:
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
0 <
o1 &&
static' <=
static +
o4langle_clinit_rangle_Return_40(
o1,
env,
static) -{1,1}>
main_Load_41(
o1,
env,
static) :|:
0 <
o1main_Load_41(
o1,
env,
static) -{0,0}>
main_Load_42(
o1,
env,
static) :|:
0 <
o1main_Load_42(
o1,
env,
static) -{0,0}>
main_Load_43(
o1,
env,
static) :|:
0 <=
static &&
0 <
o1main_Load_43(
o1,
env,
static) -{0,0}>
main_Load_45(
o1,
env,
static) :|:
0 <
o1main_Load_45(
o1,
env,
static) -{0,0}>
main_Load_47(
o1,
env,
static) :|:
0 <
o1main_Load_47(
o1,
env,
static) -{1,1}>
main_ArrayLength_51(
o1,
env,
static) :|:
0 <
o1main_ArrayLength_51(
a6,
env,
static) -{0,0}>
main_ArrayLength_52(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6 &&
i4 <
a6main_ArrayLength_52(
a6,
i4,
env,
static) -{1,1}>
main_Load_54(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_Load_54(
a6,
i4,
env,
static) -{1,1}>
main_ArrayLength_56(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_ArrayLength_56(
a6,
i4,
env,
static) -{1,1}>
main_ConstantStackPush_58(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_ConstantStackPush_58(
a6,
i4,
env,
static) -{1,1}>
main_IntArithmetic_60(
a6,
i4,
iconst_5,
env,
static) :|:
iconst_5 =
5 &&
0 <=
i4 &&
0 <
a6main_IntArithmetic_60(
a6,
i4,
iconst_5,
env,
static) -{1,1}>
main_Load_62(
a6,
i4,
i6,
env,
static) :|:
iconst_5 =
5 &&
0 <=
i6 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
i4 %
iconst_5 =
i6main_Load_62(
a6,
i4,
i6,
env,
static) -{1,1}>
main_ArrayLength_64(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_ArrayLength_64(
a6,
i4,
i6,
env,
static) -{1,1}>
main_ConstantStackPush_66(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_ConstantStackPush_66(
a6,
i4,
i6,
env,
static) -{1,1}>
main_IntArithmetic_68(
a6,
i4,
i6,
iconst_4,
env,
static) :|:
0 <=
i6 &&
iconst_4 =
4 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_IntArithmetic_68(
a6,
i4,
i6,
iconst_4,
env,
static) -{1,1}>
main_InvokeMethod_70(
a6,
i4,
i6,
i8,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
iconst_4 =
4 &&
i4 %
iconst_4 =
i8 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8main_InvokeMethod_70(
a6,
i4,
i6,
i8,
env,
static) -{1,1}>
iter_Load_72(
i4,
i6,
i8,
a6,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8iter_Load_72(
i4,
i6,
i8,
a6,
env,
static) -{0,0}>
iter_Load_577(
i4,
i6,
i8,
a6,
i4,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
-1 <=
i6 &&
0 <=
i4 &&
-1 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8iter_Load_577(
i249,
i250,
i8,
a110,
i69,
env,
static) -{0,0}>
iter_Load_710(
i249,
i250,
i8,
a110,
i69,
env,
static) :|:
i8 <=
3 &&
0 <
a110 &&
-1 <=
i250 &&
-1 <=
i249 &&
-1 <=
i8 &&
0 <=
i8 &&
0 <=
i69iter_Load_710(
i301,
i302,
i303,
a131,
i69,
env,
static) -{0,0}>
iter_Load_762(
i301,
i302,
i303,
a131,
i69,
env,
static) :|:
i303 <=
3 &&
-1 <=
i302 &&
-2 <=
i302 &&
0 <=
i69 &&
-1 <=
i303 &&
-1 <=
i301 &&
0 <
a131iter_Load_762(
i326,
i327,
i303,
a139,
i69,
env,
static) -{0,0}>
iter_Load_796(
i326,
i327,
i303,
a139,
i69,
env,
static) :|:
-1 <=
i326 &&
i303 <=
3 &&
0 <=
i69 &&
-1 <=
i303 &&
-2 <=
i327 &&
0 <
a139iter_Load_796(
i342,
i327,
i303,
a145,
i69,
env,
static) -{0,0}>
iter_Load_899(
i342,
i327,
i303,
a145,
i69,
env,
static) :|:
i303 <=
3 &&
-2 <=
i303 &&
0 <
a145 &&
0 <=
i69 &&
-1 <=
i303 &&
-2 <=
i327iter_Load_899(
i380,
i381,
i382,
a164,
i69,
env,
static) -{0,0}>
iter_Load_1043(
i380,
i381,
i382,
a164,
i69,
env,
static) :|:
-2 <=
i381 &&
i382 <=
3 &&
0 <
a164 &&
-2 <=
i382 &&
0 <=
i69iter_Load_1043(
i426,
i427,
i382,
a176,
i69,
env,
static) -{0,0}>
iter_Load_1320(
i426,
i427,
i382,
a176,
i69,
env,
static) :|:
0 <
a176 &&
i382 <=
3 &&
-2 <=
i382 &&
0 <=
i69obtained
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
by chaining
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
obtained
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
by chaining
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
obtained
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
by chaining
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
(16) Obligation:
IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' % 5 = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' % 4 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
(17) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)
Removed div and mod.
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' % 5 = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' % 4 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
(18) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
(19) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
was transformed to
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
was transformed to
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' - 5 * div, i4' - 4 * div1, o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
(20) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' - 5 * div, i4' - 4 * div1, o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
(21) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' - 5 * div, i4' - 4 * div1, o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' + -5 * div, i4' + -4 * div1, o1, i4', env, static'1) :|: i4' + -4 * div1 < 4 && 0 < i4' + -4 * div1 + 4 && i4' + -5 * div < 5 && 0 < i4' + -5 * div + 5 && i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69, env, static) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
(22) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69, env, static) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' + -5 * div, i4' + -4 * div1, o1, i4', env, static'1) :|: i4' + -4 * div1 < 4 && 0 < i4' + -4 * div1 + 4 && i4' + -5 * div < 5 && 0 < i4' + -5 * div + 5 && i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)
Extracted set of 99 edges for the analysis of TIME complexity. Dropped leaves.
(24) Obligation:
Set of 99 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: all paths from start
(25) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 99 jbc graph edges to a weighted ITS with 99 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.
(26) Obligation:
IntTrs with 99 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: 0 <= i6 && iconst_5 = 5 && i6 < iconst_5 && 0 <= i4 && i6 <= 4 && 0 < a6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && i8 < iconst_4 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
(27) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_1(
o1,
env,
static) -{26,26}>
iter_Load_1320(
i4',
i6',
i8',
o1,
i4',
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
i4' &&
0 <=
2 &&
-2 <=
i8' &&
-1 <=
i8' &&
0 <
o1 &&
i8' <=
3 &&
static''' <=
static +
2 &&
i6' <=
4 &&
0 <=
static &&
i6' <
5 &&
-1 <=
i6' &&
0 <=
static''' &&
i8' <
4 &&
0 <=
i6' &&
0 <
2 &&
-1 <=
i4' &&
0 <=
1 &&
-2 <=
i6' &&
0 <
1 &&
0 <=
i8' &&
0 <=
static'1 &&
i4' <
o1by chaining
main_Load_1(
o1,
env,
static) -{0,0}>
main_Load_3(
o1,
env,
static) :|:
0 <
o1main_Load_3(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_5(
o1,
env,
static) :|:
0 <
o1langle_clinit_rangle_ConstantStackPush_5(
o1,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_9(
iconst_0,
o1,
env,
static) :|:
iconst_0 =
0 &&
0 <
o1langle_clinit_rangle_ArrayCreate_9(
iconst_0,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_10(
a2,
o1,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2 &&
0 <
o1langle_clinit_rangle_FieldAccess_10(
a2,
o1,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_13(
o1,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2 &&
0 <
o1langle_clinit_rangle_New_13(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_New_15(
o1,
env,
static) :|:
0 <
o1langle_clinit_rangle_New_15(
o1,
env,
static) -{0,0}>
langle_clinit_rangle_New_16(
o1,
env,
static) :|:
0 <=
static &&
0 <
o1langle_clinit_rangle_New_16(
o1,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_18(
o4,
o1,
env,
static) :|:
o4 =
1 &&
0 <
o4 &&
0 <
o1langle_clinit_rangle_Duplicate_18(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_20(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_clinit_rangle_ConstantStackPush_20(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_22(
o4,
NULL,
o1,
env,
static) :|:
NULL =
0 &&
0 <
o4 &&
0 <
o1langle_clinit_rangle_InvokeMethod_22(
o4,
NULL,
o1,
env,
static) -{1,1}>
langle_init_rangle_Load_24(
o4,
o1,
env,
static) :|:
NULL =
0 &&
0 <
o4 &&
0 <
o1langle_init_rangle_Load_24(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_25(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_InvokeMethod_25(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Load_27(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_30(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_InvokeMethod_30(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Return_32(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Return_32(
o4,
o1,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_init_rangle_Return_35(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_37(
o4,
o1,
env,
static) :|:
0 <
o4 &&
0 <
o1langle_clinit_rangle_FieldAccess_37(
o4,
o1,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
o1,
env,
static') :|:
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
0 <
o1 &&
static' <=
static +
o4langle_clinit_rangle_Return_40(
o1,
env,
static) -{1,1}>
main_Load_41(
o1,
env,
static) :|:
0 <
o1main_Load_41(
o1,
env,
static) -{0,0}>
main_Load_42(
o1,
env,
static) :|:
0 <
o1main_Load_42(
o1,
env,
static) -{0,0}>
main_Load_43(
o1,
env,
static) :|:
0 <=
static &&
0 <
o1main_Load_43(
o1,
env,
static) -{0,0}>
main_Load_45(
o1,
env,
static) :|:
0 <
o1main_Load_45(
o1,
env,
static) -{0,0}>
main_Load_47(
o1,
env,
static) :|:
0 <
o1main_Load_47(
o1,
env,
static) -{1,1}>
main_ArrayLength_51(
o1,
env,
static) :|:
0 <
o1main_ArrayLength_51(
a6,
env,
static) -{0,0}>
main_ArrayLength_52(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6 &&
i4 <
a6main_ArrayLength_52(
a6,
i4,
env,
static) -{1,1}>
main_Load_54(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_Load_54(
a6,
i4,
env,
static) -{1,1}>
main_ArrayLength_56(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_ArrayLength_56(
a6,
i4,
env,
static) -{1,1}>
main_ConstantStackPush_58(
a6,
i4,
env,
static) :|:
0 <=
i4 &&
0 <
a6main_ConstantStackPush_58(
a6,
i4,
env,
static) -{1,1}>
main_IntArithmetic_60(
a6,
i4,
iconst_5,
env,
static) :|:
iconst_5 =
5 &&
0 <=
i4 &&
0 <
a6main_IntArithmetic_60(
a6,
i4,
iconst_5,
env,
static) -{1,1}>
main_Load_62(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
iconst_5 =
5 &&
i6 <
iconst_5 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_Load_62(
a6,
i4,
i6,
env,
static) -{1,1}>
main_ArrayLength_64(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_ArrayLength_64(
a6,
i4,
i6,
env,
static) -{1,1}>
main_ConstantStackPush_66(
a6,
i4,
i6,
env,
static) :|:
0 <=
i6 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_ConstantStackPush_66(
a6,
i4,
i6,
env,
static) -{1,1}>
main_IntArithmetic_68(
a6,
i4,
i6,
iconst_4,
env,
static) :|:
0 <=
i6 &&
iconst_4 =
4 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6main_IntArithmetic_68(
a6,
i4,
i6,
iconst_4,
env,
static) -{1,1}>
main_InvokeMethod_70(
a6,
i4,
i6,
i8,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
i8 <
iconst_4 &&
iconst_4 =
4 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8main_InvokeMethod_70(
a6,
i4,
i6,
i8,
env,
static) -{1,1}>
iter_Load_72(
i4,
i6,
i8,
a6,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
0 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8iter_Load_72(
i4,
i6,
i8,
a6,
env,
static) -{0,0}>
iter_Load_577(
i4,
i6,
i8,
a6,
i4,
env,
static) :|:
0 <=
i6 &&
i8 <=
3 &&
-1 <=
i6 &&
0 <=
i4 &&
-1 <=
i4 &&
i6 <=
4 &&
0 <
a6 &&
0 <=
i8iter_Load_577(
i249,
i250,
i8,
a110,
i69,
env,
static) -{0,0}>
iter_Load_710(
i249,
i250,
i8,
a110,
i69,
env,
static) :|:
i8 <=
3 &&
0 <
a110 &&
-1 <=
i250 &&
-1 <=
i249 &&
-1 <=
i8 &&
0 <=
i8 &&
0 <=
i69iter_Load_710(
i301,
i302,
i303,
a131,
i69,
env,
static) -{0,0}>
iter_Load_762(
i301,
i302,
i303,
a131,
i69,
env,
static) :|:
i303 <=
3 &&
-1 <=
i302 &&
-2 <=
i302 &&
0 <=
i69 &&
-1 <=
i303 &&
-1 <=
i301 &&
0 <
a131iter_Load_762(
i326,
i327,
i303,
a139,
i69,
env,
static) -{0,0}>
iter_Load_796(
i326,
i327,
i303,
a139,
i69,
env,
static) :|:
-1 <=
i326 &&
i303 <=
3 &&
0 <=
i69 &&
-1 <=
i303 &&
-2 <=
i327 &&
0 <
a139iter_Load_796(
i342,
i327,
i303,
a145,
i69,
env,
static) -{0,0}>
iter_Load_899(
i342,
i327,
i303,
a145,
i69,
env,
static) :|:
i303 <=
3 &&
-2 <=
i303 &&
0 <
a145 &&
0 <=
i69 &&
-1 <=
i303 &&
-2 <=
i327iter_Load_899(
i380,
i381,
i382,
a164,
i69,
env,
static) -{0,0}>
iter_Load_1043(
i380,
i381,
i382,
a164,
i69,
env,
static) :|:
-2 <=
i381 &&
i382 <=
3 &&
0 <
a164 &&
-2 <=
i382 &&
0 <=
i69iter_Load_1043(
i426,
i427,
i382,
a176,
i69,
env,
static) -{0,0}>
iter_Load_1320(
i426,
i427,
i382,
a176,
i69,
env,
static) :|:
0 <
a176 &&
i382 <=
3 &&
-2 <=
i382 &&
0 <=
i69obtained
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
by chaining
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
obtained
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
by chaining
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
(28) Obligation:
IntTrs with 7 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
(29) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)
Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:
main_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
iter_Load_1320(x1, x2, x3, x4, x5, x6, x7) → iter_Load_1320(x1, x2, x3, x4, x5)
iter_ConstantStackPush_1327(x1, x2, x3, x4, x5, x6, x7, x8) → iter_ConstantStackPush_1327(x1, x2, x3, x4, x5, x6)
iter_LE_1349(x1, x2, x3, x4, x5, x6, x7) → iter_LE_1349(x1, x2, x3, x4, x5)
iter_LE_1378(x1, x2, x3, x4, x5, x6, x7) → iter_LE_1378(x1, x2, x3, x4, x5)
(30) Obligation:
IntTrs with 7 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
(31) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
was transformed to
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
(32) Obligation:
IntTrs with 7 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69) :|: i522 <= i523 && 0 <= i69 && 0 < a208
(33) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
(34) Obligation:
IntTrs with 7 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1349(i522, i523, i524, a208, i69) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
(35) koat Proof (EQUIVALENT transformation)
YES(?, 561*ar_0 + 39350)
Initial complexity problem:
1: T:
(Comp: ?, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: ?, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: ?, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: ?, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: ?, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Applied AI with 'oct' on problem 2 to obtain the following invariants:
For symbol iter_ConstantStackPush_1327: X_5 - X_6 - 1 >= 0 /\ X_6 >= 0 /\ X_5 + X_6 - 1 >= 0 /\ -X_4 + X_6 + 3 >= 0 /\ -X_3 + X_6 + 4 >= 0 /\ X_5 - 1 >= 0 /\ -X_4 + X_5 + 2 >= 0 /\ -X_3 + X_5 + 3 >= 0 /\ -X_4 + 3 >= 0 /\ X_3 - X_4 + 3 >= 0 /\ -X_3 - X_4 + 7 >= 0 /\ -X_3 + X_4 + 4 >= 0 /\ -X_3 + 4 >= 0 /\ -X_1 + X_2 + 4 >= 0
For symbol iter_LE_1349: X_4 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ -X_3 + X_5 + 3 >= 0 /\ -X_2 + X_5 + 4 >= 0 /\ X_1 + X_5 + 13 >= 0 /\ X_4 - 1 >= 0 /\ -X_3 + X_4 + 2 >= 0 /\ -X_2 + X_4 + 3 >= 0 /\ X_1 + X_4 + 12 >= 0 /\ -X_3 + 3 >= 0 /\ X_2 - X_3 + 3 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ X_1 - X_3 + 16 >= 0 /\ -X_2 + X_3 + 4 >= 0 /\ X_1 + X_3 + 10 >= 0 /\ -X_2 + 4 >= 0 /\ X_1 - X_2 + 17 >= 0 /\ X_1 + X_2 + 13 >= 0 /\ X_1 + 13 >= 0
For symbol iter_LE_1378: X_4 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ X_3 + X_5 + 13 >= 0 /\ -X_3 + X_5 + 4 >= 0 /\ X_2 + X_5 + 7 >= 0 /\ -X_2 + X_5 + 3 >= 0 /\ X_1 + X_5 + 6 >= 0 /\ -X_1 + X_5 + 4 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 + 12 >= 0 /\ -X_3 + X_4 + 3 >= 0 /\ X_2 + X_4 + 6 >= 0 /\ -X_2 + X_4 + 2 >= 0 /\ X_1 + X_4 + 5 >= 0 /\ -X_1 + X_4 + 3 >= 0 /\ -X_3 + 4 >= 0 /\ X_2 - X_3 + 4 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ X_1 - X_3 >= 0 /\ -X_1 - X_3 + 8 >= 0 /\ X_3 + 13 >= 0 /\ X_2 + X_3 + 10 >= 0 /\ -X_2 + X_3 + 16 >= 0 /\ X_1 + X_3 + 13 >= 0 /\ -X_1 + X_3 + 17 >= 0 /\ -X_2 + 3 >= 0 /\ X_1 - X_2 + 3 >= 0 /\ -X_1 - X_2 + 7 >= 0 /\ X_2 + 7 >= 0 /\ X_1 + X_2 + 10 >= 0 /\ -X_1 + X_2 + 4 >= 0 /\ -X_1 + 4 >= 0 /\ X_1 + 6 >= 0
For symbol iter_Load_1320: X_4 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ -X_3 + X_5 + 3 >= 0 /\ -X_2 + X_5 + 4 >= 0 /\ X_4 - 1 >= 0 /\ -X_3 + X_4 + 2 >= 0 /\ -X_2 + X_4 + 3 >= 0 /\ -X_3 + 3 >= 0 /\ X_2 - X_3 + 3 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ -X_2 + X_3 + 4 >= 0 /\ -X_2 + 4 >= 0
This yielded the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: ?, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: ?, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ -ar_1 + 4 >= 0 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: ?, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
start location: koat_start
leaf cost: 0
A polynomial rank function with
Pol(koat_start) = 11*V_1 + 771
Pol(main_Load_1) = 11*V_1 + 771
Pol(iter_LE_1378) = 8*V_1 + 25*V_2 + 11*V_3 + 671
Pol(iter_Load_1320) = 11*V_1 + 8*V_2 + 25*V_3 + 675
Pol(iter_LE_1349) = 11*V_1 + 8*V_2 + 25*V_3 + 673
Pol(iter_ConstantStackPush_1327) = 11*V_2 + 8*V_3 + 25*V_4 + 675
orients all transitions weakly and the transitions
iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: 11*ar_0 + 771, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 11*ar_0 + 771, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: 11*ar_0 + 771, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ -ar_1 + 4 >= 0 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: 11*ar_0 + 771, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
start location: koat_start
leaf cost: 0
Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: 11*ar_0 + 771, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 11*ar_0 + 771, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: 11*ar_0 + 771, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: 11*ar_0 + 771, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: 22*ar_0 + 1543, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ -ar_1 + 4 >= 0 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: 11*ar_0 + 771, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
start location: koat_start
leaf cost: 0
Complexity upper bound 561*ar_0 + 39350
Time: 1.140 sec (SMT: 0.961 sec)
(36) BOUNDS(CONSTANT, 39350 + 561 * |#0|)