time complexity proof of /tmp/tmp3KctF3/ClassAnalysis.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

    ↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)), 7 ms)

    ↳4 JBCComplexityEdges

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

        ↳6 WeightedIntTrs

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

            ↳8 WeightedIntTrs

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

            ↳10 WeightedIntTrs

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

            ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

            ↳16 WeightedIntTrs

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

            ↳18 WeightedIntTrs

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

            ↳20 WeightedIntTrs

            ↳21 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 5 ms)

            ↳22 WeightedIntTrs

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

    ↳24 JBCComplexityEdges

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

        ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

        ↳35 koat Proof (⇔, 13 ms)

        ↳36 BOUNDS(CONSTANT, 448)

↳37 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 656 ms)

↳38 JBCTerminationGraph

(0) Obligation:

Need to prove time_complexity of the following program:

package ClassAnalysis;

public class ClassAnalysis {
	A field;

	public static void main(int i) {
		ClassAnalysis t = new ClassAnalysis();
		t.field = new A();
		t.field = new B();
		t.eval(i);
	}

	public void eval(int y) {
		int x = y % 100;
		this.field.test(x);
	}
}

class A {
	public boolean test(int x) {
		while (x > 0) {
			if (x > 10) {
				x--;
			} else {
				x++;
			}
		}
		return true;
	}
}

class B extends A {
	public boolean test(int x) {
		while (x > 0) {
			x--;
		}
		return true;
	}
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ClassAnalysis.ClassAnalysis.main(I)V: Graph of 75 nodes with 1 SCC.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- ClassAnalysis.ClassAnalysis: [field]

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 69 jbc graph edges to a weighted ITS with 69 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 69 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i1, env, static) -{0,0}> main_New_4(i1, env, static) :|: 0 >= 0
main_New_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_34(i1, env, static) -{0,0}> langle_clinit_rangle_New_35(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_35(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_37(o3, i1, env, static) :|: o3 = 1 && 0 < o3
langle_clinit_rangle_Duplicate_37(o3, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) :|: NULL = 0 && 0 < o3
langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_42(o3, i1, env, static) :|: NULL = 0 && 0 < o3
langle_init_rangle_Load_42(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_45(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_45(o3, i1, env, static) -{1,1}> langle_init_rangle_Load_46(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Load_46(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_49(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_49(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_51(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_51(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_53(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_53(o3, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) -{1,1}> langle_clinit_rangle_Return_57(i1, env, static') :|: 0 < o3 && 0 <= o3 && 0 <= static && static' <= static + o3
langle_clinit_rangle_Return_57(i1, env, static) -{1,1}> main_New_59(i1, env, static) :|: 0 >= 0
main_New_59(i1, env, static) -{0,0}> main_New_60(i1, env, static) :|: 0 >= 0
main_New_60(i1, env, static) -{0,0}> main_New_61(i1, env, static) :|: 0 <= static
main_New_61(i1, env, static) -{0,0}> main_New_62(i1, env, static) :|: 0 >= 0
main_New_62(i1, env, static) -{0,0}> main_New_63(i1, env, static) :|: 0 >= 0
main_New_63(i1, env, static) -{1,1}> main_Duplicate_64(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5 && o5 = 1
main_Duplicate_64(i1, o5, NULL, env, static) -{1,1}> main_InvokeMethod_65(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_InvokeMethod_65(i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Load_66(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Load_66(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_Return_68(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Return_68(i1, o5, NULL, env, static) -{1,1}> main_Store_69(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Store_69(i1, o5, NULL, env, static) -{1,1}> main_Load_70(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Load_70(i1, o5, NULL, env, static) -{1,1}> main_New_71(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_71(i1, o5, NULL, env, static) -{0,0}> main_New_73(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_73(i1, o5, NULL, env, static) -{1,1}> main_Duplicate_75(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5 && o6 = 1
main_Duplicate_75(i1, o5, o6, NULL, env, static) -{1,1}> main_InvokeMethod_76(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_InvokeMethod_76(i1, o5, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) -{1,1}> main_FieldAccess_80(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_FieldAccess_80(i1, o5, o6, NULL, env, static) -{1,1}> main_Load_84(i1, o5', o6, env, static) :|: NULL = 0 && o5' = o5 + o6 && 0 < o6 && 0 < o5 && 0 < o5' && o5' <= o5 + o6
main_Load_84(i1, o5, o6, env, static) -{1,1}> main_New_87(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_87(i1, o5, o6, env, static) -{0,0}> main_New_89(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_89(i1, o5, o6, env, static) -{1,1}> main_Duplicate_91(i1, o5, o8, o6, env, static) :|: o8 = 1 && 0 < o6 && 0 < o5 && 0 < o8
main_Duplicate_91(i1, o5, o8, o6, env, static) -{1,1}> main_InvokeMethod_93(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_InvokeMethod_93(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) -{1,1}> main_FieldAccess_108(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_FieldAccess_108(i1, o5, o8, o6, env, static) -{1,1}> main_Load_109(i1, o5', o8, env, static) :|: 0 < o6 && 0 < o5 && o5' = o5 + o8 + -1 * o6 && 0 < o5' && o5' <= o5 + o8 && 0 < o8
main_Load_109(i1, o5, o8, env, static) -{1,1}> main_Load_111(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_Load_111(i1, o5, o8, env, static) -{1,1}> main_InvokeMethod_114(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_InvokeMethod_114(i1, o5, o8, env, static) -{1,1}> eval_Load_116(o5, i1, o8, env, static) :|: 0 < o5 && 0 < o8
eval_Load_116(o5, i1, o8, env, static) -{1,1}> eval_ConstantStackPush_117(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
eval_ConstantStackPush_117(i1, o5, o8, env, static) -{1,1}> eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) :|: 0 < o5 && iconst_100 = 100 && 0 < o8
eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) -{1,1}> eval_Store_119(i4, o5, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && iconst_100 = 100 && -99 <= i4 && 0 < o8
eval_Store_119(i4, o5, i1, o8, env, static) -{1,1}> eval_Load_120(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_120(o5, i4, i1, o8, env, static) -{1,1}> eval_FieldAccess_121(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_FieldAccess_121(o5, i4, i1, o8, env, static) -{1,1}> eval_Load_124(o8, i4, i1, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_124(o8, i4, i1, env, static) -{1,1}> eval_InvokeMethod_126(o8, i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
eval_InvokeMethod_126(o8, i4, i1, env, static) -{1,1}> test_Load_127(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0
test_LE_128(i7, i1, env, static) -{0,0}> test_LE_130(i7, i1, env, static) :|: 1 <= i7 && -99 <= i7 && i7 <= 99
test_LE_130(i7, i1, env, static) -{1,1}> test_Inc_135(i7, i1, env, static) :|: 0 < i7 && 1 <= i7 && i7 <= 99
test_Inc_135(i7, i1, env, static) -{1,1}> test_JMP_137(i9, i1, env, static) :|: 1 <= i7 && 0 <= i9 && i7 + -1 = i9 && i9 <= 98 && i7 <= 99
test_JMP_137(i9, i1, env, static) -{1,1}> test_Load_139(i9, i1, env, static) :|: 0 <= i9 && i9 <= 98
test_Load_139(i9, i1, env, static) -{0,0}> test_Load_127(i9, i1, env, static) :|: -99 <= i9 && 0 <= i9 && i9 <= 99 && i9 <= 98

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

obtained
main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
by chaining
main_New_2(i1, env, static) -{0,0}> main_New_4(i1, env, static) :|: 0 >= 0
main_New_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_34(i1, env, static) -{0,0}> langle_clinit_rangle_New_35(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_35(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_37(o3, i1, env, static) :|: o3 = 1 && 0 < o3
langle_clinit_rangle_Duplicate_37(o3, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) :|: NULL = 0 && 0 < o3
langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_42(o3, i1, env, static) :|: NULL = 0 && 0 < o3
langle_init_rangle_Load_42(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_45(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_45(o3, i1, env, static) -{1,1}> langle_init_rangle_Load_46(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Load_46(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_49(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_49(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_51(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_51(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_53(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_53(o3, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) -{1,1}> langle_clinit_rangle_Return_57(i1, env, static') :|: 0 < o3 && 0 <= o3 && 0 <= static && static' <= static + o3
langle_clinit_rangle_Return_57(i1, env, static) -{1,1}> main_New_59(i1, env, static) :|: 0 >= 0
main_New_59(i1, env, static) -{0,0}> main_New_60(i1, env, static) :|: 0 >= 0
main_New_60(i1, env, static) -{0,0}> main_New_61(i1, env, static) :|: 0 <= static
main_New_61(i1, env, static) -{0,0}> main_New_62(i1, env, static) :|: 0 >= 0
main_New_62(i1, env, static) -{0,0}> main_New_63(i1, env, static) :|: 0 >= 0
main_New_63(i1, env, static) -{1,1}> main_Duplicate_64(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5 && o5 = 1
main_Duplicate_64(i1, o5, NULL, env, static) -{1,1}> main_InvokeMethod_65(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_InvokeMethod_65(i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Load_66(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Load_66(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_Return_68(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Return_68(i1, o5, NULL, env, static) -{1,1}> main_Store_69(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Store_69(i1, o5, NULL, env, static) -{1,1}> main_Load_70(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Load_70(i1, o5, NULL, env, static) -{1,1}> main_New_71(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_71(i1, o5, NULL, env, static) -{0,0}> main_New_73(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_73(i1, o5, NULL, env, static) -{1,1}> main_Duplicate_75(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5 && o6 = 1
main_Duplicate_75(i1, o5, o6, NULL, env, static) -{1,1}> main_InvokeMethod_76(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_InvokeMethod_76(i1, o5, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) -{1,1}> main_FieldAccess_80(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_FieldAccess_80(i1, o5, o6, NULL, env, static) -{1,1}> main_Load_84(i1, o5', o6, env, static) :|: NULL = 0 && o5' = o5 + o6 && 0 < o6 && 0 < o5 && 0 < o5' && o5' <= o5 + o6
main_Load_84(i1, o5, o6, env, static) -{1,1}> main_New_87(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_87(i1, o5, o6, env, static) -{0,0}> main_New_89(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_89(i1, o5, o6, env, static) -{1,1}> main_Duplicate_91(i1, o5, o8, o6, env, static) :|: o8 = 1 && 0 < o6 && 0 < o5 && 0 < o8
main_Duplicate_91(i1, o5, o8, o6, env, static) -{1,1}> main_InvokeMethod_93(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_InvokeMethod_93(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) -{1,1}> main_FieldAccess_108(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_FieldAccess_108(i1, o5, o8, o6, env, static) -{1,1}> main_Load_109(i1, o5', o8, env, static) :|: 0 < o6 && 0 < o5 && o5' = o5 + o8 + -1 * o6 && 0 < o5' && o5' <= o5 + o8 && 0 < o8
main_Load_109(i1, o5, o8, env, static) -{1,1}> main_Load_111(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_Load_111(i1, o5, o8, env, static) -{1,1}> main_InvokeMethod_114(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_InvokeMethod_114(i1, o5, o8, env, static) -{1,1}> eval_Load_116(o5, i1, o8, env, static) :|: 0 < o5 && 0 < o8
eval_Load_116(o5, i1, o8, env, static) -{1,1}> eval_ConstantStackPush_117(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
eval_ConstantStackPush_117(i1, o5, o8, env, static) -{1,1}> eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) :|: 0 < o5 && iconst_100 = 100 && 0 < o8
eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) -{1,1}> eval_Store_119(i4, o5, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && iconst_100 = 100 && -99 <= i4 && 0 < o8
eval_Store_119(i4, o5, i1, o8, env, static) -{1,1}> eval_Load_120(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_120(o5, i4, i1, o8, env, static) -{1,1}> eval_FieldAccess_121(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_FieldAccess_121(o5, i4, i1, o8, env, static) -{1,1}> eval_Load_124(o8, i4, i1, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_124(o8, i4, i1, env, static) -{1,1}> eval_InvokeMethod_126(o8, i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
eval_InvokeMethod_126(o8, i4, i1, env, static) -{1,1}> test_Load_127(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8

obtained
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i9', i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'
by chaining
test_LE_128(i7, i1, env, static) -{0,0}> test_LE_130(i7, i1, env, static) :|: 1 <= i7 && -99 <= i7 && i7 <= 99
test_LE_130(i7, i1, env, static) -{1,1}> test_Inc_135(i7, i1, env, static) :|: 0 < i7 && 1 <= i7 && i7 <= 99
test_Inc_135(i7, i1, env, static) -{1,1}> test_JMP_137(i9, i1, env, static) :|: 1 <= i7 && 0 <= i9 && i7 + -1 = i9 && i9 <= 98 && i7 <= 99
test_JMP_137(i9, i1, env, static) -{1,1}> test_Load_139(i9, i1, env, static) :|: 0 <= i9 && i9 <= 98
test_Load_139(i9, i1, env, static) -{0,0}> test_Load_127(i9, i1, env, static) :|: -99 <= i9 && 0 <= i9 && i9 <= 99 && i9 <= 98

(8) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i9', i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'

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

Moved arithmethic from constraints to rhss.

test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i9', i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'
was transformed to
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i7 + -1, i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'

(10) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i7 + -1, i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'
main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0

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

Simplified expressions.

test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i7 + -1, i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'
was transformed to
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i7 - 1, i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 - 1 = i9'

(12) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i7 - 1, i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 - 1 = i9'
main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 2 && 0 < o5''' && 0 <= static && o5'1 = o5''' && 0 <= static'1 && o5'1 <= o5''' + 1
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0

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

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

(14) Obligation:

IntTrs with 69 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i1, env, static) -{0,0}> main_New_4(i1, env, static) :|: 0 >= 0
main_New_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_34(i1, env, static) -{0,0}> langle_clinit_rangle_New_35(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_35(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_37(o3, i1, env, static) :|: o3 = 1 && 0 < o3
langle_clinit_rangle_Duplicate_37(o3, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) :|: NULL = 0 && 0 < o3
langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_42(o3, i1, env, static) :|: NULL = 0 && 0 < o3
langle_init_rangle_Load_42(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_45(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_45(o3, i1, env, static) -{1,1}> langle_init_rangle_Load_46(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Load_46(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_49(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_49(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_51(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_51(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_53(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_53(o3, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) -{1,1}> langle_clinit_rangle_Return_57(i1, env, static') :|: 0 < o3 && 0 <= o3 && 0 <= static && static' <= static + o3
langle_clinit_rangle_Return_57(i1, env, static) -{1,1}> main_New_59(i1, env, static) :|: 0 >= 0
main_New_59(i1, env, static) -{0,0}> main_New_60(i1, env, static) :|: 0 >= 0
main_New_60(i1, env, static) -{0,0}> main_New_61(i1, env, static) :|: 0 <= static
main_New_61(i1, env, static) -{0,0}> main_New_62(i1, env, static) :|: 0 >= 0
main_New_62(i1, env, static) -{0,0}> main_New_63(i1, env, static) :|: 0 >= 0
main_New_63(i1, env, static) -{1,1}> main_Duplicate_64(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5 && o5 = 1
main_Duplicate_64(i1, o5, NULL, env, static) -{1,1}> main_InvokeMethod_65(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_InvokeMethod_65(i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Load_66(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Load_66(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_Return_68(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Return_68(i1, o5, NULL, env, static) -{1,1}> main_Store_69(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Store_69(i1, o5, NULL, env, static) -{1,1}> main_Load_70(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Load_70(i1, o5, NULL, env, static) -{1,1}> main_New_71(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_71(i1, o5, NULL, env, static) -{0,0}> main_New_73(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_73(i1, o5, NULL, env, static) -{1,1}> main_Duplicate_75(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5 && o6 = 1
main_Duplicate_75(i1, o5, o6, NULL, env, static) -{1,1}> main_InvokeMethod_76(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_InvokeMethod_76(i1, o5, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) -{1,1}> main_FieldAccess_80(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_FieldAccess_80(i1, o5, o6, NULL, env, static) -{1,1}> main_Load_84(i1, o5', o6, env, static) :|: NULL = 0 && o5' = o5 + o6 && 0 < o6 && 0 < o5 && 0 < o5' && o5' <= o5 + o6
main_Load_84(i1, o5, o6, env, static) -{1,1}> main_New_87(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_87(i1, o5, o6, env, static) -{0,0}> main_New_89(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_89(i1, o5, o6, env, static) -{1,1}> main_Duplicate_91(i1, o5, o8, o6, env, static) :|: o8 = 1 && 0 < o6 && 0 < o5 && 0 < o8
main_Duplicate_91(i1, o5, o8, o6, env, static) -{1,1}> main_InvokeMethod_93(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_InvokeMethod_93(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) -{1,1}> main_FieldAccess_108(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_FieldAccess_108(i1, o5, o8, o6, env, static) -{1,1}> main_Load_109(i1, o5', o8, env, static) :|: 0 < o6 && 0 < o5 && o5' = o5 + o8 + -1 * o6 && 0 < o5' && o5' <= o5 + o8 && 0 < o8
main_Load_109(i1, o5, o8, env, static) -{1,1}> main_Load_111(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_Load_111(i1, o5, o8, env, static) -{1,1}> main_InvokeMethod_114(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_InvokeMethod_114(i1, o5, o8, env, static) -{1,1}> eval_Load_116(o5, i1, o8, env, static) :|: 0 < o5 && 0 < o8
eval_Load_116(o5, i1, o8, env, static) -{1,1}> eval_ConstantStackPush_117(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
eval_ConstantStackPush_117(i1, o5, o8, env, static) -{1,1}> eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) :|: 0 < o5 && iconst_100 = 100 && 0 < o8
eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) -{1,1}> eval_Store_119(i4, o5, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && i1 % iconst_100 = i4 && iconst_100 = 100 && -99 <= i4 && 0 < o8
eval_Store_119(i4, o5, i1, o8, env, static) -{1,1}> eval_Load_120(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_120(o5, i4, i1, o8, env, static) -{1,1}> eval_FieldAccess_121(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_FieldAccess_121(o5, i4, i1, o8, env, static) -{1,1}> eval_Load_124(o8, i4, i1, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_124(o8, i4, i1, env, static) -{1,1}> eval_InvokeMethod_126(o8, i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
eval_InvokeMethod_126(o8, i4, i1, env, static) -{1,1}> test_Load_127(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0
test_LE_128(i7, i1, env, static) -{0,0}> test_LE_130(i7, i1, env, static) :|: 1 <= i7 && -99 <= i7 && i7 <= 99
test_LE_130(i7, i1, env, static) -{1,1}> test_Inc_135(i7, i1, env, static) :|: 0 < i7 && 1 <= i7 && i7 <= 99
test_Inc_135(i7, i1, env, static) -{1,1}> test_JMP_137(i9, i1, env, static) :|: 1 <= i7 && 0 <= i9 && i7 + -1 = i9 && i9 <= 98 && i7 <= 99
test_JMP_137(i9, i1, env, static) -{1,1}> test_Load_139(i9, i1, env, static) :|: 0 <= i9 && i9 <= 98
test_Load_139(i9, i1, env, static) -{0,0}> test_Load_127(i9, i1, env, static) :|: -99 <= i9 && 0 <= i9 && i9 <= 99 && i9 <= 98

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

obtained
main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 % 100 = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
by chaining
main_New_2(i1, env, static) -{0,0}> main_New_4(i1, env, static) :|: 0 >= 0
main_New_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_34(i1, env, static) -{0,0}> langle_clinit_rangle_New_35(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_35(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_37(o3, i1, env, static) :|: o3 = 1 && 0 < o3
langle_clinit_rangle_Duplicate_37(o3, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) :|: NULL = 0 && 0 < o3
langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_42(o3, i1, env, static) :|: NULL = 0 && 0 < o3
langle_init_rangle_Load_42(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_45(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_45(o3, i1, env, static) -{1,1}> langle_init_rangle_Load_46(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Load_46(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_49(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_49(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_51(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_51(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_53(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_53(o3, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) -{1,1}> langle_clinit_rangle_Return_57(i1, env, static') :|: 0 < o3 && 0 <= o3 && 0 <= static && static' <= static + o3
langle_clinit_rangle_Return_57(i1, env, static) -{1,1}> main_New_59(i1, env, static) :|: 0 >= 0
main_New_59(i1, env, static) -{0,0}> main_New_60(i1, env, static) :|: 0 >= 0
main_New_60(i1, env, static) -{0,0}> main_New_61(i1, env, static) :|: 0 <= static
main_New_61(i1, env, static) -{0,0}> main_New_62(i1, env, static) :|: 0 >= 0
main_New_62(i1, env, static) -{0,0}> main_New_63(i1, env, static) :|: 0 >= 0
main_New_63(i1, env, static) -{1,1}> main_Duplicate_64(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5 && o5 = 1
main_Duplicate_64(i1, o5, NULL, env, static) -{1,1}> main_InvokeMethod_65(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_InvokeMethod_65(i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Load_66(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Load_66(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_Return_68(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Return_68(i1, o5, NULL, env, static) -{1,1}> main_Store_69(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Store_69(i1, o5, NULL, env, static) -{1,1}> main_Load_70(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Load_70(i1, o5, NULL, env, static) -{1,1}> main_New_71(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_71(i1, o5, NULL, env, static) -{0,0}> main_New_73(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_73(i1, o5, NULL, env, static) -{1,1}> main_Duplicate_75(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5 && o6 = 1
main_Duplicate_75(i1, o5, o6, NULL, env, static) -{1,1}> main_InvokeMethod_76(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_InvokeMethod_76(i1, o5, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) -{1,1}> main_FieldAccess_80(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_FieldAccess_80(i1, o5, o6, NULL, env, static) -{1,1}> main_Load_84(i1, o5', o6, env, static) :|: NULL = 0 && o5' = o5 + o6 && 0 < o6 && 0 < o5 && 0 < o5' && o5' <= o5 + o6
main_Load_84(i1, o5, o6, env, static) -{1,1}> main_New_87(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_87(i1, o5, o6, env, static) -{0,0}> main_New_89(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_89(i1, o5, o6, env, static) -{1,1}> main_Duplicate_91(i1, o5, o8, o6, env, static) :|: o8 = 1 && 0 < o6 && 0 < o5 && 0 < o8
main_Duplicate_91(i1, o5, o8, o6, env, static) -{1,1}> main_InvokeMethod_93(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_InvokeMethod_93(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) -{1,1}> main_FieldAccess_108(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_FieldAccess_108(i1, o5, o8, o6, env, static) -{1,1}> main_Load_109(i1, o5', o8, env, static) :|: 0 < o6 && 0 < o5 && o5' = o5 + o8 + -1 * o6 && 0 < o5' && o5' <= o5 + o8 && 0 < o8
main_Load_109(i1, o5, o8, env, static) -{1,1}> main_Load_111(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_Load_111(i1, o5, o8, env, static) -{1,1}> main_InvokeMethod_114(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_InvokeMethod_114(i1, o5, o8, env, static) -{1,1}> eval_Load_116(o5, i1, o8, env, static) :|: 0 < o5 && 0 < o8
eval_Load_116(o5, i1, o8, env, static) -{1,1}> eval_ConstantStackPush_117(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
eval_ConstantStackPush_117(i1, o5, o8, env, static) -{1,1}> eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) :|: 0 < o5 && iconst_100 = 100 && 0 < o8
eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) -{1,1}> eval_Store_119(i4, o5, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && i1 % iconst_100 = i4 && iconst_100 = 100 && -99 <= i4 && 0 < o8
eval_Store_119(i4, o5, i1, o8, env, static) -{1,1}> eval_Load_120(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_120(o5, i4, i1, o8, env, static) -{1,1}> eval_FieldAccess_121(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_FieldAccess_121(o5, i4, i1, o8, env, static) -{1,1}> eval_Load_124(o8, i4, i1, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_124(o8, i4, i1, env, static) -{1,1}> eval_InvokeMethod_126(o8, i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
eval_InvokeMethod_126(o8, i4, i1, env, static) -{1,1}> test_Load_127(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8

(16) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 % 100 = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i9', i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'

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

Removed div and mod.

main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 % 100 = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
was transformed to
main_New_2(i1, env, static) -{52,52}> main_New_2'(i1, env, static) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
main_New_2'(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: i1 - 100 * div < 100 && i1 - 100 * div + 100 > 0 && 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1

(18) Obligation:

IntTrs with 5 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i9', i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'
main_New_2(i1, env, static) -{52,52}> main_New_2'(i1, env, static) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
main_New_2'(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: i1 - 100 * div < 100 && i1 - 100 * div + 100 > 0 && 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0

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

Moved arithmethic from constraints to rhss.

main_New_2'(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: i1 - 100 * div < 100 && i1 - 100 * div + 100 > 0 && 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
was transformed to
main_New_2'(i1, env, static) -{52,52}> test_Load_127(i1 - 100 * div, i1, env, static'1) :|: i1 - 100 * div < 100 && i1 - 100 * div + 100 > 0 && 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1

(20) Obligation:

IntTrs with 5 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i7 + -1, i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 + -1 = i9'
main_New_2'(i1, env, static) -{52,52}> test_Load_127(i1 - 100 * div, i1, env, static'1) :|: i1 - 100 * div < 100 && i1 - 100 * div + 100 > 0 && 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
main_New_2(i1, env, static) -{52,52}> main_New_2'(i1, env, static) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0

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

Simplified expressions.

main_New_2'(i1, env, static) -{52,52}> test_Load_127(i1 - 100 * div, i1, env, static'1) :|: i1 - 100 * div < 100 && i1 - 100 * div + 100 > 0 && 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
was transformed to
main_New_2'(i1, env, static) -{52,52}> test_Load_127(i1 + -100 * div, i1, env, static'1) :|: i1 + -100 * div < 100 && 0 < i1 + -100 * div + 100 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 2 && 0 < o5''' && 0 <= static && o5'1 = o5''' && 0 <= static'1 && i1 + -100 * div = i4' && o5'1 <= o5''' + 1

main_New_2(i1, env, static) -{52,52}> main_New_2'(i1, env, static) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && i1 - 100 * div = i4' && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
was transformed to
main_New_2(i1, env, static) -{52,52}> main_New_2'(i1, env, static) :|: static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 2 && 0 < o5''' && 0 <= static && o5'1 = o5''' && 0 <= static'1 && i1 + -100 * div = i4' && o5'1 <= o5''' + 1

(22) Obligation:

IntTrs with 5 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i7, i1, env, static) -{3,3}> test_Load_127(i7 - 1, i1, env, static) :|: i7 <= 99 && i9' <= 98 && 0 < i7 && i9' <= 99 && -99 <= i7 && -99 <= i9' && 0 <= i9' && 1 <= i7 && i7 - 1 = i9'
test_LE_128(i5, i1, env, static) -{0,0}> test_LE_129(i5, i1, env, static) :|: -99 <= i5 && i5 <= 99 && i5 <= 0
main_New_2'(i1, env, static) -{52,52}> test_Load_127(i1 + -100 * div, i1, env, static'1) :|: i1 + -100 * div < 100 && 0 < i1 + -100 * div + 100 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 2 && 0 < o5''' && 0 <= static && o5'1 = o5''' && 0 <= static'1 && i1 + -100 * div = i4' && o5'1 <= o5''' + 1
main_New_2(i1, env, static) -{52,52}> main_New_2'(i1, env, static) :|: static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 2 && 0 < o5''' && 0 <= static && o5'1 = o5''' && 0 <= static'1 && i1 + -100 * div = i4' && o5'1 <= o5''' + 1

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

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

(24) Obligation:

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

Used field analysis yielded the following read fields:
- ClassAnalysis.ClassAnalysis: [field]

Considered paths: all paths from start

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

Transformed 68 jbc graph edges to a weighted ITS with 68 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(26) Obligation:

IntTrs with 68 rules
Start term: main_New_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_New_2(i1, env, static) -{0,0}> main_New_4(i1, env, static) :|: 0 >= 0
main_New_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_28(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_30(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_34(i1, env, static) -{0,0}> langle_clinit_rangle_New_35(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_35(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_37(o3, i1, env, static) :|: o3 = 1 && 0 < o3
langle_clinit_rangle_Duplicate_37(o3, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_ConstantStackPush_39(o3, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) :|: NULL = 0 && 0 < o3
langle_clinit_rangle_InvokeMethod_41(o3, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_42(o3, i1, env, static) :|: NULL = 0 && 0 < o3
langle_init_rangle_Load_42(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_45(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_45(o3, i1, env, static) -{1,1}> langle_init_rangle_Load_46(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Load_46(o3, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_49(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_InvokeMethod_49(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_51(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_51(o3, i1, env, static) -{1,1}> langle_init_rangle_Return_53(o3, i1, env, static) :|: 0 < o3
langle_init_rangle_Return_53(o3, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) :|: 0 < o3
langle_clinit_rangle_FieldAccess_55(o3, i1, env, static) -{1,1}> langle_clinit_rangle_Return_57(i1, env, static') :|: 0 < o3 && 0 <= o3 && 0 <= static && static' <= static + o3
langle_clinit_rangle_Return_57(i1, env, static) -{1,1}> main_New_59(i1, env, static) :|: 0 >= 0
main_New_59(i1, env, static) -{0,0}> main_New_60(i1, env, static) :|: 0 >= 0
main_New_60(i1, env, static) -{0,0}> main_New_61(i1, env, static) :|: 0 <= static
main_New_61(i1, env, static) -{0,0}> main_New_62(i1, env, static) :|: 0 >= 0
main_New_62(i1, env, static) -{0,0}> main_New_63(i1, env, static) :|: 0 >= 0
main_New_63(i1, env, static) -{1,1}> main_Duplicate_64(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5 && o5 = 1
main_Duplicate_64(i1, o5, NULL, env, static) -{1,1}> main_InvokeMethod_65(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_InvokeMethod_65(i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Load_66(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Load_66(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_InvokeMethod_67(o5, i1, NULL, env, static) -{1,1}> langle_init_rangle_Return_68(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
langle_init_rangle_Return_68(i1, o5, NULL, env, static) -{1,1}> main_Store_69(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Store_69(i1, o5, NULL, env, static) -{1,1}> main_Load_70(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_Load_70(i1, o5, NULL, env, static) -{1,1}> main_New_71(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_71(i1, o5, NULL, env, static) -{0,0}> main_New_73(i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o5
main_New_73(i1, o5, NULL, env, static) -{1,1}> main_Duplicate_75(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5 && o6 = 1
main_Duplicate_75(i1, o5, o6, NULL, env, static) -{1,1}> main_InvokeMethod_76(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_InvokeMethod_76(i1, o5, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Load_77(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_InvokeMethod_78(o6, i1, o5, NULL, env, static) -{1,1}> langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
langle_init_rangle_Return_79(i1, o5, o6, NULL, env, static) -{1,1}> main_FieldAccess_80(i1, o5, o6, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o5
main_FieldAccess_80(i1, o5, o6, NULL, env, static) -{1,1}> main_Load_84(i1, o5', o6, env, static) :|: NULL = 0 && o5' = o5 + o6 && 0 < o6 && 0 < o5 && 0 < o5' && o5' <= o5 + o6
main_Load_84(i1, o5, o6, env, static) -{1,1}> main_New_87(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_87(i1, o5, o6, env, static) -{0,0}> main_New_89(i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5
main_New_89(i1, o5, o6, env, static) -{1,1}> main_Duplicate_91(i1, o5, o8, o6, env, static) :|: o8 = 1 && 0 < o6 && 0 < o5 && 0 < o8
main_Duplicate_91(i1, o5, o8, o6, env, static) -{1,1}> main_InvokeMethod_93(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_InvokeMethod_93(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_95(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_97(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Load_98(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_InvokeMethod_104(o8, i1, o5, o6, env, static) -{1,1}> langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_106(i1, o5, o8, o6, env, static) -{1,1}> langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
langle_init_rangle_Return_107(i1, o5, o8, o6, env, static) -{1,1}> main_FieldAccess_108(i1, o5, o8, o6, env, static) :|: 0 < o6 && 0 < o5 && 0 < o8
main_FieldAccess_108(i1, o5, o8, o6, env, static) -{1,1}> main_Load_109(i1, o5', o8, env, static) :|: 0 < o6 && 0 < o5 && o5' = o5 + o8 + -1 * o6 && 0 < o5' && o5' <= o5 + o8 && 0 < o8
main_Load_109(i1, o5, o8, env, static) -{1,1}> main_Load_111(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_Load_111(i1, o5, o8, env, static) -{1,1}> main_InvokeMethod_114(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
main_InvokeMethod_114(i1, o5, o8, env, static) -{1,1}> eval_Load_116(o5, i1, o8, env, static) :|: 0 < o5 && 0 < o8
eval_Load_116(o5, i1, o8, env, static) -{1,1}> eval_ConstantStackPush_117(i1, o5, o8, env, static) :|: 0 < o5 && 0 < o8
eval_ConstantStackPush_117(i1, o5, o8, env, static) -{1,1}> eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) :|: 0 < o5 && iconst_100 = 100 && 0 < o8
eval_IntArithmetic_118(i1, iconst_100, o5, o8, env, static) -{1,1}> eval_Store_119(i4, o5, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && iconst_100 = 100 && -99 <= i4 && 0 < o8
eval_Store_119(i4, o5, i1, o8, env, static) -{1,1}> eval_Load_120(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_120(o5, i4, i1, o8, env, static) -{1,1}> eval_FieldAccess_121(o5, i4, i1, o8, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_FieldAccess_121(o5, i4, i1, o8, env, static) -{1,1}> eval_Load_124(o8, i4, i1, env, static) :|: 0 < o5 && i4 <= 99 && -99 <= i4 && 0 < o8
eval_Load_124(o8, i4, i1, env, static) -{1,1}> eval_InvokeMethod_126(o8, i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
eval_InvokeMethod_126(o8, i4, i1, env, static) -{1,1}> test_Load_127(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4 && 0 < o8
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i7, i1, env, static) -{0,0}> test_LE_130(i7, i1, env, static) :|: 1 <= i7 && -99 <= i7 && i7 <= 99
test_LE_130(i7, i1, env, static) -{1,1}> test_Inc_135(i7, i1, env, static) :|: 0 < i7 && 1 <= i7 && i7 <= 99
test_Inc_135(i7, i1, env, static) -{1,1}> test_JMP_137(i9, i1, env, static) :|: 1 <= i7 && 0 <= i9 && i7 + -1 = i9 && i9 <= 98 && i7 <= 99
test_JMP_137(i9, i1, env, static) -{1,1}> test_Load_139(i9, i1, env, static) :|: 0 <= i9 && i9 <= 98
test_Load_139(i9, i1, env, static) -{0,0}> test_Load_127(i9, i1, env, static) :|: -99 <= i9 && 0 <= i9 && i9 <= 99 && i9 <= 98

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

obtained
test_Load_127(i4, i1, env, static) -{4,4}> test_Load_127(i9', i1, env, static) :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 + -1 = i9'
by chaining
test_Load_127(i4, i1, env, static) -{1,1}> test_LE_128(i4, i1, env, static) :|: i4 <= 99 && -99 <= i4
test_LE_128(i7, i1, env, static) -{0,0}> test_LE_130(i7, i1, env, static) :|: 1 <= i7 && -99 <= i7 && i7 <= 99
test_LE_130(i7, i1, env, static) -{1,1}> test_Inc_135(i7, i1, env, static) :|: 0 < i7 && 1 <= i7 && i7 <= 99
test_Inc_135(i7, i1, env, static) -{1,1}> test_JMP_137(i9, i1, env, static) :|: 1 <= i7 && 0 <= i9 && i7 + -1 = i9 && i9 <= 98 && i7 <= 99
test_JMP_137(i9, i1, env, static) -{1,1}> test_Load_139(i9, i1, env, static) :|: 0 <= i9 && i9 <= 98
test_Load_139(i9, i1, env, static) -{0,0}> test_Load_127(i9, i1, env, static) :|: -99 <= i9 && 0 <= i9 && i9 <= 99 && i9 <= 98

(28) Obligation:

IntTrs with 2 rules
Start term: main_New_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_New_2(i1, env, static) -{52,52}> test_Load_127(i4', i1, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
test_Load_127(i4, i1, env, static) -{4,4}> test_Load_127(i9', i1, env, static) :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 + -1 = i9'

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

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

main_New_2(x1, x2, x3) → main_New_2(x3)
test_Load_127(x1, x2, x3, x4) → test_Load_127(x1)

(30) Obligation:

IntTrs with 2 rules
Start term: main_New_2(static)
Considered paths: all paths from start
Rules:
main_New_2(static) -{52,52}> test_Load_127(i4') :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
test_Load_127(i4) -{4,4}> test_Load_127(i9') :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 + -1 = i9'

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

Moved arithmethic from constraints to rhss.

test_Load_127(i4) -{4,4}> test_Load_127(i9') :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 + -1 = i9'
was transformed to
test_Load_127(i4) -{4,4}> test_Load_127(i4 + -1) :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 + -1 = i9'

(32) Obligation:

IntTrs with 2 rules
Start term: main_New_2(static)
Considered paths: all paths from start
Rules:
test_Load_127(i4) -{4,4}> test_Load_127(i4 + -1) :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 + -1 = i9'
main_New_2(static) -{52,52}> test_Load_127(i4') :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1

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

Simplified expressions.

main_New_2(static) -{52,52}> test_Load_127(i4') :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 1 + 1 && 0 <= 1 && 0 < o5''' && 0 <= static && o5'1 = o5''' + 1 + -1 * 1 && 0 <= static'1 && 0 < 2 && o5'1 <= o5''' + 1 && 0 >= 0 && o5''' <= 1 + 1
was transformed to
main_New_2(static) -{52,52}> test_Load_127(i4') :|: static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 2 && 0 < o5''' && 0 <= static && o5'1 = o5''' && 0 <= static'1 && o5'1 <= o5''' + 1

test_Load_127(i4) -{4,4}> test_Load_127(i4 + -1) :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 + -1 = i9'
was transformed to
test_Load_127(i4) -{4,4}> test_Load_127(i4 - 1) :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 - 1 = i9'

(34) Obligation:

IntTrs with 2 rules
Start term: main_New_2(static)
Considered paths: all paths from start
Rules:
main_New_2(static) -{52,52}> test_Load_127(i4') :|: static'1 <= static''' + 1 && i4' <= 99 && -99 <= i4' && 0 <= static''' && 0 < o5'1 && static''' <= static + 2 && o5''' = 2 && 0 < o5''' && 0 <= static && o5'1 = o5''' && 0 <= static'1 && o5'1 <= o5''' + 1
test_Load_127(i4) -{4,4}> test_Load_127(i4 - 1) :|: i4 <= 99 && i9' <= 98 && 0 < i4 && i9' <= 99 && -99 <= i4 && -99 <= i9' && 0 <= i9' && 1 <= i4 && i4 - 1 = i9'

(35) koat Proof (EQUIVALENT transformation)

YES(?, 448)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 52) main_New_2(ar_0) -> Com_1(test_Load_127(i4')) [ static'1 <= static''' + 1 /\ i4' <= 99 /\ -99 <= i4' /\ 0 <= static''' /\ 0 < o5'1 /\ static''' <= ar_0 + 2 /\ o5''' = 2 /\ 0 < o5''' /\ 0 <= ar_0 /\ o5'1 = o5''' /\ 0 <= static'1 /\ o5'1 <= o5''' + 1 ]
(Comp: ?, Cost: 4) test_Load_127(ar_0) -> Com_1(test_Load_127(ar_0 - 1)) [ ar_0 <= 99 /\ i9' <= 98 /\ 0 < ar_0 /\ i9' <= 99 /\ -99 <= ar_0 /\ -99 <= i9' /\ 0 <= i9' /\ 1 <= ar_0 /\ ar_0 - 1 = i9' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_New_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: 1, Cost: 52) main_New_2(ar_0) -> Com_1(test_Load_127(i4')) [ static'1 <= static''' + 1 /\ i4' <= 99 /\ -99 <= i4' /\ 0 <= static''' /\ 0 < o5'1 /\ static''' <= ar_0 + 2 /\ o5''' = 2 /\ 0 < o5''' /\ 0 <= ar_0 /\ o5'1 = o5''' /\ 0 <= static'1 /\ o5'1 <= o5''' + 1 ]
(Comp: ?, Cost: 4) test_Load_127(ar_0) -> Com_1(test_Load_127(ar_0 - 1)) [ ar_0 <= 99 /\ i9' <= 98 /\ 0 < ar_0 /\ i9' <= 99 /\ -99 <= ar_0 /\ -99 <= i9' /\ 0 <= i9' /\ 1 <= ar_0 /\ ar_0 - 1 = i9' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_New_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_New_2) = 99
Pol(test_Load_127) = V_1
Pol(koat_start) = 99
orients all transitions weakly and the transition
test_Load_127(ar_0) -> Com_1(test_Load_127(ar_0 - 1)) [ ar_0 <= 99 /\ i9' <= 98 /\ 0 < ar_0 /\ i9' <= 99 /\ -99 <= ar_0 /\ -99 <= i9' /\ 0 <= i9' /\ 1 <= ar_0 /\ ar_0 - 1 = i9' ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 52) main_New_2(ar_0) -> Com_1(test_Load_127(i4')) [ static'1 <= static''' + 1 /\ i4' <= 99 /\ -99 <= i4' /\ 0 <= static''' /\ 0 < o5'1 /\ static''' <= ar_0 + 2 /\ o5''' = 2 /\ 0 < o5''' /\ 0 <= ar_0 /\ o5'1 = o5''' /\ 0 <= static'1 /\ o5'1 <= o5''' + 1 ]
(Comp: 99, Cost: 4) test_Load_127(ar_0) -> Com_1(test_Load_127(ar_0 - 1)) [ ar_0 <= 99 /\ i9' <= 98 /\ 0 < ar_0 /\ i9' <= 99 /\ -99 <= ar_0 /\ -99 <= i9' /\ 0 <= i9' /\ 1 <= ar_0 /\ ar_0 - 1 = i9' ]
(Comp: 1, Cost: 0) koat_start(ar_0) -> Com_1(main_New_2(ar_0)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 448

Time: 0.067 sec (SMT: 0.063 sec)

(36) BOUNDS(CONSTANT, 448)

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

Constructed TerminationGraph.

(38) Obligation:

Termination Graph based on JBC Program:
ClassAnalysis.ClassAnalysis.main(I)V: Graph of 1258 nodes with 0 SCCs.