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

0 JBC problem
↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 223 ms)
↳2 JBCTerminationGraph
    ↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(53)), 0 ms)
    ↳4 JBCComplexityEdges
        ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 217 ms)
        ↳6 WeightedIntTrs
        ↳7 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 230 ms)
        ↳8 WeightedIntTrs
    ↳9 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(53)), 10 ms)
    ↳10 JBCComplexityEdges
        ↳11 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 252 ms)
        ↳12 WeightedIntTrs
↳13 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 780 ms)
↳14 JBCTerminationGraph
    ↳15 TerminationGraphToComplexityProof (⇔, 118 ms)
    ↳16 BOUNDS(CONSTANT, 1111)

(0) Obligation:

Need to prove time_complexity of the following program:
package ClassAnalysis;

public class ClassAnalysis {
	A field;

	public static void main(String[] args) {
		Random.args = args;
		ClassAnalysis t = new ClassAnalysis();
		t.field = new A();
		t.field = new B();
		t.eval();
	}

	public void eval() {
		int x = Random.random() % 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;
	}
}


package ClassAnalysis;

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    final String string = args[index];
    index++;
    return string.length();
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

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


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

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

(4) Obligation:

Set of 91 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 91 jbc graph edges to a weighted ITS with 91 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 91 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_15(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_17(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_17(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_20(o2, env, static) -{0,0}> langle_clinit_rangle_New_22(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_22(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_31(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_33(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_33(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_35(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_35(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_41(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_43(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_46(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_46(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_48(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_48(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_49(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_49(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_52(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_52(o2, env, static) -{1,1}> main_Load_57(o2, env, static) :|: 0 < o2
main_Load_57(o2, env, static) -{0,0}> main_Load_58(o2, env, static) :|: 0 < o2
main_Load_58(o2, env, static) -{0,0}> main_Load_61(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_61(o2, env, static) -{0,0}> main_Load_62(o2, env, static) :|: 0 < o2
main_Load_62(o2, env, static) -{0,0}> main_Load_63(o2, env, static) :|: 0 < o2
main_Load_63(o2, env, static) -{1,1}> main_FieldAccess_65(o2, env, static) :|: 0 < o2
main_FieldAccess_65(o2, env, static) -{0,0}> main_FieldAccess_67(o2, env, static) :|: 0 < o2
main_FieldAccess_67(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_69(o2, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ConstantStackPush_69(o2, NULL, iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_70(iconst_0, o2, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
langle_clinit_rangle_FieldAccess_70(iconst_0, o2, NULL, env, static) -{1,1}> langle_clinit_rangle_Return_71(o2, NULL, iconst_0, env, static') :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 <= static && static' <= static + iconst_0
langle_clinit_rangle_Return_71(o2, NULL, iconst_0, env, static) -{1,1}> main_FieldAccess_72(o2, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
main_FieldAccess_72(o2, NULL, iconst_0, env, static) -{1,1}> main_New_73(o2, iconst_0, env, static') :|: NULL = 0 && 0 < o2 && 0 <= o2 && iconst_0 = 0 && 0 <= static && static' <= static + o2
main_New_73(o2, iconst_0, env, static) -{1,1}> main_Duplicate_74(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && o7 = 1 && iconst_0 = 0 && 0 < o7
main_Duplicate_74(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_InvokeMethod_75(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_InvokeMethod_75(o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Load_76(o7, o2, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_Load_76(o7, o2, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o7, o2, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_InvokeMethod_78(o7, o2, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Return_80(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_Return_80(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Store_83(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_Store_83(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Load_84(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_Load_84(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_New_85(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_New_85(o2, o7, iconst_0, NULL, env, static) -{0,0}> main_New_86(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_New_86(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Duplicate_87(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && o8 = 1 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_Duplicate_87(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_InvokeMethod_88(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_InvokeMethod_88(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Load_89(o8, o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_Load_89(o8, o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_90(o8, o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_90(o8, o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Return_91(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_Return_91(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_FieldAccess_92(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_FieldAccess_92(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_Load_95(o2, o7', iconst_0, o8, env, static) :|: NULL = 0 && 0 < o2 && o7' = o7 + o8 && iconst_0 = 0 && o7' <= o7 + o8 && 0 < o7' && 0 < o7 && 0 < o8
main_Load_95(o2, o7, iconst_0, o8, env, static) -{1,1}> main_New_98(o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_New_98(o2, o7, iconst_0, o8, env, static) -{0,0}> main_New_100(o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_New_100(o2, o7, iconst_0, o8, env, static) -{1,1}> main_Duplicate_103(o2, o7, o10, iconst_0, o8, env, static) :|: o10 = 1 && 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_Duplicate_103(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_InvokeMethod_105(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_InvokeMethod_105(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Load_107(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Load_107(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_115(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_115(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Load_117(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Load_117(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_119(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_119(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Return_120(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Return_120(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Return_122(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Return_122(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_FieldAccess_123(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_FieldAccess_123(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_Load_126(o2, o7', iconst_0, o10, env, static) :|: 0 < o2 && o7' = o7 + o10 + -1 * o8 && o7' <= o7 + o10 && iconst_0 = 0 && 0 < o10 && 0 < o7' && 0 < o7 && 0 < o8
main_Load_126(o2, o7, iconst_0, o10, env, static) -{1,1}> main_InvokeMethod_128(o2, o7, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
main_InvokeMethod_128(o2, o7, iconst_0, o10, env, static) -{1,1}> eval_InvokeMethod_129(o7, o2, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
eval_InvokeMethod_129(o7, o2, iconst_0, o10, env, static) -{1,1}> random_FieldAccess_130(o7, o2, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
random_FieldAccess_130(o7, o2, iconst_0, o10, env, static) -{1,1}> random_FieldAccess_131(o2, o7, iconst_0, o10, env, static) :|: 0 < o2 && o2 <= static && 0 <= o2 && iconst_0 = 0 && 0 <= static && 0 < o10 && 0 < o7
random_FieldAccess_131(o2, o7, iconst_0, o10, env, static) -{1,1}> random_ArrayAccess_132(o2, iconst_0, o7, o10, env, static) :|: 0 < o2 && -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && 0 < o10 && iconst_0 <= static && 0 < o7
random_ArrayAccess_132(a6, iconst_0, o7, o10, env, static) -{0,0}> random_ArrayAccess_134(a6, iconst_0, o7, i3, o10, env, static) :|: i3 < a6 && 0 <= i3 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7
random_ArrayAccess_134(a6, iconst_0, o7, iconst_0, o10, env, static) -{0,0}> random_ArrayAccess_136(a6, iconst_0, o7, o10, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7
random_ArrayAccess_134(a6, iconst_0, o7, i4, o10, env, static) -{0,0}> random_ArrayAccess_137(a6, iconst_0, o7, i4, o10, env, static) :|: iconst_0 = 0 && 0 <= i4 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_ArrayAccess_137(a6, iconst_0, o7, i4, o10, env, static) -{1,1}> random_Store_141(o18, o7, a6, iconst_0, o10, i4, env, static) :|: iconst_0 < i4 && 0 <= o18 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4 && o18 < a6
random_Store_141(o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_FieldAccess_143(o18, o7, a6, iconst_0, o10, i4, env, static) :|: 0 <= o18 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_FieldAccess_143(o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_ConstantStackPush_147(iconst_0, o18, o7, a6, o10, i4, env, static) :|: -1 * static <= iconst_0 && 0 <= o18 && iconst_0 = 0 && 0 <= static && 0 < a6 && 0 < o10 && iconst_0 <= static && 0 < o7 && 1 <= i4
random_ConstantStackPush_147(iconst_0, o18, o7, a6, o10, i4, env, static) -{1,1}> random_IntArithmetic_150(iconst_0, iconst_1, o18, o7, a6, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_IntArithmetic_150(iconst_0, iconst_1, o18, o7, a6, o10, i4, env, static) -{1,1}> random_FieldAccess_152(iconst_1, o18, o7, a6, iconst_0, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_FieldAccess_152(iconst_1, o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_Load_158(o18, o7, a6, iconst_1, o10, i4, env, static') :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 <= static && 0 < a6 && 0 < o10 && static' <= static + iconst_1 && 0 < o7 && 1 <= i4
random_Load_158(o18, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> random_InvokeMethod_163(o18, o7, a6, iconst_1, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_163(o21, o7, a6, iconst_1, o10, i4, env, static) -{0,0}> random_InvokeMethod_169(o21, o7, a6, iconst_1, o10, i4, env, static) :|: 0 <= o21 && iconst_1 = 1 && 0 < o21 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_163(NULL, o7, a6, iconst_1, o10, i4, env, static) -{0,0}> random_InvokeMethod_170(NULL, o7, a6, iconst_1, o10, i4, env, static) :|: NULL = 0 && iconst_1 = 1 && 0 <= NULL && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_169(o21, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> random_Return_173(i7, o7, a6, iconst_1, o10, i4, env, static) :|: i7 <= o21 && iconst_1 = 1 && 0 < o21 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
random_Return_173(i7, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_ConstantStackPush_178(i7, o7, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
eval_ConstantStackPush_178(i7, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_IntArithmetic_181(i7, iconst_100, o7, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && iconst_100 = 100 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
eval_IntArithmetic_181(i7, iconst_100, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Store_185(i8, o7, a6, iconst_1, o10, i4, env, static) :|: i7 % iconst_100 = i8 && iconst_1 = 1 && iconst_100 = 100 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 <= i7 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Store_185(i8, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Load_190(o7, i8, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Load_190(o7, i8, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_FieldAccess_193(o7, i8, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_FieldAccess_193(o7, i8, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Load_196(o10, i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Load_196(o10, i8, a6, iconst_1, i4, env, static) -{1,1}> eval_InvokeMethod_205(o10, i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && i8 <= 99 && 1 <= i4
eval_InvokeMethod_205(o10, i8, a6, iconst_1, i4, env, static) -{1,1}> test_Load_208(i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && i8 <= 99 && 1 <= i4
test_Load_208(i8, a6, iconst_1, i4, env, static) -{1,1}> test_LE_212(i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 <= i8 && i8 <= 99 && 1 <= i4
test_LE_212(iconst_0, a6, iconst_1, i4, env, static) -{0,0}> test_LE_221(iconst_0, a6, iconst_1, i4, env, static) :|: iconst_0 <= 99 && 0 <= iconst_0 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 1 <= i4
test_LE_212(i10, a6, iconst_1, i4, env, static) -{0,0}> test_LE_222(i10, a6, iconst_1, i4, env, static) :|: 0 <= i10 && 1 <= i10 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && 1 <= i4
test_LE_222(i10, a6, iconst_1, i4, env, static) -{1,1}> test_Inc_230(i10, a6, iconst_1, i4, env, static) :|: 1 <= i10 && 0 < i10 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && 1 <= i4
test_Inc_230(i10, a6, iconst_1, i4, env, static) -{1,1}> test_JMP_250(i13, a6, iconst_1, i4, env, static) :|: 1 <= i10 && i13 <= 98 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && i10 + -1 = i13 && 1 <= i4 && 0 <= i13
test_JMP_250(i13, a6, iconst_1, i4, env, static) -{1,1}> test_Load_278(i13, a6, iconst_1, i4, env, static) :|: i13 <= 98 && iconst_1 = 1 && 0 < a6 && 1 <= i4 && 0 <= i13
test_Load_278(i13, a6, iconst_1, i4, env, static) -{0,0}> test_Load_208(i13, a6, iconst_1, i4, env, static) :|: i13 <= 98 && iconst_1 = 1 && i13 <= 99 && 0 < a6 && 1 <= i4 && 0 <= i13

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

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

(8) Obligation:

IntTrs with 91 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_15(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_17(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_17(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_20(o2, env, static) -{0,0}> langle_clinit_rangle_New_22(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_22(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_31(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_33(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_33(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_35(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_35(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_41(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_43(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_46(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_46(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_48(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_48(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_49(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_49(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_52(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_52(o2, env, static) -{1,1}> main_Load_57(o2, env, static) :|: 0 < o2
main_Load_57(o2, env, static) -{0,0}> main_Load_58(o2, env, static) :|: 0 < o2
main_Load_58(o2, env, static) -{0,0}> main_Load_61(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_61(o2, env, static) -{0,0}> main_Load_62(o2, env, static) :|: 0 < o2
main_Load_62(o2, env, static) -{0,0}> main_Load_63(o2, env, static) :|: 0 < o2
main_Load_63(o2, env, static) -{1,1}> main_FieldAccess_65(o2, env, static) :|: 0 < o2
main_FieldAccess_65(o2, env, static) -{0,0}> main_FieldAccess_67(o2, env, static) :|: 0 < o2
main_FieldAccess_67(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_69(o2, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ConstantStackPush_69(o2, NULL, iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_70(iconst_0, o2, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
langle_clinit_rangle_FieldAccess_70(iconst_0, o2, NULL, env, static) -{1,1}> langle_clinit_rangle_Return_71(o2, NULL, iconst_0, env, static') :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 <= static && static' <= static + iconst_0
langle_clinit_rangle_Return_71(o2, NULL, iconst_0, env, static) -{1,1}> main_FieldAccess_72(o2, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
main_FieldAccess_72(o2, NULL, iconst_0, env, static) -{1,1}> main_New_73(o2, iconst_0, env, static') :|: NULL = 0 && 0 < o2 && 0 <= o2 && iconst_0 = 0 && 0 <= static && static' <= static + o2
main_New_73(o2, iconst_0, env, static) -{1,1}> main_Duplicate_74(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && o7 = 1 && iconst_0 = 0 && 0 < o7
main_Duplicate_74(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_InvokeMethod_75(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_InvokeMethod_75(o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Load_76(o7, o2, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_Load_76(o7, o2, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o7, o2, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_InvokeMethod_78(o7, o2, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Return_80(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_Return_80(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Store_83(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_Store_83(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Load_84(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_Load_84(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_New_85(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_New_85(o2, o7, iconst_0, NULL, env, static) -{0,0}> main_New_86(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_New_86(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Duplicate_87(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && o8 = 1 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_Duplicate_87(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_InvokeMethod_88(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_InvokeMethod_88(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Load_89(o8, o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_Load_89(o8, o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_90(o8, o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_90(o8, o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Return_91(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_Return_91(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_FieldAccess_92(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_FieldAccess_92(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_Load_95(o2, o7', iconst_0, o8, env, static) :|: NULL = 0 && 0 < o2 && o7' = o7 + o8 && iconst_0 = 0 && o7' <= o7 + o8 && 0 < o7' && 0 < o7 && 0 < o8
main_Load_95(o2, o7, iconst_0, o8, env, static) -{1,1}> main_New_98(o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_New_98(o2, o7, iconst_0, o8, env, static) -{0,0}> main_New_100(o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_New_100(o2, o7, iconst_0, o8, env, static) -{1,1}> main_Duplicate_103(o2, o7, o10, iconst_0, o8, env, static) :|: o10 = 1 && 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_Duplicate_103(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_InvokeMethod_105(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_InvokeMethod_105(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Load_107(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Load_107(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_115(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_115(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Load_117(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Load_117(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_119(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_119(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Return_120(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Return_120(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Return_122(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Return_122(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_FieldAccess_123(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_FieldAccess_123(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_Load_126(o2, o7', iconst_0, o10, env, static) :|: 0 < o2 && o7' = o7 + o10 + -1 * o8 && o7' <= o7 + o10 && iconst_0 = 0 && 0 < o10 && 0 < o7' && 0 < o7 && 0 < o8
main_Load_126(o2, o7, iconst_0, o10, env, static) -{1,1}> main_InvokeMethod_128(o2, o7, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
main_InvokeMethod_128(o2, o7, iconst_0, o10, env, static) -{1,1}> eval_InvokeMethod_129(o7, o2, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
eval_InvokeMethod_129(o7, o2, iconst_0, o10, env, static) -{1,1}> random_FieldAccess_130(o7, o2, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
random_FieldAccess_130(o7, o2, iconst_0, o10, env, static) -{1,1}> random_FieldAccess_131(o2, o7, iconst_0, o10, env, static) :|: 0 < o2 && o2 <= static && 0 <= o2 && iconst_0 = 0 && 0 <= static && 0 < o10 && 0 < o7
random_FieldAccess_131(o2, o7, iconst_0, o10, env, static) -{1,1}> random_ArrayAccess_132(o2, iconst_0, o7, o10, env, static) :|: 0 < o2 && -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && 0 < o10 && iconst_0 <= static && 0 < o7
random_ArrayAccess_132(a6, iconst_0, o7, o10, env, static) -{0,0}> random_ArrayAccess_134(a6, iconst_0, o7, i3, o10, env, static) :|: i3 < a6 && 0 <= i3 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7
random_ArrayAccess_134(a6, iconst_0, o7, iconst_0, o10, env, static) -{0,0}> random_ArrayAccess_136(a6, iconst_0, o7, o10, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7
random_ArrayAccess_134(a6, iconst_0, o7, i4, o10, env, static) -{0,0}> random_ArrayAccess_137(a6, iconst_0, o7, i4, o10, env, static) :|: iconst_0 = 0 && 0 <= i4 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_ArrayAccess_137(a6, iconst_0, o7, i4, o10, env, static) -{1,1}> random_Store_141(o18, o7, a6, iconst_0, o10, i4, env, static) :|: iconst_0 < i4 && 0 <= o18 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4 && o18 < a6
random_Store_141(o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_FieldAccess_143(o18, o7, a6, iconst_0, o10, i4, env, static) :|: 0 <= o18 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_FieldAccess_143(o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_ConstantStackPush_147(iconst_0, o18, o7, a6, o10, i4, env, static) :|: -1 * static <= iconst_0 && 0 <= o18 && iconst_0 = 0 && 0 <= static && 0 < a6 && 0 < o10 && iconst_0 <= static && 0 < o7 && 1 <= i4
random_ConstantStackPush_147(iconst_0, o18, o7, a6, o10, i4, env, static) -{1,1}> random_IntArithmetic_150(iconst_0, iconst_1, o18, o7, a6, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_IntArithmetic_150(iconst_0, iconst_1, o18, o7, a6, o10, i4, env, static) -{1,1}> random_FieldAccess_152(iconst_1, o18, o7, a6, iconst_0, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_FieldAccess_152(iconst_1, o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_Load_158(o18, o7, a6, iconst_1, o10, i4, env, static') :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 <= static && 0 < a6 && 0 < o10 && static' <= static + iconst_1 && 0 < o7 && 1 <= i4
random_Load_158(o18, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> random_InvokeMethod_163(o18, o7, a6, iconst_1, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_163(o21, o7, a6, iconst_1, o10, i4, env, static) -{0,0}> random_InvokeMethod_169(o21, o7, a6, iconst_1, o10, i4, env, static) :|: 0 <= o21 && iconst_1 = 1 && 0 < o21 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_163(NULL, o7, a6, iconst_1, o10, i4, env, static) -{0,0}> random_InvokeMethod_170(NULL, o7, a6, iconst_1, o10, i4, env, static) :|: NULL = 0 && iconst_1 = 1 && 0 <= NULL && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_169(o21, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> random_Return_173(i7, o7, a6, iconst_1, o10, i4, env, static) :|: i7 <= o21 && iconst_1 = 1 && 0 < o21 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
random_Return_173(i7, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_ConstantStackPush_178(i7, o7, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
eval_ConstantStackPush_178(i7, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_IntArithmetic_181(i7, iconst_100, o7, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && iconst_100 = 100 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
eval_IntArithmetic_181(i7, iconst_100, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Store_185(i8, o7, a6, iconst_1, o10, i4, env, static) :|: i8 < iconst_100 && iconst_1 = 1 && iconst_100 = 100 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 <= i7 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Store_185(i8, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Load_190(o7, i8, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Load_190(o7, i8, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_FieldAccess_193(o7, i8, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_FieldAccess_193(o7, i8, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Load_196(o10, i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Load_196(o10, i8, a6, iconst_1, i4, env, static) -{1,1}> eval_InvokeMethod_205(o10, i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && i8 <= 99 && 1 <= i4
eval_InvokeMethod_205(o10, i8, a6, iconst_1, i4, env, static) -{1,1}> test_Load_208(i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && i8 <= 99 && 1 <= i4
test_Load_208(i8, a6, iconst_1, i4, env, static) -{1,1}> test_LE_212(i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 <= i8 && i8 <= 99 && 1 <= i4
test_LE_212(iconst_0, a6, iconst_1, i4, env, static) -{0,0}> test_LE_221(iconst_0, a6, iconst_1, i4, env, static) :|: iconst_0 <= 99 && 0 <= iconst_0 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 1 <= i4
test_LE_212(i10, a6, iconst_1, i4, env, static) -{0,0}> test_LE_222(i10, a6, iconst_1, i4, env, static) :|: 0 <= i10 && 1 <= i10 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && 1 <= i4
test_LE_222(i10, a6, iconst_1, i4, env, static) -{1,1}> test_Inc_230(i10, a6, iconst_1, i4, env, static) :|: 1 <= i10 && 0 < i10 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && 1 <= i4
test_Inc_230(i10, a6, iconst_1, i4, env, static) -{1,1}> test_JMP_250(i13, a6, iconst_1, i4, env, static) :|: 1 <= i10 && i13 <= 98 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && i10 + -1 = i13 && 1 <= i4 && 0 <= i13
test_JMP_250(i13, a6, iconst_1, i4, env, static) -{1,1}> test_Load_278(i13, a6, iconst_1, i4, env, static) :|: i13 <= 98 && iconst_1 = 1 && 0 < a6 && 1 <= i4 && 0 <= i13
test_Load_278(i13, a6, iconst_1, i4, env, static) -{0,0}> test_Load_208(i13, a6, iconst_1, i4, env, static) :|: i13 <= 98 && iconst_1 = 1 && i13 <= 99 && 0 < a6 && 1 <= i4 && 0 <= i13

(9) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(53)) transformation)

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

(10) Obligation:

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

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

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

(12) Obligation:

IntTrs with 88 rules
Start term: main_Load_1(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_15(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_17(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_17(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_20(o2, env, static) -{0,0}> langle_clinit_rangle_New_22(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_22(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_31(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_33(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_33(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_35(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_35(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_41(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_43(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_46(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_46(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_48(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_48(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_49(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_49(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_52(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_52(o2, env, static) -{1,1}> main_Load_57(o2, env, static) :|: 0 < o2
main_Load_57(o2, env, static) -{0,0}> main_Load_58(o2, env, static) :|: 0 < o2
main_Load_58(o2, env, static) -{0,0}> main_Load_61(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_61(o2, env, static) -{0,0}> main_Load_62(o2, env, static) :|: 0 < o2
main_Load_62(o2, env, static) -{0,0}> main_Load_63(o2, env, static) :|: 0 < o2
main_Load_63(o2, env, static) -{1,1}> main_FieldAccess_65(o2, env, static) :|: 0 < o2
main_FieldAccess_65(o2, env, static) -{0,0}> main_FieldAccess_67(o2, env, static) :|: 0 < o2
main_FieldAccess_67(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_69(o2, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ConstantStackPush_69(o2, NULL, iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_70(iconst_0, o2, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
langle_clinit_rangle_FieldAccess_70(iconst_0, o2, NULL, env, static) -{1,1}> langle_clinit_rangle_Return_71(o2, NULL, iconst_0, env, static') :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 <= static && static' <= static + iconst_0
langle_clinit_rangle_Return_71(o2, NULL, iconst_0, env, static) -{1,1}> main_FieldAccess_72(o2, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0
main_FieldAccess_72(o2, NULL, iconst_0, env, static) -{1,1}> main_New_73(o2, iconst_0, env, static') :|: NULL = 0 && 0 < o2 && 0 <= o2 && iconst_0 = 0 && 0 <= static && static' <= static + o2
main_New_73(o2, iconst_0, env, static) -{1,1}> main_Duplicate_74(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && o7 = 1 && iconst_0 = 0 && 0 < o7
main_Duplicate_74(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_InvokeMethod_75(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_InvokeMethod_75(o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Load_76(o7, o2, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_Load_76(o7, o2, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_78(o7, o2, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_InvokeMethod_78(o7, o2, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Return_80(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
langle_init_rangle_Return_80(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Store_83(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_Store_83(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Load_84(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_Load_84(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_New_85(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_New_85(o2, o7, iconst_0, NULL, env, static) -{0,0}> main_New_86(o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7
main_New_86(o2, o7, iconst_0, NULL, env, static) -{1,1}> main_Duplicate_87(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && o8 = 1 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_Duplicate_87(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_InvokeMethod_88(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_InvokeMethod_88(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Load_89(o8, o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_Load_89(o8, o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_90(o8, o2, o7, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_90(o8, o2, o7, iconst_0, NULL, env, static) -{1,1}> langle_init_rangle_Return_91(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
langle_init_rangle_Return_91(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_FieldAccess_92(o2, o7, o8, iconst_0, NULL, env, static) :|: NULL = 0 && 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_FieldAccess_92(o2, o7, o8, iconst_0, NULL, env, static) -{1,1}> main_Load_95(o2, o7', iconst_0, o8, env, static) :|: NULL = 0 && 0 < o2 && o7' = o7 + o8 && iconst_0 = 0 && o7' <= o7 + o8 && 0 < o7' && 0 < o7 && 0 < o8
main_Load_95(o2, o7, iconst_0, o8, env, static) -{1,1}> main_New_98(o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_New_98(o2, o7, iconst_0, o8, env, static) -{0,0}> main_New_100(o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o7 && 0 < o8
main_New_100(o2, o7, iconst_0, o8, env, static) -{1,1}> main_Duplicate_103(o2, o7, o10, iconst_0, o8, env, static) :|: o10 = 1 && 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_Duplicate_103(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_InvokeMethod_105(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_InvokeMethod_105(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Load_107(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Load_107(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_115(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_115(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Load_117(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Load_117(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_119(o10, o2, o7, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_InvokeMethod_119(o10, o2, o7, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Return_120(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Return_120(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> langle_init_rangle_Return_122(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
langle_init_rangle_Return_122(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_FieldAccess_123(o2, o7, o10, iconst_0, o8, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7 && 0 < o8
main_FieldAccess_123(o2, o7, o10, iconst_0, o8, env, static) -{1,1}> main_Load_126(o2, o7', iconst_0, o10, env, static) :|: 0 < o2 && o7' = o7 + o10 + -1 * o8 && o7' <= o7 + o10 && iconst_0 = 0 && 0 < o10 && 0 < o7' && 0 < o7 && 0 < o8
main_Load_126(o2, o7, iconst_0, o10, env, static) -{1,1}> main_InvokeMethod_128(o2, o7, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
main_InvokeMethod_128(o2, o7, iconst_0, o10, env, static) -{1,1}> eval_InvokeMethod_129(o7, o2, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
eval_InvokeMethod_129(o7, o2, iconst_0, o10, env, static) -{1,1}> random_FieldAccess_130(o7, o2, iconst_0, o10, env, static) :|: 0 < o2 && iconst_0 = 0 && 0 < o10 && 0 < o7
random_FieldAccess_130(o7, o2, iconst_0, o10, env, static) -{1,1}> random_FieldAccess_131(o2, o7, iconst_0, o10, env, static) :|: 0 < o2 && o2 <= static && 0 <= o2 && iconst_0 = 0 && 0 <= static && 0 < o10 && 0 < o7
random_FieldAccess_131(o2, o7, iconst_0, o10, env, static) -{1,1}> random_ArrayAccess_132(o2, iconst_0, o7, o10, env, static) :|: 0 < o2 && -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && 0 < o10 && iconst_0 <= static && 0 < o7
random_ArrayAccess_132(a6, iconst_0, o7, o10, env, static) -{0,0}> random_ArrayAccess_134(a6, iconst_0, o7, i3, o10, env, static) :|: i3 < a6 && 0 <= i3 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7
random_ArrayAccess_134(a6, iconst_0, o7, i4, o10, env, static) -{0,0}> random_ArrayAccess_137(a6, iconst_0, o7, i4, o10, env, static) :|: iconst_0 = 0 && 0 <= i4 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_ArrayAccess_137(a6, iconst_0, o7, i4, o10, env, static) -{1,1}> random_Store_141(o18, o7, a6, iconst_0, o10, i4, env, static) :|: iconst_0 < i4 && 0 <= o18 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4 && o18 < a6
random_Store_141(o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_FieldAccess_143(o18, o7, a6, iconst_0, o10, i4, env, static) :|: 0 <= o18 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_FieldAccess_143(o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_ConstantStackPush_147(iconst_0, o18, o7, a6, o10, i4, env, static) :|: -1 * static <= iconst_0 && 0 <= o18 && iconst_0 = 0 && 0 <= static && 0 < a6 && 0 < o10 && iconst_0 <= static && 0 < o7 && 1 <= i4
random_ConstantStackPush_147(iconst_0, o18, o7, a6, o10, i4, env, static) -{1,1}> random_IntArithmetic_150(iconst_0, iconst_1, o18, o7, a6, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_IntArithmetic_150(iconst_0, iconst_1, o18, o7, a6, o10, i4, env, static) -{1,1}> random_FieldAccess_152(iconst_1, o18, o7, a6, iconst_0, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_FieldAccess_152(iconst_1, o18, o7, a6, iconst_0, o10, i4, env, static) -{1,1}> random_Load_158(o18, o7, a6, iconst_1, o10, i4, env, static') :|: 0 <= o18 && iconst_1 = 1 && iconst_0 = 0 && 0 <= static && 0 < a6 && 0 < o10 && static' <= static + iconst_1 && 0 < o7 && 1 <= i4
random_Load_158(o18, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> random_InvokeMethod_163(o18, o7, a6, iconst_1, o10, i4, env, static) :|: 0 <= o18 && iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_163(o21, o7, a6, iconst_1, o10, i4, env, static) -{0,0}> random_InvokeMethod_169(o21, o7, a6, iconst_1, o10, i4, env, static) :|: 0 <= o21 && iconst_1 = 1 && 0 < o21 && 0 < a6 && 0 < o10 && 0 < o7 && 1 <= i4
random_InvokeMethod_169(o21, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> random_Return_173(i7, o7, a6, iconst_1, o10, i4, env, static) :|: i7 <= o21 && iconst_1 = 1 && 0 < o21 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
random_Return_173(i7, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_ConstantStackPush_178(i7, o7, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
eval_ConstantStackPush_178(i7, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_IntArithmetic_181(i7, iconst_100, o7, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && iconst_100 = 100 && 0 < a6 && 0 < o10 && 0 <= i7 && 0 < o7 && 1 <= i4
eval_IntArithmetic_181(i7, iconst_100, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Store_185(i8, o7, a6, iconst_1, o10, i4, env, static) :|: i8 < iconst_100 && iconst_1 = 1 && iconst_100 = 100 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 <= i7 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Store_185(i8, o7, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Load_190(o7, i8, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Load_190(o7, i8, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_FieldAccess_193(o7, i8, a6, iconst_1, o10, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_FieldAccess_193(o7, i8, a6, iconst_1, o10, i4, env, static) -{1,1}> eval_Load_196(o10, i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && 0 < o7 && i8 <= 99 && 1 <= i4
eval_Load_196(o10, i8, a6, iconst_1, i4, env, static) -{1,1}> eval_InvokeMethod_205(o10, i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && i8 <= 99 && 1 <= i4
eval_InvokeMethod_205(o10, i8, a6, iconst_1, i4, env, static) -{1,1}> test_Load_208(i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 < o10 && 0 <= i8 && i8 <= 99 && 1 <= i4
test_Load_208(i8, a6, iconst_1, i4, env, static) -{1,1}> test_LE_212(i8, a6, iconst_1, i4, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 <= i8 && i8 <= 99 && 1 <= i4
test_LE_212(i10, a6, iconst_1, i4, env, static) -{0,0}> test_LE_222(i10, a6, iconst_1, i4, env, static) :|: 0 <= i10 && 1 <= i10 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && 1 <= i4
test_LE_222(i10, a6, iconst_1, i4, env, static) -{1,1}> test_Inc_230(i10, a6, iconst_1, i4, env, static) :|: 1 <= i10 && 0 < i10 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && 1 <= i4
test_Inc_230(i10, a6, iconst_1, i4, env, static) -{1,1}> test_JMP_250(i13, a6, iconst_1, i4, env, static) :|: 1 <= i10 && i13 <= 98 && i10 <= 99 && iconst_1 = 1 && 0 < a6 && i10 + -1 = i13 && 1 <= i4 && 0 <= i13
test_JMP_250(i13, a6, iconst_1, i4, env, static) -{1,1}> test_Load_278(i13, a6, iconst_1, i4, env, static) :|: i13 <= 98 && iconst_1 = 1 && 0 < a6 && 1 <= i4 && 0 <= i13
test_Load_278(i13, a6, iconst_1, i4, env, static) -{0,0}> test_Load_208(i13, a6, iconst_1, i4, env, static) :|: i13 <= 98 && iconst_1 = 1 && i13 <= 99 && 0 < a6 && 1 <= i4 && 0 <= i13

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

Constructed TerminationGraph.

(14) Obligation:

Termination Graph based on JBC Program:
ClassAnalysis.ClassAnalysis.main([Ljava/lang/String;)V: Graph of 1328 nodes with 0 SCCs.


(15) TerminationGraphToComplexityProof (EQUIVALENT transformation)

Proven constant complexity by absence of SCCs and edges with non-constant weight

(16) BOUNDS(CONSTANT, 1111)