(0) Obligation:
Need to prove time_complexity of the following program:
public class AG313 {
public static void main(String[] args) {
int x, y;
x = args[0].length();
y = args[1].length() + 1;
quot(x,y);
}
public static int quot(int x, int y) {
int i = 0;
if(x==0) return 0;
while (x > 0 && y > 0) {
i += 1;
x = (x - 1)- (y - 1);
}
return i;
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
AG313.main([Ljava/lang/String;)V: Graph of 171 nodes with 1 SCC.
(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(94)) transformation)
Extracted set of 73 edges for the analysis of TIME complexity. Kept leaves.
(4) Obligation:
Set of 73 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 73 jbc graph edges to a weighted ITS with 73 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 73 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114
(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_2(
o2,
env,
static) -{17,17}>
main_ArrayAccess_57(
o2,
0,
i5',
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
i5' &&
0 <=
2 &&
0 <
o2 &&
static''' <=
static +
2 &&
i5' <
o2 &&
0 <=
static''' &&
0 <=
static &&
0 <
1 &&
0 <=
1 &&
0 <=
static'1 &&
0 <
2by chaining
main_Load_2(
o2,
env,
static) -{0,0}>
main_Load_4(
o2,
env,
static) :|:
0 <
o2main_Load_4(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_6(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_13(
iconst_0,
o2,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0langle_clinit_rangle_ArrayCreate_13(
iconst_0,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_19(
a2,
o2,
iconst_0,
env,
static) :|:
a2 =
2 &&
0 <
o2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_19(
a2,
o2,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_21(
o2,
env,
static') :|:
0 <=
a2 &&
0 <
o2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_21(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_23(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_New_23(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_24(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticlangle_clinit_rangle_New_24(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_26(
o4,
o2,
env,
static) :|:
o4 =
1 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_Duplicate_26(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_29(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_ConstantStackPush_29(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_32(
o4,
NULL,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_InvokeMethod_32(
o4,
NULL,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_33(
o4,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_init_rangle_Load_33(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_35(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_35(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_37(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Load_37(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_40(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_40(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_42(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_42(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_43(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_43(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_44(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_FieldAccess_44(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Return_45(
o2,
env,
static') :|:
0 <
o2 &&
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
static' <=
static +
o4langle_clinit_rangle_Return_45(
o2,
env,
static) -{1,1}>
main_Load_47(
o2,
env,
static) :|:
0 <
o2main_Load_47(
o2,
env,
static) -{0,0}>
main_Load_48(
o2,
env,
static) :|:
0 <
o2main_Load_48(
o2,
env,
static) -{0,0}>
main_Load_49(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticmain_Load_49(
o2,
env,
static) -{0,0}>
main_Load_50(
o2,
env,
static) :|:
0 <
o2main_Load_50(
o2,
env,
static) -{0,0}>
main_Load_53(
o2,
env,
static) :|:
0 <
o2main_Load_53(
o2,
env,
static) -{1,1}>
main_ConstantStackPush_54(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_54(
o2,
env,
static) -{1,1}>
main_ArrayAccess_56(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_ArrayAccess_56(
a6,
iconst_0,
env,
static) -{0,0}>
main_ArrayAccess_57(
a6,
iconst_0,
i5,
env,
static) :|:
i5 <
a6 &&
iconst_0 =
0 &&
0 <
a6 &&
0 <=
i5obtained
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
by chaining
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
obtained
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
by chaining
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
obtained
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
by chaining
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
obtained
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
by chaining
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
obtained
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
by chaining
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
obtained
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
by chaining
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114
(8) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from lhss to constraints.
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
(10) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
(11) LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Linearized lhss.
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
(12) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
(13) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
was transformed to
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
was transformed to
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
(14) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
(15) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
was transformed to
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
(16) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
(17) CESProof (EQUIVALENT transformation)
proved upper bound 21 + 14 * args using cofloco
(18) BOUNDS(CONSTANT, 21 + 14 * args)
(19) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 73 jbc graph edges to a weighted ITS with 73 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.
(20) Obligation:
IntTrs with 73 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114
(21) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_2(
o2,
env,
static) -{17,17}>
main_ArrayAccess_57(
o2,
0,
i5',
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
i5' &&
0 <=
2 &&
0 <
o2 &&
static''' <=
static +
2 &&
i5' <
o2 &&
0 <=
static''' &&
0 <=
static &&
0 <
1 &&
0 <=
1 &&
0 <=
static'1 &&
0 <
2by chaining
main_Load_2(
o2,
env,
static) -{0,0}>
main_Load_4(
o2,
env,
static) :|:
0 <
o2main_Load_4(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_6(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_13(
iconst_0,
o2,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0langle_clinit_rangle_ArrayCreate_13(
iconst_0,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_19(
a2,
o2,
iconst_0,
env,
static) :|:
a2 =
2 &&
0 <
o2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_19(
a2,
o2,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_21(
o2,
env,
static') :|:
0 <=
a2 &&
0 <
o2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_21(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_23(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_New_23(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_24(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticlangle_clinit_rangle_New_24(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_26(
o4,
o2,
env,
static) :|:
o4 =
1 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_Duplicate_26(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_29(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_ConstantStackPush_29(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_32(
o4,
NULL,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_InvokeMethod_32(
o4,
NULL,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_33(
o4,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_init_rangle_Load_33(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_35(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_35(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_37(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Load_37(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_40(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_40(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_42(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_42(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_43(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_43(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_44(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_FieldAccess_44(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Return_45(
o2,
env,
static') :|:
0 <
o2 &&
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
static' <=
static +
o4langle_clinit_rangle_Return_45(
o2,
env,
static) -{1,1}>
main_Load_47(
o2,
env,
static) :|:
0 <
o2main_Load_47(
o2,
env,
static) -{0,0}>
main_Load_48(
o2,
env,
static) :|:
0 <
o2main_Load_48(
o2,
env,
static) -{0,0}>
main_Load_49(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticmain_Load_49(
o2,
env,
static) -{0,0}>
main_Load_50(
o2,
env,
static) :|:
0 <
o2main_Load_50(
o2,
env,
static) -{0,0}>
main_Load_53(
o2,
env,
static) :|:
0 <
o2main_Load_53(
o2,
env,
static) -{1,1}>
main_ConstantStackPush_54(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_54(
o2,
env,
static) -{1,1}>
main_ArrayAccess_56(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_ArrayAccess_56(
a6,
iconst_0,
env,
static) -{0,0}>
main_ArrayAccess_57(
a6,
iconst_0,
i5,
env,
static) :|:
i5 <
a6 &&
iconst_0 =
0 &&
0 <
a6 &&
0 <=
i5obtained
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
by chaining
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
obtained
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
by chaining
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
obtained
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
by chaining
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
obtained
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
by chaining
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
obtained
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
by chaining
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
obtained
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
by chaining
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114
(22) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
(23) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from lhss to constraints.
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
(24) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
(25) LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Linearized lhss.
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
(26) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
(27) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
was transformed to
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
was transformed to
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
(28) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
(29) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
was transformed to
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
(30) Obligation:
IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
(31) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(94)) transformation)
Extracted set of 67 edges for the analysis of TIME complexity. Dropped leaves.
(32) Obligation:
Set of 67 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: all paths from start
(33) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 67 jbc graph edges to a weighted ITS with 67 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.
(34) Obligation:
IntTrs with 67 rules
Start term: main_Load_2(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114
(35) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_2(
o2,
env,
static) -{34,34}>
quot_Load_531(
i8',
i16',
0,
o2,
i5',
env,
static'1) :|:
1 <=
i8' &&
0 <
o2 &&
i15' <=
o20' &&
0 <=
0 &&
o20' <
o2 &&
0 <=
2 &&
0 <=
i15' &&
2 <=
i5' &&
1 <=
i16' &&
0 <
2 &&
0 <=
static'1 &&
0 <=
i8' &&
0 <=
o8' &&
i15' +
1 =
i16' &&
0 <
o20' &&
1 <
i5' &&
0 <=
i5' &&
0 <
1 &&
0 <=
static &&
0 <
i5' &&
0 <=
static''' &&
i5' <
o2 &&
i8' <=
o8' &&
o8' <
o2 &&
0 <
o8' &&
static''' <=
static +
2 &&
0 <
i8' &&
static'1 <=
static''' +
1 &&
1 <=
i5' &&
0 <=
o20' &&
0 <=
1by chaining
main_Load_2(
o2,
env,
static) -{0,0}>
main_Load_4(
o2,
env,
static) :|:
0 <
o2main_Load_4(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_6(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_13(
iconst_0,
o2,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0langle_clinit_rangle_ArrayCreate_13(
iconst_0,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_19(
a2,
o2,
iconst_0,
env,
static) :|:
a2 =
2 &&
0 <
o2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_19(
a2,
o2,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_21(
o2,
env,
static') :|:
0 <=
a2 &&
0 <
o2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_21(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_23(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_New_23(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_24(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticlangle_clinit_rangle_New_24(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_26(
o4,
o2,
env,
static) :|:
o4 =
1 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_Duplicate_26(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_29(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_ConstantStackPush_29(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_32(
o4,
NULL,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_InvokeMethod_32(
o4,
NULL,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_33(
o4,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_init_rangle_Load_33(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_35(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_35(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_37(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Load_37(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_40(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_40(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_42(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_42(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_43(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_43(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_44(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_FieldAccess_44(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Return_45(
o2,
env,
static') :|:
0 <
o2 &&
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
static' <=
static +
o4langle_clinit_rangle_Return_45(
o2,
env,
static) -{1,1}>
main_Load_47(
o2,
env,
static) :|:
0 <
o2main_Load_47(
o2,
env,
static) -{0,0}>
main_Load_48(
o2,
env,
static) :|:
0 <
o2main_Load_48(
o2,
env,
static) -{0,0}>
main_Load_49(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticmain_Load_49(
o2,
env,
static) -{0,0}>
main_Load_50(
o2,
env,
static) :|:
0 <
o2main_Load_50(
o2,
env,
static) -{0,0}>
main_Load_53(
o2,
env,
static) :|:
0 <
o2main_Load_53(
o2,
env,
static) -{1,1}>
main_ConstantStackPush_54(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_54(
o2,
env,
static) -{1,1}>
main_ArrayAccess_56(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_ArrayAccess_56(
a6,
iconst_0,
env,
static) -{0,0}>
main_ArrayAccess_57(
a6,
iconst_0,
i5,
env,
static) :|:
i5 <
a6 &&
iconst_0 =
0 &&
0 <
a6 &&
0 <=
i5main_ArrayAccess_57(
a6,
iconst_0,
i6,
env,
static) -{0,0}>
main_ArrayAccess_59(
a6,
iconst_0,
i6,
env,
static) :|:
0 <=
i6 &&
1 <=
i6 &&
iconst_0 =
0 &&
0 <
a6main_ArrayAccess_59(
a6,
iconst_0,
i6,
env,
static) -{1,1}>
main_InvokeMethod_64(
a6,
o8,
i6,
env,
static) :|:
1 <=
i6 &&
iconst_0 <
i6 &&
0 <=
o8 &&
o8 <
a6 &&
iconst_0 =
0 &&
0 <
a6main_InvokeMethod_64(
a6,
o12,
i6,
env,
static) -{0,0}>
main_InvokeMethod_66(
a6,
o12,
i6,
env,
static) :|:
1 <=
i6 &&
0 <=
o12 &&
0 <
o12 &&
0 <
a6main_InvokeMethod_66(
a6,
o12,
i6,
env,
static) -{1,1}>
main_Store_71(
a6,
i8,
i6,
env,
static) :|:
1 <=
i6 &&
i8 <=
o12 &&
0 <
o12 &&
0 <
a6 &&
0 <=
i8main_Store_71(
a6,
i8,
i6,
env,
static) -{1,1}>
main_Load_79(
a6,
i8,
i6,
env,
static) :|:
1 <=
i6 &&
0 <
a6 &&
0 <=
i8main_Load_79(
a6,
i8,
i6,
env,
static) -{1,1}>
main_ConstantStackPush_83(
a6,
i8,
i6,
env,
static) :|:
1 <=
i6 &&
0 <
a6 &&
0 <=
i8main_ConstantStackPush_83(
a6,
i8,
i6,
env,
static) -{1,1}>
main_ArrayAccess_90(
a6,
iconst_1,
i8,
i6,
env,
static) :|:
1 <=
i6 &&
iconst_1 =
1 &&
0 <
a6 &&
0 <=
i8main_ArrayAccess_90(
a6,
iconst_1,
i8,
i12,
env,
static) -{0,0}>
main_ArrayAccess_108(
a6,
iconst_1,
i8,
i12,
env,
static) :|:
2 <=
i12 &&
iconst_1 =
1 &&
0 <
a6 &&
0 <=
i8 &&
1 <=
i12main_ArrayAccess_108(
a6,
iconst_1,
i8,
i12,
env,
static) -{1,1}>
main_InvokeMethod_111(
a6,
o20,
i8,
i12,
env,
static) :|:
2 <=
i12 &&
iconst_1 =
1 &&
0 <=
o20 &&
iconst_1 <
i12 &&
0 <
a6 &&
0 <=
i8 &&
o20 <
a6main_InvokeMethod_111(
a6,
o23,
i8,
i12,
env,
static) -{0,0}>
main_InvokeMethod_113(
a6,
o23,
i8,
i12,
env,
static) :|:
0 <
o23 &&
2 <=
i12 &&
0 <
a6 &&
0 <=
i8 &&
0 <=
o23main_InvokeMethod_113(
a6,
o23,
i8,
i12,
env,
static) -{1,1}>
main_ConstantStackPush_125(
a6,
i15,
i8,
i12,
env,
static) :|:
0 <
o23 &&
2 <=
i12 &&
0 <
a6 &&
0 <=
i15 &&
0 <=
i8 &&
i15 <=
o23main_ConstantStackPush_125(
a6,
i15,
i8,
i12,
env,
static) -{1,1}>
main_IntArithmetic_133(
a6,
i15,
iconst_1,
i8,
i12,
env,
static) :|:
2 <=
i12 &&
iconst_1 =
1 &&
0 <
a6 &&
0 <=
i15 &&
0 <=
i8main_IntArithmetic_133(
a6,
i15,
iconst_1,
i8,
i12,
env,
static) -{1,1}>
main_Store_140(
a6,
i16,
i8,
i12,
env,
static) :|:
i15 +
iconst_1 =
i16 &&
2 <=
i12 &&
1 <=
i16 &&
iconst_1 =
1 &&
0 <
a6 &&
0 <=
i15 &&
0 <=
i8main_Store_140(
a6,
i16,
i8,
i12,
env,
static) -{1,1}>
main_Load_149(
a6,
i8,
i16,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
0 <
a6 &&
0 <=
i8main_Load_149(
a6,
i8,
i16,
i12,
env,
static) -{1,1}>
main_Load_158(
a6,
i8,
i16,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
0 <
a6 &&
0 <=
i8main_Load_158(
a6,
i8,
i16,
i12,
env,
static) -{1,1}>
main_InvokeMethod_161(
a6,
i8,
i16,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
0 <
a6 &&
0 <=
i8main_InvokeMethod_161(
a6,
i8,
i16,
i12,
env,
static) -{1,1}>
quot_ConstantStackPush_165(
i8,
i16,
a6,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
0 <
a6 &&
0 <=
i8quot_ConstantStackPush_165(
i8,
i16,
a6,
i12,
env,
static) -{1,1}>
quot_Store_173(
iconst_0,
i8,
i16,
a6,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
iconst_0 =
0 &&
0 <
a6 &&
0 <=
i8quot_Store_173(
iconst_0,
i8,
i16,
a6,
i12,
env,
static) -{1,1}>
quot_Load_185(
i8,
i16,
iconst_0,
a6,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
iconst_0 =
0 &&
0 <
a6 &&
0 <=
i8quot_Load_185(
i8,
i16,
iconst_0,
a6,
i12,
env,
static) -{1,1}>
quot_NE_195(
i8,
i16,
iconst_0,
a6,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
iconst_0 =
0 &&
0 <
a6 &&
0 <=
i8quot_NE_195(
i20,
i16,
iconst_0,
a6,
i12,
env,
static) -{0,0}>
quot_NE_204(
i20,
i16,
iconst_0,
a6,
i12,
env,
static) :|:
0 <=
i20 &&
2 <=
i12 &&
1 <=
i16 &&
iconst_0 =
0 &&
0 <
a6 &&
1 <=
i20quot_NE_204(
i20,
i16,
iconst_0,
a6,
i12,
env,
static) -{1,1}>
quot_Load_222(
i20,
i16,
iconst_0,
a6,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
iconst_0 =
0 &&
0 <
i20 &&
0 <
a6 &&
1 <=
i20quot_Load_222(
i20,
i16,
iconst_0,
a6,
i12,
env,
static) -{0,0}>
quot_Load_397(
i20,
i16,
iconst_0,
a6,
i12,
env,
static) :|:
0 <=
iconst_0 &&
2 <=
i12 &&
1 <=
i16 &&
iconst_0 <=
1 &&
iconst_0 =
0 &&
0 <
a6 &&
1 <=
i20quot_Load_397(
i40,
i16,
i41,
a87,
i12,
env,
static) -{0,0}>
quot_Load_471(
i40,
i16,
i41,
a87,
i12,
env,
static) :|:
0 <=
i41 &&
2 <=
i12 &&
1 <=
i16 &&
0 <
a87 &&
i41 <=
2 &&
i41 <=
1quot_Load_471(
i71,
i16,
i72,
a95,
i12,
env,
static) -{0,0}>
quot_Load_531(
i71,
i16,
i72,
a95,
i12,
env,
static) :|:
2 <=
i12 &&
1 <=
i16 &&
i72 <=
2 &&
0 <=
i72 &&
0 <
a95obtained
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
by chaining
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114
(36) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, env, static) -{34,34}> quot_Load_531(i8', i16', 0, o2, i5', env, static'1) :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
(37) 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_2(x1, x2, x3) → main_Load_2(x1, x3)
quot_Load_531(x1, x2, x3, x4, x5, x6, x7) → quot_Load_531(x1, x2, x3, x4, x5)
(38) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i16', 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
(39) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' - i16 - 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i16', 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
was transformed to
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
(40) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' - i16 - 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
(41) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' - i16 - 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' + -1 * i16 + 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' + -1 * i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
was transformed to
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && o20' < o2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 <= static'1 && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1
(42) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' + -1 * i16 + 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' + -1 * i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && o20' < o2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 <= static'1 && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1