time complexity proof of /tmp/tmp4QATpY/Overflow.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

        ↳23 LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

        ↳29 CESProof (⇔, 166 ms)

        ↳30 BOUNDS(CONSTANT, 10737418275)

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

↳32 JBCComplexityEdges

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

    ↳34 WeightedIntTrs

    ↳35 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 49 ms)

    ↳36 WeightedIntTrs

    ↳37 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 38 ms)

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class Overflow {

  // does not terminate for any value of i
  public static void overflow(int i) {
    while(i <= 2147483647) {
      i++;
    }
  }

  public static void main(String[] args) {
    Random.args = args;
    overflow(Random.random());
  }
}


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

  public static int random() {
    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:
Overflow.main([Ljava/lang/String;)V: Graph of 107 nodes with 1 SCC.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 58 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_6(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_28(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_28(o1, env, static) -{0,0}> langle_clinit_rangle_New_30(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_30(o1, env, static) -{0,0}> langle_clinit_rangle_New_31(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_31(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_32(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_32(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_46(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_46(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_47(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_47(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_48(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_48(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_50(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_50(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_51(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_51(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_52(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_52(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_56(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_56(o1, env, static) -{1,1}> main_Load_58(o1, env, static) :|: 0 < o1
main_Load_58(o1, env, static) -{0,0}> main_Load_59(o1, env, static) :|: 0 < o1
main_Load_59(o1, env, static) -{0,0}> main_Load_60(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_60(o1, env, static) -{0,0}> main_Load_61(o1, env, static) :|: 0 < o1
main_Load_61(o1, env, static) -{0,0}> main_Load_62(o1, env, static) :|: 0 < o1
main_Load_62(o1, env, static) -{1,1}> main_FieldAccess_63(o1, env, static) :|: 0 < o1
main_FieldAccess_63(o1, env, static) -{0,0}> main_FieldAccess_65(o1, env, static) :|: 0 < o1
main_FieldAccess_65(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) -{1,1}> langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static') :|: NULL = 0 && iconst_0 = 0 && 0 <= static && static' <= static + iconst_0 && 0 < o1
langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static) -{1,1}> main_FieldAccess_72(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
main_FieldAccess_72(o1, NULL, iconst_0, env, static) -{1,1}> main_InvokeMethod_74(o1, iconst_0, env, static') :|: static' <= static + o1 && NULL = 0 && 0 <= o1 && iconst_0 = 0 && 0 <= static && 0 < o1
main_InvokeMethod_74(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_75(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
random_FieldAccess_75(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_77(o1, iconst_0, env, static) :|: 0 <= o1 && o1 <= static && iconst_0 = 0 && 0 <= static && 0 < o1
random_FieldAccess_77(o1, iconst_0, env, static) -{1,1}> random_ArrayAccess_78(o1, iconst_0, env, static) :|: -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && iconst_0 <= static && 0 < o1
random_ArrayAccess_78(a6, iconst_0, env, static) -{0,0}> random_ArrayAccess_79(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
random_ArrayAccess_79(a6, iconst_0, iconst_0, env, static) -{0,0}> random_ArrayAccess_81(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
random_ArrayAccess_79(a6, iconst_0, i6, env, static) -{0,0}> random_ArrayAccess_82(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
random_ArrayAccess_82(a6, iconst_0, i6, env, static) -{1,1}> random_Store_86(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
random_Store_86(o8, a6, iconst_0, i6, env, static) -{1,1}> random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_0 = 0 && 0 < a6
random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) -{1,1}> random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && 0 < a6 && iconst_0 <= static
random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) -{1,1}> random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) -{1,1}> random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) -{1,1}> random_Load_98(o8, a6, iconst_1, i6, env, static') :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 <= static && 0 < a6 && static' <= static + iconst_1
random_Load_98(o8, a6, iconst_1, i6, env, static) -{1,1}> random_InvokeMethod_100(o8, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && 0 < a6
random_InvokeMethod_100(o12, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && iconst_1 = 1 && 0 < a6
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(NULL, a6, iconst_1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6
random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) -{1,1}> random_Return_105(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 < o12 && iconst_1 = 1 && i7 <= o12 && 0 < a6 && 0 <= i7
random_Return_105(i7, a6, iconst_1, i6, env, static) -{1,1}> main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) -{1,1}> overflow_Load_115(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_Load_115(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_GT_133(i7, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_GT_133(i15, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_135(i15, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && i15 <= 2147483647 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
overflow_GT_135(i15, iconst_2147483647, a6, iconst_1, i6, env, static) -{1,1}> overflow_Inc_145(i15, a6, iconst_1, i6, env, static) :|: 1 <= i6 && i15 <= iconst_2147483647 && i15 <= 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15
overflow_Inc_145(i15, a6, iconst_1, i6, env, static) -{1,1}> overflow_JMP_153(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && i15 + 1 = i18 && 1 <= i6 && i15 <= 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && i18 <= 2147483648
overflow_JMP_153(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_Load_156(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_Load_156(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_ConstantStackPush_165(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_ConstantStackPush_165(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_GT_176(i18, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_GT_176(i18, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_133(i18, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 0 <= i18 && 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648

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

obtained
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= 1 && 0 < 1
by chaining
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_6(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_28(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_28(o1, env, static) -{0,0}> langle_clinit_rangle_New_30(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_30(o1, env, static) -{0,0}> langle_clinit_rangle_New_31(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_31(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_32(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_32(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_46(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_46(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_47(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_47(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_48(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_48(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_50(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_50(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_51(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_51(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_52(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_52(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_56(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_56(o1, env, static) -{1,1}> main_Load_58(o1, env, static) :|: 0 < o1
main_Load_58(o1, env, static) -{0,0}> main_Load_59(o1, env, static) :|: 0 < o1
main_Load_59(o1, env, static) -{0,0}> main_Load_60(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_60(o1, env, static) -{0,0}> main_Load_61(o1, env, static) :|: 0 < o1
main_Load_61(o1, env, static) -{0,0}> main_Load_62(o1, env, static) :|: 0 < o1
main_Load_62(o1, env, static) -{1,1}> main_FieldAccess_63(o1, env, static) :|: 0 < o1
main_FieldAccess_63(o1, env, static) -{0,0}> main_FieldAccess_65(o1, env, static) :|: 0 < o1
main_FieldAccess_65(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) -{1,1}> langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static') :|: NULL = 0 && iconst_0 = 0 && 0 <= static && static' <= static + iconst_0 && 0 < o1
langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static) -{1,1}> main_FieldAccess_72(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
main_FieldAccess_72(o1, NULL, iconst_0, env, static) -{1,1}> main_InvokeMethod_74(o1, iconst_0, env, static') :|: static' <= static + o1 && NULL = 0 && 0 <= o1 && iconst_0 = 0 && 0 <= static && 0 < o1
main_InvokeMethod_74(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_75(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
random_FieldAccess_75(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_77(o1, iconst_0, env, static) :|: 0 <= o1 && o1 <= static && iconst_0 = 0 && 0 <= static && 0 < o1
random_FieldAccess_77(o1, iconst_0, env, static) -{1,1}> random_ArrayAccess_78(o1, iconst_0, env, static) :|: -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && iconst_0 <= static && 0 < o1
random_ArrayAccess_78(a6, iconst_0, env, static) -{0,0}> random_ArrayAccess_79(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5

obtained
random_ArrayAccess_79(a6, 0, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1
by chaining
random_ArrayAccess_79(a6, iconst_0, i6, env, static) -{0,0}> random_ArrayAccess_82(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
random_ArrayAccess_82(a6, iconst_0, i6, env, static) -{1,1}> random_Store_86(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
random_Store_86(o8, a6, iconst_0, i6, env, static) -{1,1}> random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_0 = 0 && 0 < a6
random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) -{1,1}> random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && 0 < a6 && iconst_0 <= static
random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) -{1,1}> random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) -{1,1}> random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) -{1,1}> random_Load_98(o8, a6, iconst_1, i6, env, static') :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 <= static && 0 < a6 && static' <= static + iconst_1
random_Load_98(o8, a6, iconst_1, i6, env, static) -{1,1}> random_InvokeMethod_100(o8, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && 0 < a6

obtained
random_InvokeMethod_100(o12, a6, 1, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12
by chaining
random_InvokeMethod_100(o12, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && iconst_1 = 1 && 0 < a6
random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) -{1,1}> random_Return_105(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 < o12 && iconst_1 = 1 && i7 <= o12 && 0 < a6 && 0 <= i7
random_Return_105(i7, a6, iconst_1, i6, env, static) -{1,1}> main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) -{1,1}> overflow_Load_115(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_Load_115(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_GT_133(i7, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7

obtained
overflow_GT_133(i15, 2147483647, a6, 1, i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18'
by chaining
overflow_GT_133(i15, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_135(i15, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && i15 <= 2147483647 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15
overflow_GT_135(i15, iconst_2147483647, a6, iconst_1, i6, env, static) -{1,1}> overflow_Inc_145(i15, a6, iconst_1, i6, env, static) :|: 1 <= i6 && i15 <= iconst_2147483647 && i15 <= 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15
overflow_Inc_145(i15, a6, iconst_1, i6, env, static) -{1,1}> overflow_JMP_153(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && i15 + 1 = i18 && 1 <= i6 && i15 <= 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && i18 <= 2147483648
overflow_JMP_153(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_Load_156(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_Load_156(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_ConstantStackPush_165(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_ConstantStackPush_165(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_GT_176(i18, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_GT_176(i18, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_133(i18, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 0 <= i18 && 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648

(8) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= 1 && 0 < 1
random_ArrayAccess_79(a6, iconst_0, iconst_0, env, static) -{0,0}> random_ArrayAccess_81(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
random_ArrayAccess_79(a6, 0, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(NULL, a6, iconst_1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6
random_InvokeMethod_100(o12, a6, 1, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
overflow_GT_133(i15, 2147483647, a6, 1, i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18'

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

Moved arithmethic from lhss to constraints.

random_ArrayAccess_79(a6, 0, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1
was transformed to
random_ArrayAccess_79(a6, x, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1 && x = 0

random_InvokeMethod_100(o12, a6, 1, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12
was transformed to
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12 && x = 1

overflow_GT_133(i15, 2147483647, a6, 1, i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18'
was transformed to
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1

(10) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
random_ArrayAccess_79(a6, x, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1 && x = 0
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12 && x = 1
random_ArrayAccess_79(a6, iconst_0, iconst_0, env, static) -{0,0}> random_ArrayAccess_81(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= 1 && 0 < 1
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(NULL, a6, iconst_1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6

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

Linearized lhss.

random_ArrayAccess_79(a6, iconst_0, iconst_0, env, static) -{0,0}> random_ArrayAccess_81(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
was transformed to
random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

(12) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12 && x = 1
random_ArrayAccess_79(a6, x, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1 && x = 0
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= 1 && 0 < 1
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(NULL, a6, iconst_1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6

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

Moved arithmethic from constraints to rhss.

random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1
was transformed to
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1

overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
was transformed to
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, 2147483647, a6, 1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16

random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(NULL, a6, iconst_1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6
was transformed to
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(0, a6, 1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6

(14) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1
random_ArrayAccess_79(a6, x, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1 && x = 0
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12 && x = 1
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= 1 && 0 < 1
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, 2147483647, a6, 1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(0, a6, 1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6

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

Simplified expressions.

random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12 && x = 1
was transformed to
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && x = 1

main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= 1 && 0 < 1
was transformed to
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 <= static'3

(16) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 <= static'3
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && x = 1
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1
random_ArrayAccess_79(a6, x, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1 && x = 0
random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, 2147483647, a6, 1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(0, a6, 1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6

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

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

(18) Obligation:

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

(20) Obligation:

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

Moved arithmethic from lhss to constraints.

(22) Obligation:

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

Linearized lhss.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1
random_ArrayAccess_79(a6, x, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1 && x = 0
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && 0 <= o12 && x = 1
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= 1 && 0 < 1
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, 2147483647, a6, 1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(0, a6, 1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6

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

Simplified expressions.

(28) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{23,23}> random_ArrayAccess_79(o1, 0, i5', env, static'3) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o1 && 0 <= static'2 && i5' < o1 && static'2 <= static'1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && -1 * static'3 <= 0 && 0 <= static''' && 0 <= static'3
random_InvokeMethod_100(o12, a6, x, i6, env, static) -{5,5}> overflow_GT_133(i7', iconst_2147483647', a6, 1, i6, env, static) :|: 0 < o12 && 0 <= i7' && i7' <= o12 && 0 < a6 && 1 <= i6 && x = 1
overflow_GT_133(i15, x, a6, x', i6, env, static) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647 && x' = 1
random_ArrayAccess_79(a6, x, i6, env, static) -{7,7}> random_InvokeMethod_100(o8', a6, 1, i6, env, static'4) :|: 0 <= i6 && 0 < a6 && 1 <= i6 && 0 <= static && 0 <= o8' && o8' < a6 && -1 * static <= 0 && static'4 <= static + 1 && x = 0
random_ArrayAccess_79(a6, iconst_0, x, env, static) -{0,0}> random_ArrayAccess_81(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
overflow_GT_133(i16, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_136(i16, 2147483647, a6, 1, i6, env, static) :|: 1 <= i6 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 <= i16 && 0 < a6 && 2147483648 <= i16
random_InvokeMethod_100(NULL, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_102(0, a6, 1, i6, env, static) :|: NULL = 0 && 1 <= i6 && iconst_1 = 1 && 0 <= NULL && 0 < a6

(29) CESProof (EQUIVALENT transformation)

proved upper bound 10737418275 using cofloco

(30) BOUNDS(CONSTANT, 10737418275)

(31) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(48)) transformation)

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

(32) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(34) Obligation:

IntTrs with 55 rules
Start term: main_Load_1(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_6(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_28(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_28(o1, env, static) -{0,0}> langle_clinit_rangle_New_30(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_30(o1, env, static) -{0,0}> langle_clinit_rangle_New_31(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_31(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_32(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_32(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_46(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_46(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_47(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_47(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_48(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_48(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_50(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_50(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_51(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_51(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_52(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_52(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_56(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_56(o1, env, static) -{1,1}> main_Load_58(o1, env, static) :|: 0 < o1
main_Load_58(o1, env, static) -{0,0}> main_Load_59(o1, env, static) :|: 0 < o1
main_Load_59(o1, env, static) -{0,0}> main_Load_60(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_60(o1, env, static) -{0,0}> main_Load_61(o1, env, static) :|: 0 < o1
main_Load_61(o1, env, static) -{0,0}> main_Load_62(o1, env, static) :|: 0 < o1
main_Load_62(o1, env, static) -{1,1}> main_FieldAccess_63(o1, env, static) :|: 0 < o1
main_FieldAccess_63(o1, env, static) -{0,0}> main_FieldAccess_65(o1, env, static) :|: 0 < o1
main_FieldAccess_65(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) -{1,1}> langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static') :|: NULL = 0 && iconst_0 = 0 && 0 <= static && static' <= static + iconst_0 && 0 < o1
langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static) -{1,1}> main_FieldAccess_72(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
main_FieldAccess_72(o1, NULL, iconst_0, env, static) -{1,1}> main_InvokeMethod_74(o1, iconst_0, env, static') :|: static' <= static + o1 && NULL = 0 && 0 <= o1 && iconst_0 = 0 && 0 <= static && 0 < o1
main_InvokeMethod_74(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_75(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
random_FieldAccess_75(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_77(o1, iconst_0, env, static) :|: 0 <= o1 && o1 <= static && iconst_0 = 0 && 0 <= static && 0 < o1
random_FieldAccess_77(o1, iconst_0, env, static) -{1,1}> random_ArrayAccess_78(o1, iconst_0, env, static) :|: -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && iconst_0 <= static && 0 < o1
random_ArrayAccess_78(a6, iconst_0, env, static) -{0,0}> random_ArrayAccess_79(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
random_ArrayAccess_79(a6, iconst_0, i6, env, static) -{0,0}> random_ArrayAccess_82(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
random_ArrayAccess_82(a6, iconst_0, i6, env, static) -{1,1}> random_Store_86(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
random_Store_86(o8, a6, iconst_0, i6, env, static) -{1,1}> random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_0 = 0 && 0 < a6
random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) -{1,1}> random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && 0 < a6 && iconst_0 <= static
random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) -{1,1}> random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) -{1,1}> random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) -{1,1}> random_Load_98(o8, a6, iconst_1, i6, env, static') :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 <= static && 0 < a6 && static' <= static + iconst_1
random_Load_98(o8, a6, iconst_1, i6, env, static) -{1,1}> random_InvokeMethod_100(o8, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && 0 < a6
random_InvokeMethod_100(o12, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && iconst_1 = 1 && 0 < a6
random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) -{1,1}> random_Return_105(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 < o12 && iconst_1 = 1 && i7 <= o12 && 0 < a6 && 0 <= i7
random_Return_105(i7, a6, iconst_1, i6, env, static) -{1,1}> main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) -{1,1}> overflow_Load_115(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_Load_115(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_GT_133(i7, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_GT_133(i15, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_135(i15, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && i15 <= 2147483647 && iconst_2147483647 = 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15
overflow_GT_135(i15, iconst_2147483647, a6, iconst_1, i6, env, static) -{1,1}> overflow_Inc_145(i15, a6, iconst_1, i6, env, static) :|: 1 <= i6 && i15 <= iconst_2147483647 && i15 <= 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15
overflow_Inc_145(i15, a6, iconst_1, i6, env, static) -{1,1}> overflow_JMP_153(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && i15 + 1 = i18 && 1 <= i6 && i15 <= 2147483647 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && i18 <= 2147483648
overflow_JMP_153(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_Load_156(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_Load_156(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_ConstantStackPush_165(i18, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_ConstantStackPush_165(i18, a6, iconst_1, i6, env, static) -{1,1}> overflow_GT_176(i18, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648
overflow_GT_176(i18, iconst_2147483647, a6, iconst_1, i6, env, static) -{0,0}> overflow_GT_133(i18, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 0 <= i18 && 1 <= i18 && 1 <= i6 && iconst_1 = 1 && 0 < a6 && i18 <= 2147483648

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

obtained
main_Load_1(o1, env, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, 1, i5', env, static'4) :|: static'1 <= static''' + 1 && 0 <= i7' && 0 <= 2 && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= o8' && 0 <= i5' && 0 <= 1 && 0 < 1 && static'4 <= static'3 + 1
by chaining
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_6(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_16(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_26(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_28(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_28(o1, env, static) -{0,0}> langle_clinit_rangle_New_30(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_30(o1, env, static) -{0,0}> langle_clinit_rangle_New_31(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_31(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_32(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_32(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_34(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_37(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_46(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_46(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_47(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_47(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_48(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_48(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_50(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_50(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_51(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_51(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_52(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_52(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_54(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_56(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_56(o1, env, static) -{1,1}> main_Load_58(o1, env, static) :|: 0 < o1
main_Load_58(o1, env, static) -{0,0}> main_Load_59(o1, env, static) :|: 0 < o1
main_Load_59(o1, env, static) -{0,0}> main_Load_60(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_60(o1, env, static) -{0,0}> main_Load_61(o1, env, static) :|: 0 < o1
main_Load_61(o1, env, static) -{0,0}> main_Load_62(o1, env, static) :|: 0 < o1
main_Load_62(o1, env, static) -{1,1}> main_FieldAccess_63(o1, env, static) :|: 0 < o1
main_FieldAccess_63(o1, env, static) -{0,0}> main_FieldAccess_65(o1, env, static) :|: 0 < o1
main_FieldAccess_65(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ConstantStackPush_66(o1, NULL, iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
langle_clinit_rangle_FieldAccess_68(iconst_0, o1, NULL, env, static) -{1,1}> langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static') :|: NULL = 0 && iconst_0 = 0 && 0 <= static && static' <= static + iconst_0 && 0 < o1
langle_clinit_rangle_Return_70(o1, NULL, iconst_0, env, static) -{1,1}> main_FieldAccess_72(o1, NULL, iconst_0, env, static) :|: NULL = 0 && iconst_0 = 0 && 0 < o1
main_FieldAccess_72(o1, NULL, iconst_0, env, static) -{1,1}> main_InvokeMethod_74(o1, iconst_0, env, static') :|: static' <= static + o1 && NULL = 0 && 0 <= o1 && iconst_0 = 0 && 0 <= static && 0 < o1
main_InvokeMethod_74(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_75(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
random_FieldAccess_75(o1, iconst_0, env, static) -{1,1}> random_FieldAccess_77(o1, iconst_0, env, static) :|: 0 <= o1 && o1 <= static && iconst_0 = 0 && 0 <= static && 0 < o1
random_FieldAccess_77(o1, iconst_0, env, static) -{1,1}> random_ArrayAccess_78(o1, iconst_0, env, static) :|: -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && iconst_0 <= static && 0 < o1
random_ArrayAccess_78(a6, iconst_0, env, static) -{0,0}> random_ArrayAccess_79(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
random_ArrayAccess_79(a6, iconst_0, i6, env, static) -{0,0}> random_ArrayAccess_82(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
random_ArrayAccess_82(a6, iconst_0, i6, env, static) -{1,1}> random_Store_86(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
random_Store_86(o8, a6, iconst_0, i6, env, static) -{1,1}> random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_0 = 0 && 0 < a6
random_FieldAccess_88(o8, a6, iconst_0, i6, env, static) -{1,1}> random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && -1 * static <= iconst_0 && iconst_0 = 0 && 0 <= static && 0 < a6 && iconst_0 <= static
random_ConstantStackPush_91(iconst_0, o8, a6, i6, env, static) -{1,1}> random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_IntArithmetic_95(iconst_0, iconst_1, o8, a6, i6, env, static) -{1,1}> random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 < a6
random_FieldAccess_96(iconst_1, o8, a6, iconst_0, i6, env, static) -{1,1}> random_Load_98(o8, a6, iconst_1, i6, env, static') :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && iconst_0 = 0 && 0 <= static && 0 < a6 && static' <= static + iconst_1
random_Load_98(o8, a6, iconst_1, i6, env, static) -{1,1}> random_InvokeMethod_100(o8, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o8 && iconst_1 = 1 && 0 < a6
random_InvokeMethod_100(o12, a6, iconst_1, i6, env, static) -{0,0}> random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && iconst_1 = 1 && 0 < a6
random_InvokeMethod_101(o12, a6, iconst_1, i6, env, static) -{1,1}> random_Return_105(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && 0 < o12 && iconst_1 = 1 && i7 <= o12 && 0 < a6 && 0 <= i7
random_Return_105(i7, a6, iconst_1, i6, env, static) -{1,1}> main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
main_InvokeMethod_112(a6, i7, iconst_1, i6, env, static) -{1,1}> overflow_Load_115(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_Load_115(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7
overflow_ConstantStackPush_126(i7, a6, iconst_1, i6, env, static) -{1,1}> overflow_GT_133(i7, iconst_2147483647, a6, iconst_1, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i7

(36) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, env, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, 1, i5', env, static'4) :|: static'1 <= static''' + 1 && 0 <= i7' && 0 <= 2 && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= o8' && 0 <= i5' && 0 <= 1 && 0 < 1 && static'4 <= static'3 + 1
overflow_GT_133(i15, 2147483647, a6, 1, i6, env, static) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, 1, i6, env, static) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18'

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

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

main_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
overflow_GT_133(x1, x2, x3, x4, x5, x6, x7) → overflow_GT_133(x1, x2, x3, x5)

(38) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, i5') :|: static'1 <= static''' + 1 && 0 <= i7' && 0 <= 2 && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= o8' && 0 <= i5' && 0 <= 1 && 0 < 1 && static'4 <= static'3 + 1
overflow_GT_133(i15, 2147483647, a6, i6) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18'

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

Moved arithmethic from lhss to constraints.

overflow_GT_133(i15, 2147483647, a6, i6) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18'
was transformed to
overflow_GT_133(i15, x, a6, i6) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647

(40) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
overflow_GT_133(i15, x, a6, i6) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647
main_Load_1(o1, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, i5') :|: static'1 <= static''' + 1 && 0 <= i7' && 0 <= 2 && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= o8' && 0 <= i5' && 0 <= 1 && 0 < 1 && static'4 <= static'3 + 1

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

Moved arithmethic from constraints to rhss.

overflow_GT_133(i15, x, a6, i6) -{5,5}> overflow_GT_133(i18', iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647
was transformed to
overflow_GT_133(i15, x, a6, i6) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647

(42) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
overflow_GT_133(i15, x, a6, i6) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647
main_Load_1(o1, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, i5') :|: static'1 <= static''' + 1 && 0 <= i7' && 0 <= 2 && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= o8' && 0 <= i5' && 0 <= 1 && 0 < 1 && static'4 <= static'3 + 1

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

Simplified expressions.

main_Load_1(o1, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, i5') :|: static'1 <= static''' + 1 && 0 <= i7' && 0 <= 2 && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 + 0 && 0 <= o1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 < 2 && 0 <= static'3 && 0 <= o8' && 0 <= i5' && 0 <= 1 && 0 < 1 && static'4 <= static'3 + 1
was transformed to
main_Load_1(o1, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, i5') :|: static'1 <= static''' + 1 && 0 <= i7' && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 <= static'3 && 0 <= i5' && static'4 <= static'3 + 1

(44) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
overflow_GT_133(i15, x, a6, i6) -{5,5}> overflow_GT_133(i15 + 1, iconst_21474836471, a6, i6) :|: i15 <= 2147483647 && i18' <= 2147483648 && 1 <= i6 && 0 < a6 && 0 <= i15 && 1 <= i18' && 0 <= i18' && i15 + 1 = i18' && x = 2147483647
main_Load_1(o1, static) -{35,35}> overflow_GT_133(i7', iconst_2147483647', o1, i5') :|: static'1 <= static''' + 1 && 0 <= i7' && 0 < o1 && 0 <= static'2 && 1 <= i5' && i7' <= o8' && o8' < o1 && i5' < o1 && 0 < o8' && -1 * static'3 <= 0 && static'2 <= static'1 && o1 <= static'3 && static''' <= static + 2 && 0 <= static'1 && static'3 <= static'2 + o1 && 0 <= static && 0 <= static''' && 0 <= static'3 && 0 <= i5' && static'4 <= static'3 + 1