time complexity proof of /tmp/tmpoF23pk/Sequence.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 12 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 25 ms)

    ↳10 WeightedIntTrs

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

    ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

    ↳15 koat Proof (⇔, 94 ms)

    ↳16 BOUNDS(CONSTANT, 612)

↳17 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 4 ms)

↳18 JBCComplexityEdges

    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 45 ms)

    ↳20 WeightedIntTrs

        ↳21 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 13 ms)

        ↳22 WeightedIntTrs

        ↳23 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 57 ms)

    ↳30 WeightedIntTrs

        ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 2 ms)

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

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

        ↳36 WeightedIntTrs

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

        ↳38 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class Sequence {
    public static void main() {
	for (int i = 0; i < 100; i++) {};

	for (int j = 5; j < 21; j += 3) {};
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Sequence.main()V: Graph of 55 nodes with 2 SCCs.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 53 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_3(env, static) :|: 0 >= 0
main_ConstantStackPush_3(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_19(env, static) :|: 0 <= static
langle_clinit_rangle_New_19(env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_27(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_41(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(iconst_0, env, static) -{1,1}> main_GE_56(iconst_0, iconst_100, env, static) :|: iconst_100 = 100 && iconst_0 = 0
main_GE_56(iconst_0, iconst_100, env, static) -{1,1}> main_Inc_57(iconst_0, env, static) :|: iconst_100 = 100 && iconst_0 = 0
main_Inc_57(iconst_0, env, static) -{1,1}> main_JMP_59(iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_59(iconst_1, env, static) -{1,1}> main_Load_63(iconst_1, env, static) :|: iconst_1 = 1
main_Load_63(iconst_1, env, static) -{0,0}> main_Load_85(iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_85(i2, env, static) -{0,0}> main_Load_111(i2, env, static) :|: 1 <= i2 && i2 <= 3 && i2 <= 2
main_Load_111(i5, env, static) -{0,0}> main_Load_137(i5, env, static) :|: i5 <= 3 && 1 <= i5
main_Load_137(i10, env, static) -{1,1}> main_ConstantStackPush_139(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_139(i10, env, static) -{1,1}> main_GE_148(i10, iconst_100, env, static) :|: 1 <= i10 && iconst_100 = 100
main_GE_148(i16, iconst_100, env, static) -{0,0}> main_GE_150(i16, iconst_100, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99
main_GE_148(i17, iconst_100, env, static) -{0,0}> main_GE_151(i17, iconst_100, env, static) :|: iconst_100 = 100 && 1 <= i17 && 100 <= i17
main_GE_150(i16, iconst_100, env, static) -{1,1}> main_Inc_157(i16, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && i16 < iconst_100
main_GE_151(i17, iconst_100, env, static) -{1,1}> main_ConstantStackPush_158(env, static) :|: iconst_100 <= i17 && iconst_100 = 100 && 100 <= i17
main_Inc_157(i16, env, static) -{1,1}> main_JMP_161(i18, env, static) :|: i16 + 1 = i18 && 1 <= i16 && i16 <= 99 && 2 <= i18 && i18 <= 100
main_ConstantStackPush_158(env, static) -{1,1}> main_Store_162(iconst_5, env, static) :|: iconst_5 = 5
main_JMP_161(i18, env, static) -{1,1}> main_Load_166(i18, env, static) :|: 2 <= i18 && i18 <= 100
main_Store_162(iconst_5, env, static) -{1,1}> main_Load_167(iconst_5, env, static) :|: iconst_5 = 5
main_Load_166(i18, env, static) -{0,0}> main_Load_137(i18, env, static) :|: 1 <= i18 && 2 <= i18 && i18 <= 100
main_Load_167(iconst_5, env, static) -{0,0}> main_Load_222(iconst_5, env, static) :|: iconst_5 = 5 && iconst_5 <= 14 && 5 <= iconst_5
main_Load_222(i24, env, static) -{0,0}> main_Load_235(i24, env, static) :|: 5 <= i24 && i24 <= 14
main_Load_235(i29, env, static) -{1,1}> main_ConstantStackPush_236(i29, env, static) :|: 0 >= 0
main_ConstantStackPush_236(i29, env, static) -{1,1}> main_GE_242(i29, iconst_21, env, static) :|: iconst_21 = 21
main_GE_242(i35, iconst_21, env, static) -{0,0}> main_GE_243(i35, iconst_21, env, static) :|: iconst_21 = 21 && i35 <= 20
main_GE_243(i35, iconst_21, env, static) -{1,1}> main_Inc_250(i35, env, static) :|: iconst_21 = 21 && i35 <= 20 && i35 < iconst_21
main_Inc_250(i35, env, static) -{1,1}> main_JMP_252(i37, env, static) :|: i35 + 3 = i37 && i35 <= 20 && i37 <= 23
main_JMP_252(i37, env, static) -{1,1}> main_Load_256(i37, env, static) :|: i37 <= 23
main_Load_256(i37, env, static) -{0,0}> main_Load_235(i37, env, static) :|: i37 <= 23

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

obtained
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2
by chaining
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_3(env, static) :|: 0 >= 0
main_ConstantStackPush_3(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_19(env, static) :|: 0 <= static
langle_clinit_rangle_New_19(env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_27(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_41(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(iconst_0, env, static) -{1,1}> main_GE_56(iconst_0, iconst_100, env, static) :|: iconst_100 = 100 && iconst_0 = 0
main_GE_56(iconst_0, iconst_100, env, static) -{1,1}> main_Inc_57(iconst_0, env, static) :|: iconst_100 = 100 && iconst_0 = 0
main_Inc_57(iconst_0, env, static) -{1,1}> main_JMP_59(iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_59(iconst_1, env, static) -{1,1}> main_Load_63(iconst_1, env, static) :|: iconst_1 = 1
main_Load_63(iconst_1, env, static) -{0,0}> main_Load_85(iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_85(i2, env, static) -{0,0}> main_Load_111(i2, env, static) :|: 1 <= i2 && i2 <= 3 && i2 <= 2
main_Load_111(i5, env, static) -{0,0}> main_Load_137(i5, env, static) :|: i5 <= 3 && 1 <= i5

obtained
main_Load_137(i10, env, static) -{2,2}> main_GE_148(i10, 100, env, static) :|: 1 <= i10
by chaining
main_Load_137(i10, env, static) -{1,1}> main_ConstantStackPush_139(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_139(i10, env, static) -{1,1}> main_GE_148(i10, iconst_100, env, static) :|: 1 <= i10 && iconst_100 = 100

obtained
main_GE_148(i17, 100, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17
by chaining
main_GE_148(i17, iconst_100, env, static) -{0,0}> main_GE_151(i17, iconst_100, env, static) :|: iconst_100 = 100 && 1 <= i17 && 100 <= i17
main_GE_151(i17, iconst_100, env, static) -{1,1}> main_ConstantStackPush_158(env, static) :|: iconst_100 <= i17 && iconst_100 = 100 && 100 <= i17
main_ConstantStackPush_158(env, static) -{1,1}> main_Store_162(iconst_5, env, static) :|: iconst_5 = 5
main_Store_162(iconst_5, env, static) -{1,1}> main_Load_167(iconst_5, env, static) :|: iconst_5 = 5
main_Load_167(iconst_5, env, static) -{0,0}> main_Load_222(iconst_5, env, static) :|: iconst_5 = 5 && iconst_5 <= 14 && 5 <= iconst_5
main_Load_222(i24, env, static) -{0,0}> main_Load_235(i24, env, static) :|: 5 <= i24 && i24 <= 14

obtained
main_Load_235(i29, env, static) -{5,5}> main_Load_235(i37', env, static) :|: i37' <= 23 && i29 < 21 && 0 >= 0 && i29 <= 20 && i29 + 3 = i37'
by chaining
main_Load_235(i29, env, static) -{1,1}> main_ConstantStackPush_236(i29, env, static) :|: 0 >= 0
main_ConstantStackPush_236(i29, env, static) -{1,1}> main_GE_242(i29, iconst_21, env, static) :|: iconst_21 = 21
main_GE_242(i35, iconst_21, env, static) -{0,0}> main_GE_243(i35, iconst_21, env, static) :|: iconst_21 = 21 && i35 <= 20
main_GE_243(i35, iconst_21, env, static) -{1,1}> main_Inc_250(i35, env, static) :|: iconst_21 = 21 && i35 <= 20 && i35 < iconst_21
main_Inc_250(i35, env, static) -{1,1}> main_JMP_252(i37, env, static) :|: i35 + 3 = i37 && i35 <= 20 && i37 <= 23
main_JMP_252(i37, env, static) -{1,1}> main_Load_256(i37, env, static) :|: i37 <= 23
main_Load_256(i37, env, static) -{0,0}> main_Load_235(i37, env, static) :|: i37 <= 23

obtained
main_GE_148(i16, 100, env, static) -{3,3}> main_Load_137(i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'
by chaining
main_GE_148(i16, iconst_100, env, static) -{0,0}> main_GE_150(i16, iconst_100, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99
main_GE_150(i16, iconst_100, env, static) -{1,1}> main_Inc_157(i16, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && i16 < iconst_100
main_Inc_157(i16, env, static) -{1,1}> main_JMP_161(i18, env, static) :|: i16 + 1 = i18 && 1 <= i16 && i16 <= 99 && 2 <= i18 && i18 <= 100
main_JMP_161(i18, env, static) -{1,1}> main_Load_166(i18, env, static) :|: 2 <= i18 && i18 <= 100
main_Load_166(i18, env, static) -{0,0}> main_Load_137(i18, env, static) :|: 1 <= i18 && 2 <= i18 && i18 <= 100

(8) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2
main_Load_137(i10, env, static) -{2,2}> main_GE_148(i10, 100, env, static) :|: 1 <= i10
main_GE_148(i17, 100, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17
main_Load_235(i29, env, static) -{5,5}> main_Load_235(i37', env, static) :|: i37' <= 23 && i29 < 21 && 0 >= 0 && i29 <= 20 && i29 + 3 = i37'
main_GE_148(i16, 100, env, static) -{3,3}> main_Load_137(i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'

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

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

main_ConstantStackPush_2(x1, x2) → main_ConstantStackPush_2(x2)
main_Load_137(x1, x2, x3) → main_Load_137(x1)
main_GE_148(x1, x2, x3, x4) → main_GE_148(x1)
main_Load_235(x1, x2, x3) → main_Load_235(x1)

(10) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_2(static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(static) -{22,22}> main_Load_137(1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2
main_Load_137(i10) -{2,2}> main_GE_148(i10) :|: 1 <= i10
main_GE_148(i17) -{3,3}> main_Load_235(5) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17
main_Load_235(i29) -{5,5}> main_Load_235(i37') :|: i37' <= 23 && i29 < 21 && 0 >= 0 && i29 <= 20 && i29 + 3 = i37'
main_GE_148(i16) -{3,3}> main_Load_137(i18') :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'

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

Moved arithmethic from constraints to rhss.

main_Load_235(i29) -{5,5}> main_Load_235(i37') :|: i37' <= 23 && i29 < 21 && 0 >= 0 && i29 <= 20 && i29 + 3 = i37'
was transformed to
main_Load_235(i29) -{5,5}> main_Load_235(i29 + 3) :|: i37' <= 23 && i29 < 21 && 0 >= 0 && i29 <= 20 && i29 + 3 = i37'

main_GE_148(i16) -{3,3}> main_Load_137(i18') :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'
was transformed to
main_GE_148(i16) -{3,3}> main_Load_137(i16 + 1) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'

(12) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_2(static)
Considered paths: all paths from start
Rules:
main_GE_148(i17) -{3,3}> main_Load_235(5) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17
main_Load_235(i29) -{5,5}> main_Load_235(i29 + 3) :|: i37' <= 23 && i29 < 21 && 0 >= 0 && i29 <= 20 && i29 + 3 = i37'
main_GE_148(i16) -{3,3}> main_Load_137(i16 + 1) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'
main_Load_137(i10) -{2,2}> main_GE_148(i10) :|: 1 <= i10
main_ConstantStackPush_2(static) -{22,22}> main_Load_137(1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2

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

Simplified expressions.

main_GE_148(i17) -{3,3}> main_Load_235(5) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17
was transformed to
main_GE_148(i17) -{3,3}> main_Load_235(5) :|: 100 <= i17 && 1 <= i17

main_Load_235(i29) -{5,5}> main_Load_235(i29 + 3) :|: i37' <= 23 && i29 < 21 && 0 >= 0 && i29 <= 20 && i29 + 3 = i37'
was transformed to
main_Load_235(i29) -{5,5}> main_Load_235(i29 + 3) :|: i37' <= 23 && i29 < 21 && i29 <= 20 && i29 + 3 = i37'

main_ConstantStackPush_2(static) -{22,22}> main_Load_137(1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2
was transformed to
main_ConstantStackPush_2(static) -{22,22}> main_Load_137(1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(14) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_2(static)
Considered paths: all paths from start
Rules:
main_Load_235(i29) -{5,5}> main_Load_235(i29 + 3) :|: i37' <= 23 && i29 < 21 && i29 <= 20 && i29 + 3 = i37'
main_ConstantStackPush_2(static) -{22,22}> main_Load_137(1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GE_148(i17) -{3,3}> main_Load_235(5) :|: 100 <= i17 && 1 <= i17
main_Load_137(i10) -{2,2}> main_GE_148(i10) :|: 1 <= i10
main_GE_148(i16) -{3,3}> main_Load_137(i16 + 1) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'

(15) koat Proof (EQUIVALENT transformation)

YES(?, 612)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 5) main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\ ar_0 < 21 /\ ar_0 <= 20 /\ ar_0 + 3 = i37' ]
(Comp: ?, Cost: 22) main_ConstantStackPush_2(ar_0) -> Com_1(main_Load_137(1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]
(Comp: ?, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_ConstantStackPush_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 5) main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\ ar_0 < 21 /\ ar_0 <= 20 /\ ar_0 + 3 = i37' ]
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0) -> Com_1(main_Load_137(1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]
(Comp: ?, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_ConstantStackPush_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_235) = 0
Pol(main_ConstantStackPush_2) = 1
Pol(main_Load_137) = 1
Pol(main_GE_148) = 1
Pol(koat_start) = 1
orients all transitions weakly and the transition
main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\ 1 <= ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 5) main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\ ar_0 < 21 /\ ar_0 <= 20 /\ ar_0 + 3 = i37' ]
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0) -> Com_1(main_Load_137(1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]
(Comp: ?, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_ConstantStackPush_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_235) = -V_1 + 21
Pol(main_ConstantStackPush_2) = 16
Pol(main_Load_137) = 16
Pol(main_GE_148) = 16
Pol(koat_start) = 16
orients all transitions weakly and the transition
main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\ ar_0 < 21 /\ ar_0 <= 20 /\ ar_0 + 3 = i37' ]
strictly and produces the following problem:
4: T:
(Comp: 16, Cost: 5) main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\ ar_0 < 21 /\ ar_0 <= 20 /\ ar_0 + 3 = i37' ]
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0) -> Com_1(main_Load_137(1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]
(Comp: ?, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_ConstantStackPush_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_137) = -V_1 + 100
Pol(main_GE_148) = -V_1 + 100
and size complexities
S("koat_start(ar_0) -> Com_1(main_ConstantStackPush_2(ar_0)) [ 0 <= 0 ]", 0-0) = ar_0
S("main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\\ i18' <= 100 /\\ ar_0 <= 99 /\\ 1 <= i18' /\\ 2 <= i18' /\\ ar_0 < 100 /\\ ar_0 + 1 = i18' ]", 0-0) = 100
S("main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]", 0-0) = 100
S("main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\\ 1 <= ar_0 ]", 0-0) = 5
S("main_ConstantStackPush_2(ar_0) -> Com_1(main_Load_137(1)) [ 0 <= static'1 /\\ 0 <= ar_0 /\\ static''' <= ar_0 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-0) = 1
S("main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\\ ar_0 < 21 /\\ ar_0 <= 20 /\\ ar_0 + 3 = i37' ]", 0-0) = 23
orients the transitions
main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]
main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
weakly and the transition
main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
strictly and produces the following problem:
5: T:
(Comp: 16, Cost: 5) main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\ ar_0 < 21 /\ ar_0 <= 20 /\ ar_0 + 3 = i37' ]
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0) -> Com_1(main_Load_137(1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]
(Comp: 101, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_ConstantStackPush_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 5 produces the following problem:
6: T:
(Comp: 16, Cost: 5) main_Load_235(ar_0) -> Com_1(main_Load_235(ar_0 + 3)) [ i37' <= 23 /\ ar_0 < 21 /\ ar_0 <= 20 /\ ar_0 + 3 = i37' ]
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0) -> Com_1(main_Load_137(1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_235(5)) [ 100 <= ar_0 /\ 1 <= ar_0 ]
(Comp: 102, Cost: 2) main_Load_137(ar_0) -> Com_1(main_GE_148(ar_0)) [ 1 <= ar_0 ]
(Comp: 101, Cost: 3) main_GE_148(ar_0) -> Com_1(main_Load_137(ar_0 + 1)) [ 1 <= ar_0 /\ i18' <= 100 /\ ar_0 <= 99 /\ 1 <= i18' /\ 2 <= i18' /\ ar_0 < 100 /\ ar_0 + 1 = i18' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_ConstantStackPush_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 612

Time: 0.121 sec (SMT: 0.108 sec)

(16) BOUNDS(CONSTANT, 612)

(17) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)

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

(18) Obligation:

Set of 54 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

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

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

(20) Obligation:

IntTrs with 54 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_3(env, static) :|: 0 >= 0
main_ConstantStackPush_3(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_19(env, static) :|: 0 <= static
langle_clinit_rangle_New_19(env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_27(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_41(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(iconst_0, env, static) -{1,1}> main_GE_56(iconst_0, iconst_100, env, static) :|: iconst_100 = 100 && iconst_0 = 0
main_GE_56(iconst_0, iconst_100, env, static) -{1,1}> main_Inc_57(iconst_0, env, static) :|: iconst_100 = 100 && iconst_0 = 0
main_Inc_57(iconst_0, env, static) -{1,1}> main_JMP_59(iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_59(iconst_1, env, static) -{1,1}> main_Load_63(iconst_1, env, static) :|: iconst_1 = 1
main_Load_63(iconst_1, env, static) -{0,0}> main_Load_85(iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_85(i2, env, static) -{0,0}> main_Load_111(i2, env, static) :|: 1 <= i2 && i2 <= 3 && i2 <= 2
main_Load_111(i5, env, static) -{0,0}> main_Load_137(i5, env, static) :|: i5 <= 3 && 1 <= i5
main_Load_137(i10, env, static) -{1,1}> main_ConstantStackPush_139(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_139(i10, env, static) -{1,1}> main_GE_148(i10, iconst_100, env, static) :|: 1 <= i10 && iconst_100 = 100
main_GE_148(i16, iconst_100, env, static) -{0,0}> main_GE_150(i16, iconst_100, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99
main_GE_148(i17, iconst_100, env, static) -{0,0}> main_GE_151(i17, iconst_100, env, static) :|: iconst_100 = 100 && 1 <= i17 && 100 <= i17
main_GE_150(i16, iconst_100, env, static) -{1,1}> main_Inc_157(i16, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && i16 < iconst_100
main_GE_151(i17, iconst_100, env, static) -{1,1}> main_ConstantStackPush_158(env, static) :|: iconst_100 <= i17 && iconst_100 = 100 && 100 <= i17
main_Inc_157(i16, env, static) -{1,1}> main_JMP_161(i18, env, static) :|: i16 + 1 = i18 && 1 <= i16 && i16 <= 99 && 2 <= i18 && i18 <= 100
main_ConstantStackPush_158(env, static) -{1,1}> main_Store_162(iconst_5, env, static) :|: iconst_5 = 5
main_JMP_161(i18, env, static) -{1,1}> main_Load_166(i18, env, static) :|: 2 <= i18 && i18 <= 100
main_Store_162(iconst_5, env, static) -{1,1}> main_Load_167(iconst_5, env, static) :|: iconst_5 = 5
main_Load_166(i18, env, static) -{0,0}> main_Load_137(i18, env, static) :|: 1 <= i18 && 2 <= i18 && i18 <= 100
main_Load_167(iconst_5, env, static) -{0,0}> main_Load_222(iconst_5, env, static) :|: iconst_5 = 5 && iconst_5 <= 14 && 5 <= iconst_5
main_Load_222(i24, env, static) -{0,0}> main_Load_235(i24, env, static) :|: 5 <= i24 && i24 <= 14
main_Load_235(i29, env, static) -{1,1}> main_ConstantStackPush_236(i29, env, static) :|: 0 >= 0
main_ConstantStackPush_236(i29, env, static) -{1,1}> main_GE_242(i29, iconst_21, env, static) :|: iconst_21 = 21
main_GE_242(i35, iconst_21, env, static) -{0,0}> main_GE_243(i35, iconst_21, env, static) :|: iconst_21 = 21 && i35 <= 20
main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, iconst_21, env, static) :|: iconst_21 = 21 && 21 <= i36
main_GE_243(i35, iconst_21, env, static) -{1,1}> main_Inc_250(i35, env, static) :|: iconst_21 = 21 && i35 <= 20 && i35 < iconst_21
main_Inc_250(i35, env, static) -{1,1}> main_JMP_252(i37, env, static) :|: i35 + 3 = i37 && i35 <= 20 && i37 <= 23
main_JMP_252(i37, env, static) -{1,1}> main_Load_256(i37, env, static) :|: i37 <= 23
main_Load_256(i37, env, static) -{0,0}> main_Load_235(i37, env, static) :|: i37 <= 23

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

obtained
main_Load_235(i29, env, static) -{2,2}> main_GE_242(i29, 21, env, static) :|: 0 >= 0
by chaining
main_Load_235(i29, env, static) -{1,1}> main_ConstantStackPush_236(i29, env, static) :|: 0 >= 0
main_ConstantStackPush_236(i29, env, static) -{1,1}> main_GE_242(i29, iconst_21, env, static) :|: iconst_21 = 21

obtained
main_GE_242(i35, 21, env, static) -{3,3}> main_Load_235(i37', env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37'
by chaining
main_GE_242(i35, iconst_21, env, static) -{0,0}> main_GE_243(i35, iconst_21, env, static) :|: iconst_21 = 21 && i35 <= 20
main_GE_243(i35, iconst_21, env, static) -{1,1}> main_Inc_250(i35, env, static) :|: iconst_21 = 21 && i35 <= 20 && i35 < iconst_21
main_Inc_250(i35, env, static) -{1,1}> main_JMP_252(i37, env, static) :|: i35 + 3 = i37 && i35 <= 20 && i37 <= 23
main_JMP_252(i37, env, static) -{1,1}> main_Load_256(i37, env, static) :|: i37 <= 23
main_Load_256(i37, env, static) -{0,0}> main_Load_235(i37, env, static) :|: i37 <= 23

(22) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2
main_Load_137(i10, env, static) -{2,2}> main_GE_148(i10, 100, env, static) :|: 1 <= i10
main_GE_148(i17, 100, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17
main_Load_235(i29, env, static) -{2,2}> main_GE_242(i29, 21, env, static) :|: 0 >= 0
main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, iconst_21, env, static) :|: iconst_21 = 21 && 21 <= i36
main_GE_242(i35, 21, env, static) -{3,3}> main_Load_235(i37', env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37'
main_GE_148(i16, 100, env, static) -{3,3}> main_Load_137(i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'

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

Moved arithmethic from lhss to constraints.

main_GE_242(i35, 21, env, static) -{3,3}> main_Load_235(i37', env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37'
was transformed to
main_GE_242(i35, x, env, static) -{3,3}> main_Load_235(i37', env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37' && x = 21

main_GE_148(i16, 100, env, static) -{3,3}> main_Load_137(i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18'
was transformed to
main_GE_148(i16, x, env, static) -{3,3}> main_Load_137(i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18' && x = 100

main_GE_148(i17, 100, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17
was transformed to
main_GE_148(i17, x, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17 && x = 100

(24) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_137(i10, env, static) -{2,2}> main_GE_148(i10, 100, env, static) :|: 1 <= i10
main_GE_242(i35, x, env, static) -{3,3}> main_Load_235(i37', env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37' && x = 21
main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, iconst_21, env, static) :|: iconst_21 = 21 && 21 <= i36
main_GE_148(i16, x, env, static) -{3,3}> main_Load_137(i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18' && x = 100
main_Load_235(i29, env, static) -{2,2}> main_GE_242(i29, 21, env, static) :|: 0 >= 0
main_GE_148(i17, x, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17 && x = 100
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2

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

Moved arithmethic from constraints to rhss.

main_GE_242(i35, x, env, static) -{3,3}> main_Load_235(i37', env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37' && x = 21
was transformed to
main_GE_242(i35, x, env, static) -{3,3}> main_Load_235(i35 + 3, env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37' && x = 21

main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, iconst_21, env, static) :|: iconst_21 = 21 && 21 <= i36
was transformed to
main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, 21, env, static) :|: iconst_21 = 21 && 21 <= i36

main_GE_148(i16, x, env, static) -{3,3}> main_Load_137(i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18' && x = 100
was transformed to
main_GE_148(i16, x, env, static) -{3,3}> main_Load_137(i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18' && x = 100

(26) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_242(i35, x, env, static) -{3,3}> main_Load_235(i35 + 3, env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37' && x = 21
main_Load_137(i10, env, static) -{2,2}> main_GE_148(i10, 100, env, static) :|: 1 <= i10
main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, 21, env, static) :|: iconst_21 = 21 && 21 <= i36
main_GE_148(i16, x, env, static) -{3,3}> main_Load_137(i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18' && x = 100
main_GE_148(i17, x, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17 && x = 100
main_Load_235(i29, env, static) -{2,2}> main_GE_242(i29, 21, env, static) :|: 0 >= 0
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2

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

Simplified expressions.

main_GE_148(i17, x, env, static) -{3,3}> main_Load_235(5, env, static) :|: 5 <= 14 && 5 <= 5 && 100 <= i17 && 1 <= i17 && x = 100
was transformed to
main_GE_148(i17, x, env, static) -{3,3}> main_Load_235(5, env, static) :|: 100 <= i17 && 1 <= i17 && x = 100

main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 < 2 && 1 <= 3 && 1 <= 1 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 1 <= 2
was transformed to
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(28) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_137(i10, env, static) -{2,2}> main_GE_148(i10, 100, env, static) :|: 1 <= i10
main_GE_148(i16, x, env, static) -{3,3}> main_Load_137(i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18' && x = 100
main_GE_242(i35, x, env, static) -{3,3}> main_Load_235(i35 + 3, env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37' && x = 21
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, 21, env, static) :|: iconst_21 = 21 && 21 <= i36
main_GE_148(i17, x, env, static) -{3,3}> main_Load_235(5, env, static) :|: 100 <= i17 && 1 <= i17 && x = 100
main_Load_235(i29, env, static) -{2,2}> main_GE_242(i29, 21, env, static) :|: 0 >= 0

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

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

(30) Obligation:

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

(32) Obligation:

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

Moved arithmethic from lhss to constraints.

(34) Obligation:

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

Moved arithmethic from constraints to rhss.

(36) Obligation:

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

Simplified expressions.

(38) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_137(i10, env, static) -{2,2}> main_GE_148(i10, 100, env, static) :|: 1 <= i10
main_GE_148(i16, x, env, static) -{3,3}> main_Load_137(i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 1 <= i18' && 2 <= i18' && i16 < 100 && i16 + 1 = i18' && x = 100
main_GE_242(i35, x, env, static) -{3,3}> main_Load_235(i35 + 3, env, static) :|: i37' <= 23 && i35 < 21 && i35 <= 20 && i35 + 3 = i37' && x = 21
main_ConstantStackPush_2(env, static) -{22,22}> main_Load_137(1, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GE_242(i36, iconst_21, env, static) -{0,0}> main_GE_244(i36, 21, env, static) :|: iconst_21 = 21 && 21 <= i36
main_GE_148(i17, x, env, static) -{3,3}> main_Load_235(5, env, static) :|: 100 <= i17 && 1 <= i17 && x = 100
main_Load_235(i29, env, static) -{2,2}> main_GE_242(i29, 21, env, static) :|: 0 >= 0