time complexity proof of /tmp/tmp5qcw9Q/CountUpRound.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 67 + 25 * |#0| + 25 * |#1|).

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 14 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

        ↳11 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 83 ms)

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

        ↳21 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 1 ms)

        ↳22 WeightedIntTrs

        ↳23 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

↳29 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 14 ms)

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 86 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 26 ms)

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 21 ms)

    ↳36 WeightedIntTrs

    ↳37 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳38 WeightedIntTrs

    ↳39 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

    ↳45 koat Proof (⇔, 63 ms)

    ↳46 BOUNDS(CONSTANT, 63 + 25 * |#0| + 25 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class CountUpRound{
  public static int round (int x) {

    if (x % 2 == 0) return x;
    else return x+1;
  }


  public static void main(int x, int y) {

    while (x > y) {

      y = round(y+1);

    }


  }

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CountUpRound.main(II)V: Graph of 61 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 58 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 58 jbc graph edges to a weighted ITS with 58 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 58 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_Load_49(i2, i4, env, static) :|: 0 >= 0
main_Load_49(i2, i4, env, static) -{1,1}> main_LE_55(i2, i4, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_65(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_65(i2, i4, env, static) -{1,1}> main_IntArithmetic_66(i2, i4, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_66(i2, i4, iconst_1, env, static) -{1,1}> main_InvokeMethod_68(i2, i4, i6, env, static) :|: iconst_1 = 1 && i4 + iconst_1 = i6
main_InvokeMethod_68(i2, i4, i6, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i6, env, static) :|: 0 >= 0
main_InvokeMethod_218(i2, i4, i32, env, static) -{1,1}> round_Load_221(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_221(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_224(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_224(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) :|: iconst_2 = 2
round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) -{1,1}> round_NE_230(i41, i32, i2, i4, env, static) :|: i32 % iconst_2 = i41 && -1 <= i41 && i41 <= 1 && iconst_2 = 2
round_NE_230(i45, i32, i2, i4, env, static) -{0,0}> round_NE_233(i45, i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1
round_NE_230(iconst_0, i32, i2, i4, env, static) -{0,0}> round_NE_234(iconst_0, i32, i2, i4, env, static) :|: -1 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
round_NE_233(i45, i32, i2, i4, env, static) -{1,1}> round_Load_235(i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1 && !(i45 = 0)
round_NE_234(iconst_0, i32, i2, i4, env, static) -{1,1}> round_Load_238(i32, i2, i4, env, static) :|: iconst_0 = 0
round_Load_235(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_241(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_238(i32, i2, i4, env, static) -{1,1}> round_Return_243(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_241(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) :|: iconst_1 = 1
round_Return_243(i32, i2, i4, env, static) -{1,1}> main_Store_247(i2, i4, i32, env, static) :|: 0 >= 0
round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) -{1,1}> round_Return_250(i49, i2, i4, env, static) :|: i32 + iconst_1 = i49 && iconst_1 = 1
main_Store_247(i2, i4, i32, env, static) -{0,0}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0
round_Return_250(i49, i2, i4, env, static) -{1,1}> main_Store_270(i2, i4, i49, env, static) :|: 0 >= 0
main_Store_270(i2, i4, i49, env, static) -{1,1}> main_JMP_273(i2, i4, i49, env, static) :|: 0 >= 0
main_JMP_273(i2, i4, i49, env, static) -{1,1}> main_Load_279(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_279(i2, i4, i49, env, static) -{1,1}> main_Load_287(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_287(i2, i4, i49, env, static) -{1,1}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_318(i2, i4, i49, env, static) :|: i49 < i2
main_LE_318(i2, i4, i49, env, static) -{1,1}> main_Load_336(i2, i4, i49, env, static) :|: i49 < i2
main_Load_336(i2, i4, i49, env, static) -{1,1}> main_ConstantStackPush_341(i2, i4, i49, env, static) :|: 0 >= 0
main_ConstantStackPush_341(i2, i4, i49, env, static) -{1,1}> main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) -{1,1}> main_InvokeMethod_366(i2, i4, i65, env, static) :|: iconst_1 = 1 && i49 + iconst_1 = i65
main_InvokeMethod_366(i2, i4, i65, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i65, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_Load_49(i2, i4, env, static) :|: 0 >= 0
main_Load_49(i2, i4, env, static) -{1,1}> main_LE_55(i2, i4, env, static) :|: 0 >= 0

obtained
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
by chaining
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_65(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_65(i2, i4, env, static) -{1,1}> main_IntArithmetic_66(i2, i4, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_66(i2, i4, iconst_1, env, static) -{1,1}> main_InvokeMethod_68(i2, i4, i6, env, static) :|: iconst_1 = 1 && i4 + iconst_1 = i6
main_InvokeMethod_68(i2, i4, i6, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i6, env, static) :|: 0 >= 0

obtained
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && i41' <= 1 && i32 % 2 = i41' && -1 <= i41'
by chaining
main_InvokeMethod_218(i2, i4, i32, env, static) -{1,1}> round_Load_221(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_221(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_224(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_224(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) :|: iconst_2 = 2
round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) -{1,1}> round_NE_230(i41, i32, i2, i4, env, static) :|: i32 % iconst_2 = i41 && -1 <= i41 && i41 <= 1 && iconst_2 = 2

obtained
round_NE_230(0, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1
by chaining
round_NE_230(iconst_0, i32, i2, i4, env, static) -{0,0}> round_NE_234(iconst_0, i32, i2, i4, env, static) :|: -1 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
round_NE_234(iconst_0, i32, i2, i4, env, static) -{1,1}> round_Load_238(i32, i2, i4, env, static) :|: iconst_0 = 0
round_Load_238(i32, i2, i4, env, static) -{1,1}> round_Return_243(i32, i2, i4, env, static) :|: 0 >= 0
round_Return_243(i32, i2, i4, env, static) -{1,1}> main_Store_247(i2, i4, i32, env, static) :|: 0 >= 0
main_Store_247(i2, i4, i32, env, static) -{0,0}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0

obtained
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
by chaining
main_Store_270(i2, i4, i49, env, static) -{1,1}> main_JMP_273(i2, i4, i49, env, static) :|: 0 >= 0
main_JMP_273(i2, i4, i49, env, static) -{1,1}> main_Load_279(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_279(i2, i4, i49, env, static) -{1,1}> main_Load_287(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_287(i2, i4, i49, env, static) -{1,1}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0

obtained
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
by chaining
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_318(i2, i4, i49, env, static) :|: i49 < i2
main_LE_318(i2, i4, i49, env, static) -{1,1}> main_Load_336(i2, i4, i49, env, static) :|: i49 < i2
main_Load_336(i2, i4, i49, env, static) -{1,1}> main_ConstantStackPush_341(i2, i4, i49, env, static) :|: 0 >= 0
main_ConstantStackPush_341(i2, i4, i49, env, static) -{1,1}> main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) -{1,1}> main_InvokeMethod_366(i2, i4, i65, env, static) :|: iconst_1 = 1 && i49 + iconst_1 = i65
main_InvokeMethod_366(i2, i4, i65, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i65, env, static) :|: 0 >= 0

obtained
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i497
by chaining
round_NE_230(i45, i32, i2, i4, env, static) -{0,0}> round_NE_233(i45, i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1
round_NE_233(i45, i32, i2, i4, env, static) -{1,1}> round_Load_235(i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1 && !(i45 = 0)
round_Load_235(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_241(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_241(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) :|: iconst_1 = 1
round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) -{1,1}> round_Return_250(i49, i2, i4, env, static) :|: i32 + iconst_1 = i49 && iconst_1 = 1
round_Return_250(i49, i2, i4, env, static) -{1,1}> main_Store_270(i2, i4, i49, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && i41' <= 1 && i32 % 2 = i41' && -1 <= i41'
round_NE_230(0, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i497

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

Moved arithmethic from lhss to constraints.

round_NE_230(0, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1
was transformed to
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && i41' <= 1 && i32 % 2 = i41' && -1 <= i41'
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i497
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

(11) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && i41' <= 1 && i32 % 2 = i41' && -1 <= i41'
was transformed to
main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: i32 - 2 * div < 2 && i32 - 2 * div + 2 > 0 && 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> main_InvokeMethod_218'(i2, i4, i32, env, static) :|: 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'

round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i497
was transformed to
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497

(12) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: i32 - 2 * div < 2 && i32 - 2 * div + 2 > 0 && 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> main_InvokeMethod_218'(i2, i4, i32, env, static) :|: 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49

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

Moved arithmethic from constraints to rhss.

round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
was transformed to
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497

round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497
was transformed to
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497

main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
was transformed to
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2

main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
was transformed to
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i49 + 1, env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2

main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: i32 - 2 * div < 2 && i32 - 2 * div + 2 > 0 && 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
was transformed to
main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i32 - 2 * div, i32, i2, i4, env, static) :|: i32 - 2 * div < 2 && i32 - 2 * div + 2 > 0 && 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'

(14) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i49 + 1, env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i32 - 2 * div, i32, i2, i4, env, static) :|: i32 - 2 * div < 2 && i32 - 2 * div + 2 > 0 && 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> main_InvokeMethod_218'(i2, i4, i32, env, static) :|: 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i32 - 2 * div, i32, i2, i4, env, static) :|: i32 - 2 * div < 2 && i32 - 2 * div + 2 > 0 && 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
was transformed to
main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i32 + -2 * div, i32, i2, i4, env, static) :|: i32 + -2 * div < 2 && 0 < i32 + -2 * div + 2 && i41' <= 1 && i32 + -2 * div = i41' && -1 <= i41'

round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497
was transformed to
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: -1 <= i45 && i45 <= 1 && 0 < i45 && i32 + 1 = i497

round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
was transformed to
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497

main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
was transformed to
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i4 + 1, env, static) :|: i4 + 1 = i6' && i4 < i2

round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
was transformed to
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: x = 0

main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> main_InvokeMethod_218'(i2, i4, i32, env, static) :|: 0 >= 0 && i41' <= 1 && i32 - 2 * div = i41' && -1 <= i41'
was transformed to
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> main_InvokeMethod_218'(i2, i4, i32, env, static) :|: i41' <= 1 && i32 + -2 * div = i41' && -1 <= i41'

main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i49 + 1, env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
was transformed to
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i49 + 1, env, static) :|: i49 + 1 = i65' && i49 < i2

main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(16) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: x = 0
main_InvokeMethod_218'(i2, i4, i32, env, static) -{4,4}> round_NE_230(i32 + -2 * div, i32, i2, i4, env, static) :|: i32 + -2 * div < 2 && 0 < i32 + -2 * div + 2 && i41' <= 1 && i32 + -2 * div = i41' && -1 <= i41'
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i49 + 1, env, static) :|: i49 + 1 = i65' && i49 < i2
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i4 + 1, env, static) :|: i4 + 1 = i6' && i4 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: -1 <= i45 && i45 <= 1 && 0 < i45 && i32 + 1 = i497
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> main_InvokeMethod_218'(i2, i4, i32, env, static) :|: i41' <= 1 && i32 + -2 * div = i41' && -1 <= i41'
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49

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

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

(18) Obligation:

IntTrs with 58 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_Load_49(i2, i4, env, static) :|: 0 >= 0
main_Load_49(i2, i4, env, static) -{1,1}> main_LE_55(i2, i4, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_65(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_65(i2, i4, env, static) -{1,1}> main_IntArithmetic_66(i2, i4, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_66(i2, i4, iconst_1, env, static) -{1,1}> main_InvokeMethod_68(i2, i4, i6, env, static) :|: iconst_1 = 1 && i4 + iconst_1 = i6
main_InvokeMethod_68(i2, i4, i6, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i6, env, static) :|: 0 >= 0
main_InvokeMethod_218(i2, i4, i32, env, static) -{1,1}> round_Load_221(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_221(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_224(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_224(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) :|: iconst_2 = 2
round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) -{1,1}> round_NE_230(i41, i32, i2, i4, env, static) :|: -1 <= i41 && i41 <= 1 && iconst_2 = 2
round_NE_230(i45, i32, i2, i4, env, static) -{0,0}> round_NE_233(i45, i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1
round_NE_230(iconst_0, i32, i2, i4, env, static) -{0,0}> round_NE_234(iconst_0, i32, i2, i4, env, static) :|: -1 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
round_NE_233(i45, i32, i2, i4, env, static) -{1,1}> round_Load_235(i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1 && !(i45 = 0)
round_NE_234(iconst_0, i32, i2, i4, env, static) -{1,1}> round_Load_238(i32, i2, i4, env, static) :|: iconst_0 = 0
round_Load_235(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_241(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_238(i32, i2, i4, env, static) -{1,1}> round_Return_243(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_241(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) :|: iconst_1 = 1
round_Return_243(i32, i2, i4, env, static) -{1,1}> main_Store_247(i2, i4, i32, env, static) :|: 0 >= 0
round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) -{1,1}> round_Return_250(i49, i2, i4, env, static) :|: i32 + iconst_1 = i49 && iconst_1 = 1
main_Store_247(i2, i4, i32, env, static) -{0,0}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0
round_Return_250(i49, i2, i4, env, static) -{1,1}> main_Store_270(i2, i4, i49, env, static) :|: 0 >= 0
main_Store_270(i2, i4, i49, env, static) -{1,1}> main_JMP_273(i2, i4, i49, env, static) :|: 0 >= 0
main_JMP_273(i2, i4, i49, env, static) -{1,1}> main_Load_279(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_279(i2, i4, i49, env, static) -{1,1}> main_Load_287(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_287(i2, i4, i49, env, static) -{1,1}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_318(i2, i4, i49, env, static) :|: i49 < i2
main_LE_318(i2, i4, i49, env, static) -{1,1}> main_Load_336(i2, i4, i49, env, static) :|: i49 < i2
main_Load_336(i2, i4, i49, env, static) -{1,1}> main_ConstantStackPush_341(i2, i4, i49, env, static) :|: 0 >= 0
main_ConstantStackPush_341(i2, i4, i49, env, static) -{1,1}> main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) -{1,1}> main_InvokeMethod_366(i2, i4, i65, env, static) :|: iconst_1 = 1 && i49 + iconst_1 = i65
main_InvokeMethod_366(i2, i4, i65, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i65, env, static) :|: 0 >= 0

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

obtained
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
by chaining
main_InvokeMethod_218(i2, i4, i32, env, static) -{1,1}> round_Load_221(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_221(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_224(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_224(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) :|: iconst_2 = 2
round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) -{1,1}> round_NE_230(i41, i32, i2, i4, env, static) :|: -1 <= i41 && i41 <= 1 && iconst_2 = 2

(20) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
round_NE_230(0, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i497

(21) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

(22) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i497
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

(23) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

(24) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i6', env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i497, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i497
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i6' && i4 < i2
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i49 + 1, env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
was transformed to
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: -1 <= i41' && i41' <= 1

(28) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
round_NE_230(x, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: x = 0
main_Load_2(i2, i4, env, static) -{17,17}> main_LE_55(i2, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_Store_270(i2, i4, i49, env, static) -{4,4}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i49 + 1, env, static) :|: i49 + 1 = i65' && i49 < i2
main_LE_55(i2, i4, env, static) -{4,4}> main_InvokeMethod_218(i2, i4, i4 + 1, env, static) :|: i4 + 1 = i6' && i4 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: -1 <= i45 && i45 <= 1 && 0 < i45 && i32 + 1 = i497
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i32 + 1, env, static) :|: -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i497
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: -1 <= i41' && i41' <= 1
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_317(i2, i4, i49, env, static) :|: i2 <= i49

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) transformation)

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

(30) 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

(31) 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.

(32) Obligation:

IntTrs with 56 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_Load_49(i2, i4, env, static) :|: 0 >= 0
main_Load_49(i2, i4, env, static) -{1,1}> main_LE_55(i2, i4, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_65(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_65(i2, i4, env, static) -{1,1}> main_IntArithmetic_66(i2, i4, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_66(i2, i4, iconst_1, env, static) -{1,1}> main_InvokeMethod_68(i2, i4, i6, env, static) :|: iconst_1 = 1 && i4 + iconst_1 = i6
main_InvokeMethod_68(i2, i4, i6, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i6, env, static) :|: 0 >= 0
main_InvokeMethod_218(i2, i4, i32, env, static) -{1,1}> round_Load_221(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_221(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_224(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_224(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) :|: iconst_2 = 2
round_IntArithmetic_226(i32, iconst_2, i2, i4, env, static) -{1,1}> round_NE_230(i41, i32, i2, i4, env, static) :|: -1 <= i41 && i41 <= 1 && iconst_2 = 2
round_NE_230(i45, i32, i2, i4, env, static) -{0,0}> round_NE_233(i45, i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1
round_NE_230(iconst_0, i32, i2, i4, env, static) -{0,0}> round_NE_234(iconst_0, i32, i2, i4, env, static) :|: -1 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
round_NE_233(i45, i32, i2, i4, env, static) -{1,1}> round_Load_235(i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1 && !(i45 = 0)
round_NE_234(iconst_0, i32, i2, i4, env, static) -{1,1}> round_Load_238(i32, i2, i4, env, static) :|: iconst_0 = 0
round_Load_235(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_241(i32, i2, i4, env, static) :|: 0 >= 0
round_Load_238(i32, i2, i4, env, static) -{1,1}> round_Return_243(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_241(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) :|: iconst_1 = 1
round_Return_243(i32, i2, i4, env, static) -{1,1}> main_Store_247(i2, i4, i32, env, static) :|: 0 >= 0
round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) -{1,1}> round_Return_250(i49, i2, i4, env, static) :|: i32 + iconst_1 = i49 && iconst_1 = 1
main_Store_247(i2, i4, i32, env, static) -{0,0}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0
round_Return_250(i49, i2, i4, env, static) -{1,1}> main_Store_270(i2, i4, i49, env, static) :|: 0 >= 0
main_Store_270(i2, i4, i49, env, static) -{1,1}> main_JMP_273(i2, i4, i49, env, static) :|: 0 >= 0
main_JMP_273(i2, i4, i49, env, static) -{1,1}> main_Load_279(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_279(i2, i4, i49, env, static) -{1,1}> main_Load_287(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_287(i2, i4, i49, env, static) -{1,1}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_318(i2, i4, i49, env, static) :|: i49 < i2
main_LE_318(i2, i4, i49, env, static) -{1,1}> main_Load_336(i2, i4, i49, env, static) :|: i49 < i2
main_Load_336(i2, i4, i49, env, static) -{1,1}> main_ConstantStackPush_341(i2, i4, i49, env, static) :|: 0 >= 0
main_ConstantStackPush_341(i2, i4, i49, env, static) -{1,1}> main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) -{1,1}> main_InvokeMethod_366(i2, i4, i65, env, static) :|: iconst_1 = 1 && i49 + iconst_1 = i65
main_InvokeMethod_366(i2, i4, i65, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i65, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, i4, env, static) -{21,21}> main_InvokeMethod_218(i2, i4, i6', env, static'1) :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
by chaining
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_Load_49(i2, i4, env, static) :|: 0 >= 0
main_Load_49(i2, i4, env, static) -{1,1}> main_LE_55(i2, i4, env, static) :|: 0 >= 0
main_LE_55(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_65(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_65(i2, i4, env, static) -{1,1}> main_IntArithmetic_66(i2, i4, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_66(i2, i4, iconst_1, env, static) -{1,1}> main_InvokeMethod_68(i2, i4, i6, env, static) :|: iconst_1 = 1 && i4 + iconst_1 = i6
main_InvokeMethod_68(i2, i4, i6, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i6, env, static) :|: 0 >= 0

obtained
main_Store_270(i2, i4, i49, env, static) -{8,8}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
by chaining
main_Store_270(i2, i4, i49, env, static) -{1,1}> main_JMP_273(i2, i4, i49, env, static) :|: 0 >= 0
main_JMP_273(i2, i4, i49, env, static) -{1,1}> main_Load_279(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_279(i2, i4, i49, env, static) -{1,1}> main_Load_287(i2, i4, i49, env, static) :|: 0 >= 0
main_Load_287(i2, i4, i49, env, static) -{1,1}> main_LE_310(i2, i4, i49, env, static) :|: 0 >= 0
main_LE_310(i2, i4, i49, env, static) -{0,0}> main_LE_318(i2, i4, i49, env, static) :|: i49 < i2
main_LE_318(i2, i4, i49, env, static) -{1,1}> main_Load_336(i2, i4, i49, env, static) :|: i49 < i2
main_Load_336(i2, i4, i49, env, static) -{1,1}> main_ConstantStackPush_341(i2, i4, i49, env, static) :|: 0 >= 0
main_ConstantStackPush_341(i2, i4, i49, env, static) -{1,1}> main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_356(i2, i4, i49, iconst_1, env, static) -{1,1}> main_InvokeMethod_366(i2, i4, i65, env, static) :|: iconst_1 = 1 && i49 + iconst_1 = i65
main_InvokeMethod_366(i2, i4, i65, env, static) -{0,0}> main_InvokeMethod_218(i2, i4, i65, env, static) :|: 0 >= 0

obtained
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i498, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i498
by chaining
round_NE_230(i45, i32, i2, i4, env, static) -{0,0}> round_NE_233(i45, i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1
round_NE_233(i45, i32, i2, i4, env, static) -{1,1}> round_Load_235(i32, i2, i4, env, static) :|: -1 <= i45 && i45 <= 1 && !(i45 = 0)
round_Load_235(i32, i2, i4, env, static) -{1,1}> round_ConstantStackPush_241(i32, i2, i4, env, static) :|: 0 >= 0
round_ConstantStackPush_241(i32, i2, i4, env, static) -{1,1}> round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) :|: iconst_1 = 1
round_IntArithmetic_245(i32, iconst_1, i2, i4, env, static) -{1,1}> round_Return_250(i49, i2, i4, env, static) :|: i32 + iconst_1 = i49 && iconst_1 = 1
round_Return_250(i49, i2, i4, env, static) -{1,1}> main_Store_270(i2, i4, i49, env, static) :|: 0 >= 0

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, env, static) -{21,21}> main_InvokeMethod_218(i2, i4, i6', env, static'1) :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
main_InvokeMethod_218(i2, i4, i32, env, static) -{4,4}> round_NE_230(i41', i32, i2, i4, env, static) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
round_NE_230(0, i32, i2, i4, env, static) -{3,3}> main_Store_270(i2, i4, i32, env, static) :|: 0 >= 0 && -1 <= 0 && 0 <= 1
main_Store_270(i2, i4, i49, env, static) -{8,8}> main_InvokeMethod_218(i2, i4, i65', env, static) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
round_NE_230(i45, i32, i2, i4, env, static) -{5,5}> main_Store_270(i2, i4, i498, env, static) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i498

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

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

main_Load_2(x1, x2, x3, x4) → main_Load_2(x1, x2, x4)
round_NE_230(x1, x2, x3, x4, x5, x6) → round_NE_230(x1, x2, x3)
main_Store_270(x1, x2, x3, x4, x5) → main_Store_270(x1, x3)
main_InvokeMethod_218(x1, x2, x3, x4, x5) → main_InvokeMethod_218(x1, x3)

(36) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i6') :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
main_InvokeMethod_218(i2, i32) -{4,4}> round_NE_230(i41', i32, i2) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
round_NE_230(0, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: 0 >= 0 && -1 <= 0 && 0 <= 1
main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i65') :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i498

(37) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

round_NE_230(0, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: 0 >= 0 && -1 <= 0 && 0 <= 1
was transformed to
round_NE_230(x, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0

(38) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
round_NE_230(x, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
main_InvokeMethod_218(i2, i32) -{4,4}> round_NE_230(i41', i32, i2) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i65') :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i6') :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i498

(39) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && !(i45 = 0) && i32 + 1 = i498
was transformed to
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i498
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498

(40) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_InvokeMethod_218(i2, i32) -{4,4}> round_NE_230(i41', i32, i2) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i498
main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i6') :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i65') :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
round_NE_230(x, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498

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

Moved arithmethic from constraints to rhss.

round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i498
was transformed to
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i498

main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i65') :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
was transformed to
main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i49 + 1) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2

main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i6') :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
was transformed to
main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i4 + 1) :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'

round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i498) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498
was transformed to
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498

(42) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i498
main_InvokeMethod_218(i2, i32) -{4,4}> round_NE_230(i41', i32, i2) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i49 + 1) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i4 + 1) :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
round_NE_230(x, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498

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

Simplified expressions.

main_InvokeMethod_218(i2, i32) -{4,4}> round_NE_230(i41', i32, i2) :|: 0 >= 0 && -1 <= i41' && i41' <= 1
was transformed to
main_InvokeMethod_218(i2, i32) -{4,4}> round_NE_230(i41', i32, i2) :|: -1 <= i41' && i41' <= 1

round_NE_230(x, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: 0 >= 0 && -1 <= 0 && 0 <= 1 && x = 0
was transformed to
round_NE_230(x, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: x = 0

main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i49 + 1) :|: 0 >= 0 && i49 + 1 = i65' && i49 < i2
was transformed to
main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i49 + 1) :|: i49 + 1 = i65' && i49 < i2

round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498
was transformed to
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498

round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: 0 >= 0 && -1 <= i45 && i45 <= 1 && i45 > 0 && i32 + 1 = i498
was transformed to
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: -1 <= i45 && i45 <= 1 && 0 < i45 && i32 + 1 = i498

main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i4 + 1) :|: 0 >= 0 && i4 < i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && i4 + 1 = i6'
was transformed to
main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i4 + 1) :|: i4 < i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i4 + 1 = i6'

(44) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_InvokeMethod_218(i2, i32) -{4,4}> round_NE_230(i41', i32, i2) :|: -1 <= i41' && i41' <= 1
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: -1 <= i45 && i45 <= 1 && i45 < 0 && i32 + 1 = i498
round_NE_230(i45, i32, i2) -{5,5}> main_Store_270(i2, i32 + 1) :|: -1 <= i45 && i45 <= 1 && 0 < i45 && i32 + 1 = i498
main_Store_270(i2, i49) -{8,8}> main_InvokeMethod_218(i2, i49 + 1) :|: i49 + 1 = i65' && i49 < i2
round_NE_230(x, i32, i2) -{3,3}> main_Store_270(i2, i32) :|: x = 0
main_Load_2(i2, i4, static) -{21,21}> main_InvokeMethod_218(i2, i4 + 1) :|: i4 < i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i4 + 1 = i6'

(45) koat Proof (EQUIVALENT transformation)

YES(?, 25*ar_0 + 25*ar_1 + 63)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 4) main_InvokeMethod_218(ar_0, ar_1, ar_2) -> Com_1(round_NE_230(i41', ar_1, ar_0)) [ -1 <= i41' /\ i41' <= 1 ]
(Comp: ?, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ ar_0 < 0 /\ ar_1 + 1 = i498 ]
(Comp: ?, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ 0 < ar_0 /\ ar_1 + 1 = i498 ]
(Comp: ?, Cost: 8) main_Store_270(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i65' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1, arityPad)) [ ar_0 = 0 ]
(Comp: ?, Cost: 21) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_1 + 1 = i6' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_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: ?, Cost: 4) main_InvokeMethod_218(ar_0, ar_1, ar_2) -> Com_1(round_NE_230(i41', ar_1, ar_0)) [ -1 <= i41' /\ i41' <= 1 ]
(Comp: ?, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ ar_0 < 0 /\ ar_1 + 1 = i498 ]
(Comp: ?, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ 0 < ar_0 /\ ar_1 + 1 = i498 ]
(Comp: ?, Cost: 8) main_Store_270(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i65' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1, arityPad)) [ ar_0 = 0 ]
(Comp: 1, Cost: 21) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_1 + 1 = i6' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_InvokeMethod_218) = V_1 - V_2
Pol(round_NE_230) = -V_2 + V_3
Pol(main_Store_270) = V_1 - V_2
Pol(main_Load_2) = V_1 - V_2 - 1
Pol(koat_start) = V_1 - V_2 - 1
orients all transitions weakly and the transition
main_Store_270(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i65' /\ ar_1 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 4) main_InvokeMethod_218(ar_0, ar_1, ar_2) -> Com_1(round_NE_230(i41', ar_1, ar_0)) [ -1 <= i41' /\ i41' <= 1 ]
(Comp: ?, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ ar_0 < 0 /\ ar_1 + 1 = i498 ]
(Comp: ?, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ 0 < ar_0 /\ ar_1 + 1 = i498 ]
(Comp: ar_0 + ar_1 + 1, Cost: 8) main_Store_270(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i65' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1, arityPad)) [ ar_0 = 0 ]
(Comp: 1, Cost: 21) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_1 + 1 = i6' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4: T:
(Comp: ar_0 + ar_1 + 2, Cost: 4) main_InvokeMethod_218(ar_0, ar_1, ar_2) -> Com_1(round_NE_230(i41', ar_1, ar_0)) [ -1 <= i41' /\ i41' <= 1 ]
(Comp: ar_0 + ar_1 + 2, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ ar_0 < 0 /\ ar_1 + 1 = i498 ]
(Comp: ar_0 + ar_1 + 2, Cost: 5) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1 + 1, arityPad)) [ -1 <= ar_0 /\ ar_0 <= 1 /\ 0 < ar_0 /\ ar_1 + 1 = i498 ]
(Comp: ar_0 + ar_1 + 1, Cost: 8) main_Store_270(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i65' /\ ar_1 < ar_0 ]
(Comp: ar_0 + ar_1 + 2, Cost: 3) round_NE_230(ar_0, ar_1, ar_2) -> Com_1(main_Store_270(ar_2, ar_1, arityPad)) [ ar_0 = 0 ]
(Comp: 1, Cost: 21) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_InvokeMethod_218(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_1 + 1 = i6' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 25*ar_0 + 25*ar_1 + 63

Time: 0.175 sec (SMT: 0.165 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

(11) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

(21) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) transformation)

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

(37) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(38) Obligation:

(39) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

(40) Obligation:

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

(42) Obligation:

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

(44) Obligation:

(45) koat Proof (EQUIVALENT transformation)

(46) BOUNDS(CONSTANT, 63 + 25 * |#0| + 25 * |#1|)