(0) Obligation:
Need to prove time_complexity of the following program:
/**
* An example of nested iterations.
*
* All calls terminate.
*
* Julia + BinTerm prove that all calls terminate
*
* @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
*/
public class Nested {
public static void main(String[] args) {
for (int i = 0; i < 10; i++)
for (int j = 3; j < 12; j += 2) {
j -= 1;
}
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
Nested.main([Ljava/lang/String;)V: Graph of 57 nodes with 1 SCC.
(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)
Extracted set of 56 edges for the analysis of TIME complexity. Kept leaves.
(4) Obligation:
Set of 56 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 56 jbc graph edges to a weighted ITS with 56 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.
(6) Obligation:
IntTrs with 56 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(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_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71
(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_ConstantStackPush_2(
o2,
env,
static) -{22,22}>
main_Load_312(
o2,
0,
3,
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
2 &&
static''' <=
static +
2 &&
0 <
o2 &&
0 <=
0 &&
0 <=
static''' &&
0 <=
static &&
0 <=
1 &&
0 <
1 &&
0 <
2 &&
0 <=
static'1by chaining
main_ConstantStackPush_2(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_3(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_3(
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_16(
a2,
o2,
iconst_0,
env,
static) :|:
a2 =
2 &&
0 <
o2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_16(
a2,
o2,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_17(
o2,
env,
static') :|:
0 <=
a2 &&
0 <
o2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_17(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_New_18(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_20(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticlangle_clinit_rangle_New_20(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o4,
o2,
env,
static) :|:
o4 =
1 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_Duplicate_21(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_23(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_ConstantStackPush_23(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_25(
o4,
NULL,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_InvokeMethod_25(
o4,
NULL,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o4,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_init_rangle_Load_27(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_29(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_29(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_31(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Load_31(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_33(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_33(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_37(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_37(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_38(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_38(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_39(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_FieldAccess_39(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
o2,
env,
static') :|:
0 <
o2 &&
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
static' <=
static +
o4langle_clinit_rangle_Return_40(
o2,
env,
static) -{1,1}>
main_ConstantStackPush_46(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_46(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_47(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_47(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_50(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticmain_ConstantStackPush_50(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_51(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_51(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_52(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_52(
o2,
env,
static) -{1,1}>
main_Store_53(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_Store_53(
o2,
iconst_0,
env,
static) -{1,1}>
main_Load_54(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_Load_54(
o2,
iconst_0,
env,
static) -{1,1}>
main_ConstantStackPush_55(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_ConstantStackPush_55(
o2,
iconst_0,
env,
static) -{1,1}>
main_GE_56(
o2,
iconst_0,
iconst_10,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0 &&
iconst_10 =
10main_GE_56(
o2,
iconst_0,
iconst_10,
env,
static) -{1,1}>
main_ConstantStackPush_58(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0 &&
iconst_10 =
10main_ConstantStackPush_58(
o2,
iconst_0,
env,
static) -{1,1}>
main_Store_60(
o2,
iconst_3,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Store_60(
o2,
iconst_3,
iconst_0,
env,
static) -{1,1}>
main_Load_62(
o2,
iconst_0,
iconst_3,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Load_62(
o2,
iconst_0,
iconst_3,
env,
static) -{0,0}>
main_Load_161(
o2,
iconst_0,
iconst_3,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Load_161(
o70,
iconst_0,
i11,
env,
static) -{0,0}>
main_Load_214(
o70,
iconst_0,
i11,
env,
static) :|:
0 <=
iconst_0 &&
iconst_0 <=
1 &&
iconst_0 =
0 &&
0 <
o70main_Load_214(
o94,
i24,
i25,
env,
static) -{0,0}>
main_Load_263(
o94,
i24,
i25,
env,
static) :|:
0 <=
i24 &&
i24 <=
1 &&
i24 <=
2 &&
0 <
o94main_Load_263(
o114,
i38,
i39,
env,
static) -{0,0}>
main_Load_312(
o114,
i38,
i39,
env,
static) :|:
0 <
o114 &&
0 <=
i38 &&
i38 <=
2obtained
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
by chaining
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
obtained
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
by chaining
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
obtained
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
by chaining
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71
obtained
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
by chaining
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
(8) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from lhss to constraints.
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
was transformed to
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
(10) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
(11) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
was transformed to
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
(12) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
(13) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
was transformed to
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
(14) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
(15) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 56 jbc graph edges to a weighted ITS with 56 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.
(16) Obligation:
IntTrs with 56 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(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_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71
(17) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_ConstantStackPush_2(
o2,
env,
static) -{22,22}>
main_Load_312(
o2,
0,
3,
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
2 &&
static''' <=
static +
2 &&
0 <
o2 &&
0 <=
0 &&
0 <=
static''' &&
0 <=
static &&
0 <=
1 &&
0 <
1 &&
0 <
2 &&
0 <=
static'1by chaining
main_ConstantStackPush_2(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_3(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_3(
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_16(
a2,
o2,
iconst_0,
env,
static) :|:
a2 =
2 &&
0 <
o2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_16(
a2,
o2,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_17(
o2,
env,
static') :|:
0 <=
a2 &&
0 <
o2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_17(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_New_18(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_20(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticlangle_clinit_rangle_New_20(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o4,
o2,
env,
static) :|:
o4 =
1 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_Duplicate_21(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_23(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_ConstantStackPush_23(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_25(
o4,
NULL,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_InvokeMethod_25(
o4,
NULL,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o4,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_init_rangle_Load_27(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_29(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_29(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_31(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Load_31(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_33(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_33(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_37(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_37(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_38(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_38(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_39(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_FieldAccess_39(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
o2,
env,
static') :|:
0 <
o2 &&
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
static' <=
static +
o4langle_clinit_rangle_Return_40(
o2,
env,
static) -{1,1}>
main_ConstantStackPush_46(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_46(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_47(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_47(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_50(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticmain_ConstantStackPush_50(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_51(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_51(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_52(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_52(
o2,
env,
static) -{1,1}>
main_Store_53(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_Store_53(
o2,
iconst_0,
env,
static) -{1,1}>
main_Load_54(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_Load_54(
o2,
iconst_0,
env,
static) -{1,1}>
main_ConstantStackPush_55(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_ConstantStackPush_55(
o2,
iconst_0,
env,
static) -{1,1}>
main_GE_56(
o2,
iconst_0,
iconst_10,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0 &&
iconst_10 =
10main_GE_56(
o2,
iconst_0,
iconst_10,
env,
static) -{1,1}>
main_ConstantStackPush_58(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0 &&
iconst_10 =
10main_ConstantStackPush_58(
o2,
iconst_0,
env,
static) -{1,1}>
main_Store_60(
o2,
iconst_3,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Store_60(
o2,
iconst_3,
iconst_0,
env,
static) -{1,1}>
main_Load_62(
o2,
iconst_0,
iconst_3,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Load_62(
o2,
iconst_0,
iconst_3,
env,
static) -{0,0}>
main_Load_161(
o2,
iconst_0,
iconst_3,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Load_161(
o70,
iconst_0,
i11,
env,
static) -{0,0}>
main_Load_214(
o70,
iconst_0,
i11,
env,
static) :|:
0 <=
iconst_0 &&
iconst_0 <=
1 &&
iconst_0 =
0 &&
0 <
o70main_Load_214(
o94,
i24,
i25,
env,
static) -{0,0}>
main_Load_263(
o94,
i24,
i25,
env,
static) :|:
0 <=
i24 &&
i24 <=
1 &&
i24 <=
2 &&
0 <
o94main_Load_263(
o114,
i38,
i39,
env,
static) -{0,0}>
main_Load_312(
o114,
i38,
i39,
env,
static) :|:
0 <
o114 &&
0 <=
i38 &&
i38 <=
2obtained
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
by chaining
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
obtained
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
by chaining
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
obtained
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
by chaining
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71
obtained
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
by chaining
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
(18) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
(19) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from lhss to constraints.
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
was transformed to
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
(20) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
(21) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
was transformed to
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
(22) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
(23) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
was transformed to
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
(24) Obligation:
IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)
Extracted set of 55 edges for the analysis of TIME complexity. Dropped leaves.
(26) Obligation:
Set of 55 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: all paths from start
(27) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 55 jbc graph edges to a weighted ITS with 55 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.
(28) Obligation:
IntTrs with 55 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(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_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71
(29) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_ConstantStackPush_2(
o2,
env,
static) -{22,22}>
main_Load_312(
o2,
0,
3,
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
2 &&
static''' <=
static +
2 &&
0 <
o2 &&
0 <=
0 &&
0 <=
static''' &&
0 <=
static &&
0 <=
1 &&
0 <
1 &&
0 <
2 &&
0 <=
static'1by chaining
main_ConstantStackPush_2(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_3(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_3(
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_16(
a2,
o2,
iconst_0,
env,
static) :|:
a2 =
2 &&
0 <
o2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_16(
a2,
o2,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_17(
o2,
env,
static') :|:
0 <=
a2 &&
0 <
o2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_17(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
o2,
env,
static) :|:
0 <
o2langle_clinit_rangle_New_18(
o2,
env,
static) -{0,0}>
langle_clinit_rangle_New_20(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticlangle_clinit_rangle_New_20(
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o4,
o2,
env,
static) :|:
o4 =
1 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_Duplicate_21(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_23(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_ConstantStackPush_23(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_25(
o4,
NULL,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_clinit_rangle_InvokeMethod_25(
o4,
NULL,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o4,
o2,
env,
static) :|:
NULL =
0 &&
0 <
o2 &&
0 <
o4langle_init_rangle_Load_27(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_29(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_29(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Load_31(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Load_31(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_33(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_InvokeMethod_33(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_37(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_37(
o4,
o2,
env,
static) -{1,1}>
langle_init_rangle_Return_38(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_init_rangle_Return_38(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_39(
o4,
o2,
env,
static) :|:
0 <
o2 &&
0 <
o4langle_clinit_rangle_FieldAccess_39(
o4,
o2,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
o2,
env,
static') :|:
0 <
o2 &&
0 <=
o4 &&
0 <
o4 &&
0 <=
static &&
static' <=
static +
o4langle_clinit_rangle_Return_40(
o2,
env,
static) -{1,1}>
main_ConstantStackPush_46(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_46(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_47(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_47(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_50(
o2,
env,
static) :|:
0 <
o2 &&
0 <=
staticmain_ConstantStackPush_50(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_51(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_51(
o2,
env,
static) -{0,0}>
main_ConstantStackPush_52(
o2,
env,
static) :|:
0 <
o2main_ConstantStackPush_52(
o2,
env,
static) -{1,1}>
main_Store_53(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_Store_53(
o2,
iconst_0,
env,
static) -{1,1}>
main_Load_54(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_Load_54(
o2,
iconst_0,
env,
static) -{1,1}>
main_ConstantStackPush_55(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0main_ConstantStackPush_55(
o2,
iconst_0,
env,
static) -{1,1}>
main_GE_56(
o2,
iconst_0,
iconst_10,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0 &&
iconst_10 =
10main_GE_56(
o2,
iconst_0,
iconst_10,
env,
static) -{1,1}>
main_ConstantStackPush_58(
o2,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_0 =
0 &&
iconst_10 =
10main_ConstantStackPush_58(
o2,
iconst_0,
env,
static) -{1,1}>
main_Store_60(
o2,
iconst_3,
iconst_0,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Store_60(
o2,
iconst_3,
iconst_0,
env,
static) -{1,1}>
main_Load_62(
o2,
iconst_0,
iconst_3,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Load_62(
o2,
iconst_0,
iconst_3,
env,
static) -{0,0}>
main_Load_161(
o2,
iconst_0,
iconst_3,
env,
static) :|:
0 <
o2 &&
iconst_3 =
3 &&
iconst_0 =
0main_Load_161(
o70,
iconst_0,
i11,
env,
static) -{0,0}>
main_Load_214(
o70,
iconst_0,
i11,
env,
static) :|:
0 <=
iconst_0 &&
iconst_0 <=
1 &&
iconst_0 =
0 &&
0 <
o70main_Load_214(
o94,
i24,
i25,
env,
static) -{0,0}>
main_Load_263(
o94,
i24,
i25,
env,
static) :|:
0 <=
i24 &&
i24 <=
1 &&
i24 <=
2 &&
0 <
o94main_Load_263(
o114,
i38,
i39,
env,
static) -{0,0}>
main_Load_312(
o114,
i38,
i39,
env,
static) :|:
0 <
o114 &&
0 <=
i38 &&
i38 <=
2obtained
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
by chaining
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
obtained
main_GE_320(o134, i61, 12, i52, env, static) -{10,10}> main_GE_320(o134, 3, 12, i63', env, static) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
by chaining
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71
obtained
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
by chaining
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
(30) Obligation:
IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, 12, i52, env, static) -{10,10}> main_GE_320(o134, 3, 12, i63', env, static) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
(31) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)
Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:
main_ConstantStackPush_2(x1, x2, x3) → main_ConstantStackPush_2(x1, x3)
main_Load_312(x1, x2, x3, x4, x5) → main_Load_312(x1, x2, x3)
main_GE_320(x1, x2, x3, x4, x5, x6) → main_GE_320(x1, x2, x4)
(32) Obligation:
IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53) -{2,2}> main_GE_320(o134, i53, i52) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i63') :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i64') :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
(33) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i64') :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i63') :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
was transformed to
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
(34) Obligation:
IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, static)
Considered paths: all paths from start
Rules:
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
main_Load_312(o134, i52, i53) -{2,2}> main_GE_320(o134, i53, i52) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
(35) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + 1) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
was transformed to
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
(36) Obligation:
IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_Load_312(o134, i52, i53) -{2,2}> main_GE_320(o134, i53, i52) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + 1) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
(37) koat Proof (EQUIVALENT transformation)
YES(?, 900*ar_0 + 114)
Initial complexity problem:
1: T:
(Comp: ?, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: ?, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: ?, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
A polynomial rank function with
Pol(main_ConstantStackPush_2) = 9*V_1
Pol(main_Load_312) = 9*V_1 - V_2
Pol(main_GE_320) = 9*V_1 - V_3
Pol(koat_start) = 9*V_1
orients all transitions weakly and the transition
main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: 9*ar_0, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
A polynomial rank function with
Pol(main_Load_312) = -V_3 + 12
Pol(main_GE_320) = -V_2 + 12
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-2) = ar_2
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\\ 1 <= i63' /\\ i63' < 10 /\\ i63' <= 9 /\\ 0 < ar_0 /\\ 0 <= i63' /\\ 12 <= ar_1 /\\ 0 <= ar_2 ]", 0-0) = ar_0
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\\ 1 <= i63' /\\ i63' < 10 /\\ i63' <= 9 /\\ 0 < ar_0 /\\ 0 <= i63' /\\ 12 <= ar_1 /\\ 0 <= ar_2 ]", 0-1) = 3
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\\ 1 <= i63' /\\ i63' < 10 /\\ i63' <= 9 /\\ 0 < ar_0 /\\ 0 <= i63' /\\ 12 <= ar_1 /\\ 0 <= ar_2 ]", 0-2) = 9
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\\ i64' <= 12 /\\ i62' <= 10 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ ar_1 - 1 = i62' /\\ i62' + 2 = i64' /\\ ar_1 < 12 ]", 0-0) = ar_0
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\\ i64' <= 12 /\\ i62' <= 10 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ ar_1 - 1 = i62' /\\ i62' + 2 = i64' /\\ ar_1 < 12 ]", 0-1) = 9
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\\ i64' <= 12 /\\ i62' <= 10 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ ar_1 - 1 = i62' /\\ i62' + 2 = i64' /\\ ar_1 < 12 ]", 0-2) = 12
S("main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-0) = ar_0
S("main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-1) = 12
S("main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-2) = 9
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\\ static''' <= ar_1 + 2 /\\ 0 < ar_0 /\\ 0 <= static''' /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\\ static''' <= ar_1 + 2 /\\ 0 < ar_0 /\\ 0 <= static''' /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-1) = 0
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\\ static''' <= ar_1 + 2 /\\ 0 < ar_0 /\\ 0 <= static''' /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-2) = 3
orients the transitions
main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
weakly and the transition
main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 135*ar_0 + 15, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: 9*ar_0, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 135*ar_0 + 16, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 135*ar_0 + 15, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: 9*ar_0, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Complexity upper bound 900*ar_0 + 114
Time: 0.114 sec (SMT: 0.102 sec)
(38) BOUNDS(CONSTANT, 114 + 900 * |o2|)