time complexity proof of /tmp/tmpE8GaZi/StupidArray.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 41).

0 JBC problem

↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 178 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)), 0 ms)

↳4 JBCComplexityEdges

    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 133 ms)

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 55 ms)

        ↳8 WeightedIntTrs

        ↳9 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳10 WeightedIntTrs

        ↳11 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳12 WeightedIntTrs

    ↳13 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 127 ms)

    ↳14 WeightedIntTrs

        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 40 ms)

        ↳16 WeightedIntTrs

        ↳17 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳18 WeightedIntTrs

        ↳19 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳20 WeightedIntTrs

        ↳21 CESProof (⇔, 47 ms)

        ↳22 BOUNDS(CONSTANT, 40)

↳23 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)), 0 ms)

↳24 JBCComplexityEdges

    ↳25 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 112 ms)

    ↳26 WeightedIntTrs

    ↳27 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 16 ms)

    ↳28 WeightedIntTrs

    ↳29 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 27 ms)

    ↳30 WeightedIntTrs

    ↳31 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳32 WeightedIntTrs

    ↳33 koat Proof (⇔, 2 ms)

    ↳34 BOUNDS(CONSTANT, 18)

(0) Obligation:

Need to prove time_complexity of the following program:

public class StupidArray {
  public static void main(String[] args) {
    int i = 0;
    while (true) {
      i = args.length + 1;
      args[i] = new String();
    }
  }
}

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
StupidArray.main([Ljava/lang/String;)V: Graph of 80 nodes with 1 SCC.

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)) transformation)

Extracted set of 57 edges for the analysis of TIME complexity. Kept leaves.

(4) Obligation:

Set of 57 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 57 jbc graph edges to a weighted ITS with 57 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 57 rules
Start term: main_ConstantStackPush_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(o1, env, static) -{0,0}> main_ConstantStackPush_3(o1, env, static) :|: 0 < o1
main_ConstantStackPush_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_6(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_14(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_16(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_18(o1, env, static) -{0,0}> langle_clinit_rangle_New_19(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_19(o1, env, static) -{0,0}> langle_clinit_rangle_New_21(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_21(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_23(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_25(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_27(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_29(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_29(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_31(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_33(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_36(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_37(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_41(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_43(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_45(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_45(o1, env, static) -{1,1}> main_ConstantStackPush_47(o1, env, static) :|: 0 < o1
main_ConstantStackPush_47(o1, env, static) -{0,0}> main_ConstantStackPush_48(o1, env, static) :|: 0 < o1
main_ConstantStackPush_48(o1, env, static) -{0,0}> main_ConstantStackPush_49(o1, env, static) :|: 0 <= static && 0 < o1
main_ConstantStackPush_49(o1, env, static) -{0,0}> main_ConstantStackPush_51(o1, env, static) :|: 0 < o1
main_ConstantStackPush_51(o1, env, static) -{0,0}> main_ConstantStackPush_52(o1, env, static) :|: 0 < o1
main_ConstantStackPush_52(o1, env, static) -{1,1}> main_Store_54(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
main_Store_54(o1, iconst_0, env, static) -{1,1}> main_Load_56(o1, env, static) :|: iconst_0 = 0 && 0 < o1
main_Load_56(o1, env, static) -{1,1}> main_ArrayLength_57(o1, env, static) :|: 0 < o1
main_ArrayLength_57(o1, env, static) -{0,0}> main_ArrayLength_142(o1, env, static) :|: 0 < o1
main_ArrayLength_142(a16, env, static) -{0,0}> main_ArrayLength_145(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_145(a16, i8, env, static) -{1,1}> main_ConstantStackPush_146(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_146(a16, i8, env, static) -{1,1}> main_IntArithmetic_149(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_149(a16, i8, iconst_1, env, static) -{1,1}> main_Store_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_151(a16, i9, i8, env, static) -{1,1}> main_Load_153(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_153(a16, i9, i8, env, static) -{1,1}> main_Load_154(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_154(a16, i9, i8, env, static) -{1,1}> main_New_156(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_156(a16, i9, i8, env, static) -{1,1}> main_Duplicate_158(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_158(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_160(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_160(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_192(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_192(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_194(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_196(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_197(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_196(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_202(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_202(a21, i8, env, static) -{1,1}> main_Load_208(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_208(a21, i8, env, static) -{1,1}> main_ArrayLength_215(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_215(a21, i8, env, static) -{0,0}> main_ArrayLength_142(a21, env, static) :|: 0 < a21 && 0 <= i8

(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_ConstantStackPush_1(o1, env, static) -{0,0}> main_ConstantStackPush_3(o1, env, static) :|: 0 < o1
main_ConstantStackPush_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_6(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_14(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_16(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_18(o1, env, static) -{0,0}> langle_clinit_rangle_New_19(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_19(o1, env, static) -{0,0}> langle_clinit_rangle_New_21(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_21(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_23(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_25(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_27(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_29(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_29(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_31(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_33(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_36(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_37(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_41(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_43(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_45(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_45(o1, env, static) -{1,1}> main_ConstantStackPush_47(o1, env, static) :|: 0 < o1
main_ConstantStackPush_47(o1, env, static) -{0,0}> main_ConstantStackPush_48(o1, env, static) :|: 0 < o1
main_ConstantStackPush_48(o1, env, static) -{0,0}> main_ConstantStackPush_49(o1, env, static) :|: 0 <= static && 0 < o1
main_ConstantStackPush_49(o1, env, static) -{0,0}> main_ConstantStackPush_51(o1, env, static) :|: 0 < o1
main_ConstantStackPush_51(o1, env, static) -{0,0}> main_ConstantStackPush_52(o1, env, static) :|: 0 < o1
main_ConstantStackPush_52(o1, env, static) -{1,1}> main_Store_54(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
main_Store_54(o1, iconst_0, env, static) -{1,1}> main_Load_56(o1, env, static) :|: iconst_0 = 0 && 0 < o1
main_Load_56(o1, env, static) -{1,1}> main_ArrayLength_57(o1, env, static) :|: 0 < o1
main_ArrayLength_57(o1, env, static) -{0,0}> main_ArrayLength_142(o1, env, static) :|: 0 < o1

obtained
main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i9', 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
by chaining
main_ArrayLength_142(a16, env, static) -{0,0}> main_ArrayLength_145(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_145(a16, i8, env, static) -{1,1}> main_ConstantStackPush_146(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_146(a16, i8, env, static) -{1,1}> main_IntArithmetic_149(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_149(a16, i8, iconst_1, env, static) -{1,1}> main_Store_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_151(a16, i9, i8, env, static) -{1,1}> main_Load_153(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_153(a16, i9, i8, env, static) -{1,1}> main_Load_154(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_154(a16, i9, i8, env, static) -{1,1}> main_New_156(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_156(a16, i9, i8, env, static) -{1,1}> main_Duplicate_158(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_158(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_160(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_160(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_192(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_192(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_194(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8

obtained
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_142(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
by chaining
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_196(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_196(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_202(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_202(a21, i8, env, static) -{1,1}> main_Load_208(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_208(a21, i8, env, static) -{1,1}> main_ArrayLength_215(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_215(a21, i8, env, static) -{0,0}> main_ArrayLength_142(a21, env, static) :|: 0 < a21 && 0 <= i8

(8) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i9', 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_197(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_142(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21

(9) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i9', 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
was transformed to
main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16

(10) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_197(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_142(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16

(11) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1

main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
was transformed to
main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 1 <= i9' && i8 < a16

(12) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_197(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_142(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 1 <= i9' && i8 < a16

(13) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 57 jbc graph edges to a weighted ITS with 57 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.

(14) Obligation:

(15) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

(18) Obligation:

(19) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

(20) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_197(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_142(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
main_ArrayLength_142(a16, env, static) -{22,22}> main_ArrayAccess_194(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 1 <= i9' && i8 < a16

(21) CESProof (EQUIVALENT transformation)

proved upper bound 40 using cofloco

(22) BOUNDS(CONSTANT, 40)

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)) transformation)

Extracted set of 56 edges for the analysis of TIME complexity. Dropped leaves.

(24) Obligation:

Set of 56 edges based on JBC Program.
Performed SCC analyses:

Used field analysis yielded the following read fields:

Considered paths: all paths from start

(25) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 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.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(26) Obligation:

IntTrs with 56 rules
Start term: main_ConstantStackPush_1(args, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(o1, env, static) -{0,0}> main_ConstantStackPush_3(o1, env, static) :|: 0 < o1
main_ConstantStackPush_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_6(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_14(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_16(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_18(o1, env, static) -{0,0}> langle_clinit_rangle_New_19(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_19(o1, env, static) -{0,0}> langle_clinit_rangle_New_21(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_21(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_23(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_25(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_27(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_29(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_29(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_31(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_33(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_36(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_37(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_41(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_43(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_45(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_45(o1, env, static) -{1,1}> main_ConstantStackPush_47(o1, env, static) :|: 0 < o1
main_ConstantStackPush_47(o1, env, static) -{0,0}> main_ConstantStackPush_48(o1, env, static) :|: 0 < o1
main_ConstantStackPush_48(o1, env, static) -{0,0}> main_ConstantStackPush_49(o1, env, static) :|: 0 <= static && 0 < o1
main_ConstantStackPush_49(o1, env, static) -{0,0}> main_ConstantStackPush_51(o1, env, static) :|: 0 < o1
main_ConstantStackPush_51(o1, env, static) -{0,0}> main_ConstantStackPush_52(o1, env, static) :|: 0 < o1
main_ConstantStackPush_52(o1, env, static) -{1,1}> main_Store_54(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
main_Store_54(o1, iconst_0, env, static) -{1,1}> main_Load_56(o1, env, static) :|: iconst_0 = 0 && 0 < o1
main_Load_56(o1, env, static) -{1,1}> main_ArrayLength_57(o1, env, static) :|: 0 < o1
main_ArrayLength_57(o1, env, static) -{0,0}> main_ArrayLength_142(o1, env, static) :|: 0 < o1
main_ArrayLength_142(a16, env, static) -{0,0}> main_ArrayLength_145(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_145(a16, i8, env, static) -{1,1}> main_ConstantStackPush_146(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_146(a16, i8, env, static) -{1,1}> main_IntArithmetic_149(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_149(a16, i8, iconst_1, env, static) -{1,1}> main_Store_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_151(a16, i9, i8, env, static) -{1,1}> main_Load_153(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_153(a16, i9, i8, env, static) -{1,1}> main_Load_154(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_154(a16, i9, i8, env, static) -{1,1}> main_New_156(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_156(a16, i9, i8, env, static) -{1,1}> main_Duplicate_158(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_158(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_160(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_160(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_192(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_192(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_194(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_196(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_196(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_202(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_202(a21, i8, env, static) -{1,1}> main_Load_208(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_208(a21, i8, env, static) -{1,1}> main_ArrayLength_215(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_215(a21, i8, env, static) -{0,0}> main_ArrayLength_142(a21, env, static) :|: 0 < a21 && 0 <= i8

(27) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_ArrayLength_142(a16, env, static) -{25,25}> main_ArrayLength_142(a21''', env, static) :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < 1 && 0 < a16 && 0 < 2 && i8 + 1 = i9'
by chaining
main_ArrayLength_142(a16, env, static) -{0,0}> main_ArrayLength_145(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_145(a16, i8, env, static) -{1,1}> main_ConstantStackPush_146(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_146(a16, i8, env, static) -{1,1}> main_IntArithmetic_149(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_149(a16, i8, iconst_1, env, static) -{1,1}> main_Store_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_151(a16, i9, i8, env, static) -{1,1}> main_Load_153(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_153(a16, i9, i8, env, static) -{1,1}> main_Load_154(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_154(a16, i9, i8, env, static) -{1,1}> main_New_156(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_156(a16, i9, i8, env, static) -{1,1}> main_Duplicate_158(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_158(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_160(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_160(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_162(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_164(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_169(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_171(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_179(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_181(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_182(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_184(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_187(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_192(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_192(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_194(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_194(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_196(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_196(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_202(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_202(a21, i8, env, static) -{1,1}> main_Load_208(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_208(a21, i8, env, static) -{1,1}> main_ArrayLength_215(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_215(a21, i8, env, static) -{0,0}> main_ArrayLength_142(a21, env, static) :|: 0 < a21 && 0 <= i8

(28) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_1(args, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(o1, env, static) -{18,18}> main_ArrayLength_142(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayLength_142(a16, env, static) -{25,25}> main_ArrayLength_142(a21''', env, static) :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < 1 && 0 < a16 && 0 < 2 && i8 + 1 = i9'

(29) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:

main_ConstantStackPush_1(x1, x2, x3) → main_ConstantStackPush_1(x1, x3)
main_ArrayLength_142(x1, x2, x3) → main_ArrayLength_142(x1)

(30) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_1(args, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(o1, static) -{18,18}> main_ArrayLength_142(o1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayLength_142(a16) -{25,25}> main_ArrayLength_142(a21''') :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < 1 && 0 < a16 && 0 < 2 && i8 + 1 = i9'

(31) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

main_ConstantStackPush_1(o1, static) -{18,18}> main_ArrayLength_142(o1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_1(o1, static) -{18,18}> main_ArrayLength_142(o1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1

main_ArrayLength_142(a16) -{25,25}> main_ArrayLength_142(a21''') :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < 1 && 0 < a16 && 0 < 2 && i8 + 1 = i9'
was transformed to
main_ArrayLength_142(a16) -{25,25}> main_ArrayLength_142(a21''') :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < a16 && i8 + 1 = i9'

(32) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_1(args, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(o1, static) -{18,18}> main_ArrayLength_142(o1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1
main_ArrayLength_142(a16) -{25,25}> main_ArrayLength_142(a21''') :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < a16 && i8 + 1 = i9'

(33) koat Proof (EQUIVALENT transformation)

YES(?, 18)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 18) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_ArrayLength_142(ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= static'1 /\ 0 <= static''' /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 25) main_ArrayLength_142(ar_0, ar_1) -> Com_1(main_ArrayLength_142(a21''', arityPad)) [ i9' < i8 /\ 0 < a21''' /\ 0 <= i8 /\ i8 < ar_0 /\ a21''' <= ar_0 + 1 /\ 1 <= i9' /\ 0 < ar_0 /\ i8 + 1 = i9' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 1:
main_ArrayLength_142(ar_0, ar_1) -> Com_1(main_ArrayLength_142(a21''', arityPad)) [ i9' < i8 /\ 0 < a21''' /\ 0 <= i8 /\ i8 < ar_0 /\ a21''' <= ar_0 + 1 /\ 1 <= i9' /\ 0 < ar_0 /\ i8 + 1 = i9' ]
We thus obtain the following problem:
2: T:
(Comp: ?, Cost: 18) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_ArrayLength_142(ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= static'1 /\ 0 <= static''' /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: 1, Cost: 18) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_ArrayLength_142(ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= static'1 /\ 0 <= static''' /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 18

Time: 0.039 sec (SMT: 0.037 sec)

(0) Obligation:

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)) transformation)

(4) Obligation:

(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(6) Obligation:

(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(14) Obligation:

(15) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) CESProof (EQUIVALENT transformation)

(22) BOUNDS(CONSTANT, 40)

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)) transformation)

(24) Obligation:

(25) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(26) Obligation:

(27) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(28) Obligation:

(29) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

(30) Obligation:

(31) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(32) Obligation:

(33) koat Proof (EQUIVALENT transformation)

(34) BOUNDS(CONSTANT, 18)