(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++;
    }
  }

}


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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Overflow.overflow(I)V: Graph of 43 nodes with 1 SCC.


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

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

(4) Obligation:

Set of 39 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 39 jbc graph edges to a weighted ITS with 39 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 39 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_Load_1(i2, env, static) -{0,0}> overflow_Load_4(i2, env, static) :|: 0 >= 0
overflow_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> overflow_Load_41(i2, env, static) :|: 0 >= 0
overflow_Load_41(i2, env, static) -{0,0}> overflow_Load_42(i2, env, static) :|: 0 >= 0
overflow_Load_42(i2, env, static) -{0,0}> overflow_Load_44(i2, env, static) :|: 0 <= static
overflow_Load_44(i2, env, static) -{0,0}> overflow_Load_46(i2, env, static) :|: 0 >= 0
overflow_Load_46(i2, env, static) -{0,0}> overflow_Load_48(i2, env, static) :|: 0 >= 0
overflow_Load_48(i2, env, static) -{1,1}> overflow_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
overflow_ConstantStackPush_50(i2, env, static) -{1,1}> overflow_GT_54(i2, iconst_2147483647, env, static) :|: 0 >= 0
overflow_GT_54(i9, iconst_2147483647, env, static) -{0,0}> overflow_GT_55(i9, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && i9 <= 2147483647
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_GT_55(i9, iconst_2147483647, env, static) -{1,1}> overflow_Inc_58(i9, env, static) :|: i9 <= iconst_2147483647 && i9 <= 2147483647
overflow_Inc_58(i9, env, static) -{1,1}> overflow_JMP_62(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647 && i9 + 1 = i12
overflow_JMP_62(i9, i12, env, static) -{1,1}> overflow_Load_68(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_68(i9, i12, env, static) -{1,1}> overflow_ConstantStackPush_69(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i26, i25, iconst_2147483647, env, static) -{0,0}> overflow_GT_82(i26, i25, iconst_2147483647, env, static) :|: i25 <= 2147483647 && i25 <= 2147483648 && i26 <= 2147483647 && iconst_2147483647 = 2147483647 && i26 <= 2147483646
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_82(i26, i25, iconst_2147483647, env, static) -{1,1}> overflow_Inc_85(i26, i25, env, static) :|: i25 <= 2147483647 && i25 <= iconst_2147483647 && i26 <= 2147483646
overflow_Inc_85(i26, i25, env, static) -{1,1}> overflow_JMP_93(i26, i28, env, static) :|: i25 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648 && i25 + 1 = i28
overflow_JMP_93(i26, i28, env, static) -{1,1}> overflow_Load_95(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_Load_95(i26, i28, env, static) -{1,1}> overflow_ConstantStackPush_108(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_ConstantStackPush_108(i26, i28, env, static) -{0,0}> overflow_ConstantStackPush_69(i26, i28, env, static) :|: i26 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648

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

obtained
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
overflow_Load_1(i2, env, static) -{0,0}> overflow_Load_4(i2, env, static) :|: 0 >= 0
overflow_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> overflow_Load_41(i2, env, static) :|: 0 >= 0
overflow_Load_41(i2, env, static) -{0,0}> overflow_Load_42(i2, env, static) :|: 0 >= 0
overflow_Load_42(i2, env, static) -{0,0}> overflow_Load_44(i2, env, static) :|: 0 <= static
overflow_Load_44(i2, env, static) -{0,0}> overflow_Load_46(i2, env, static) :|: 0 >= 0
overflow_Load_46(i2, env, static) -{0,0}> overflow_Load_48(i2, env, static) :|: 0 >= 0
overflow_Load_48(i2, env, static) -{1,1}> overflow_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
overflow_ConstantStackPush_50(i2, env, static) -{1,1}> overflow_GT_54(i2, iconst_2147483647, env, static) :|: 0 >= 0

obtained
overflow_GT_54(i9, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647
by chaining
overflow_GT_54(i9, iconst_2147483647, env, static) -{0,0}> overflow_GT_55(i9, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && i9 <= 2147483647
overflow_GT_55(i9, iconst_2147483647, env, static) -{1,1}> overflow_Inc_58(i9, env, static) :|: i9 <= iconst_2147483647 && i9 <= 2147483647
overflow_Inc_58(i9, env, static) -{1,1}> overflow_JMP_62(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647 && i9 + 1 = i12
overflow_JMP_62(i9, i12, env, static) -{1,1}> overflow_Load_68(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_68(i9, i12, env, static) -{1,1}> overflow_ConstantStackPush_69(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647

obtained
overflow_GT_79(i26, i25, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28'
by chaining
overflow_GT_79(i26, i25, iconst_2147483647, env, static) -{0,0}> overflow_GT_82(i26, i25, iconst_2147483647, env, static) :|: i25 <= 2147483647 && i25 <= 2147483648 && i26 <= 2147483647 && iconst_2147483647 = 2147483647 && i26 <= 2147483646
overflow_GT_82(i26, i25, iconst_2147483647, env, static) -{1,1}> overflow_Inc_85(i26, i25, env, static) :|: i25 <= 2147483647 && i25 <= iconst_2147483647 && i26 <= 2147483646
overflow_Inc_85(i26, i25, env, static) -{1,1}> overflow_JMP_93(i26, i28, env, static) :|: i25 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648 && i25 + 1 = i28
overflow_JMP_93(i26, i28, env, static) -{1,1}> overflow_Load_95(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_Load_95(i26, i28, env, static) -{1,1}> overflow_ConstantStackPush_108(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_ConstantStackPush_108(i26, i28, env, static) -{0,0}> overflow_ConstantStackPush_69(i26, i28, env, static) :|: i26 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648

(8) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_GT_54(i9, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_79(i26, i25, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28'

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

Moved arithmethic from lhss to constraints.

overflow_GT_79(i26, i25, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28'
was transformed to
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647

overflow_GT_54(i9, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647
was transformed to
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647

(10) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647

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

Moved arithmethic from constraints to rhss.

overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
was transformed to
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i25 + 1, env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647

overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647
was transformed to
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i9 + 1, env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647

overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
was transformed to
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648

overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
was transformed to
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, 2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10

(12) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i25 + 1, env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i9 + 1, env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, 2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
was transformed to
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648

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

(14) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i25 + 1, env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i9 + 1, env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, 2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648

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

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

(16) Obligation:

IntTrs with 39 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_Load_1(i2, env, static) -{0,0}> overflow_Load_4(i2, env, static) :|: 0 >= 0
overflow_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> overflow_Load_41(i2, env, static) :|: 0 >= 0
overflow_Load_41(i2, env, static) -{0,0}> overflow_Load_42(i2, env, static) :|: 0 >= 0
overflow_Load_42(i2, env, static) -{0,0}> overflow_Load_44(i2, env, static) :|: 0 <= static
overflow_Load_44(i2, env, static) -{0,0}> overflow_Load_46(i2, env, static) :|: 0 >= 0
overflow_Load_46(i2, env, static) -{0,0}> overflow_Load_48(i2, env, static) :|: 0 >= 0
overflow_Load_48(i2, env, static) -{1,1}> overflow_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
overflow_ConstantStackPush_50(i2, env, static) -{1,1}> overflow_GT_54(i2, iconst_2147483647, env, static) :|: 0 >= 0
overflow_GT_54(i9, iconst_2147483647, env, static) -{0,0}> overflow_GT_55(i9, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && i9 <= 2147483647
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_GT_55(i9, iconst_2147483647, env, static) -{1,1}> overflow_Inc_58(i9, env, static) :|: i9 <= iconst_2147483647 && i9 <= 2147483647
overflow_Inc_58(i9, env, static) -{1,1}> overflow_JMP_62(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647 && i9 + 1 = i12
overflow_JMP_62(i9, i12, env, static) -{1,1}> overflow_Load_68(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_68(i9, i12, env, static) -{1,1}> overflow_ConstantStackPush_69(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i26, i25, iconst_2147483647, env, static) -{0,0}> overflow_GT_82(i26, i25, iconst_2147483647, env, static) :|: i25 <= 2147483647 && i25 <= 2147483648 && i26 <= 2147483647 && iconst_2147483647 = 2147483647 && i26 <= 2147483646
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_82(i26, i25, iconst_2147483647, env, static) -{1,1}> overflow_Inc_85(i26, i25, env, static) :|: i25 <= 2147483647 && i25 <= iconst_2147483647 && i26 <= 2147483646
overflow_Inc_85(i26, i25, env, static) -{1,1}> overflow_JMP_93(i26, i28, env, static) :|: i25 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648 && i25 + 1 = i28
overflow_JMP_93(i26, i28, env, static) -{1,1}> overflow_Load_95(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_Load_95(i26, i28, env, static) -{1,1}> overflow_ConstantStackPush_108(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_ConstantStackPush_108(i26, i28, env, static) -{0,0}> overflow_ConstantStackPush_69(i26, i28, env, static) :|: i26 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648

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

obtained
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
overflow_Load_1(i2, env, static) -{0,0}> overflow_Load_4(i2, env, static) :|: 0 >= 0
overflow_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> overflow_Load_41(i2, env, static) :|: 0 >= 0
overflow_Load_41(i2, env, static) -{0,0}> overflow_Load_42(i2, env, static) :|: 0 >= 0
overflow_Load_42(i2, env, static) -{0,0}> overflow_Load_44(i2, env, static) :|: 0 <= static
overflow_Load_44(i2, env, static) -{0,0}> overflow_Load_46(i2, env, static) :|: 0 >= 0
overflow_Load_46(i2, env, static) -{0,0}> overflow_Load_48(i2, env, static) :|: 0 >= 0
overflow_Load_48(i2, env, static) -{1,1}> overflow_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
overflow_ConstantStackPush_50(i2, env, static) -{1,1}> overflow_GT_54(i2, iconst_2147483647, env, static) :|: 0 >= 0

obtained
overflow_GT_54(i9, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647
by chaining
overflow_GT_54(i9, iconst_2147483647, env, static) -{0,0}> overflow_GT_55(i9, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && i9 <= 2147483647
overflow_GT_55(i9, iconst_2147483647, env, static) -{1,1}> overflow_Inc_58(i9, env, static) :|: i9 <= iconst_2147483647 && i9 <= 2147483647
overflow_Inc_58(i9, env, static) -{1,1}> overflow_JMP_62(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647 && i9 + 1 = i12
overflow_JMP_62(i9, i12, env, static) -{1,1}> overflow_Load_68(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_68(i9, i12, env, static) -{1,1}> overflow_ConstantStackPush_69(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647

obtained
overflow_GT_79(i26, i25, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28'
by chaining
overflow_GT_79(i26, i25, iconst_2147483647, env, static) -{0,0}> overflow_GT_82(i26, i25, iconst_2147483647, env, static) :|: i25 <= 2147483647 && i25 <= 2147483648 && i26 <= 2147483647 && iconst_2147483647 = 2147483647 && i26 <= 2147483646
overflow_GT_82(i26, i25, iconst_2147483647, env, static) -{1,1}> overflow_Inc_85(i26, i25, env, static) :|: i25 <= 2147483647 && i25 <= iconst_2147483647 && i26 <= 2147483646
overflow_Inc_85(i26, i25, env, static) -{1,1}> overflow_JMP_93(i26, i28, env, static) :|: i25 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648 && i25 + 1 = i28
overflow_JMP_93(i26, i28, env, static) -{1,1}> overflow_Load_95(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_Load_95(i26, i28, env, static) -{1,1}> overflow_ConstantStackPush_108(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_ConstantStackPush_108(i26, i28, env, static) -{0,0}> overflow_ConstantStackPush_69(i26, i28, env, static) :|: i26 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648

(18) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_GT_54(i9, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_79(i26, i25, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28'

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

Moved arithmethic from lhss to constraints.

overflow_GT_79(i26, i25, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28'
was transformed to
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647

overflow_GT_54(i9, 2147483647, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647
was transformed to
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647

(20) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647

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

Moved arithmethic from constraints to rhss.

overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i28', env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
was transformed to
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i25 + 1, env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647

overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i12', env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647
was transformed to
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i9 + 1, env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647

overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, iconst_2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
was transformed to
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648

overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
was transformed to
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, 2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10

(22) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i25 + 1, env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i9 + 1, env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, 2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648 && iconst_2147483648 <= 2147483648
was transformed to
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648

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

(24) Obligation:

IntTrs with 6 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
overflow_GT_79(i26, i25, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i26, i25 + 1, env, static) :|: i25 <= 2147483647 && i28' <= 2147483648 && i26 <= 2147483647 && i26 <= 2147483646 && i25 <= 2147483648 && i25 + 1 = i28' && x = 2147483647
overflow_GT_54(i9, x, env, static) -{4,4}> overflow_ConstantStackPush_69(i9, i9 + 1, env, static) :|: i9 + 1 = i12' && i12' <= 2147483648 && i9 <= 2147483647 && x = 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_1(i2, env, static) -{17,17}> overflow_GT_54(i2, iconst_2147483647', env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
overflow_GT_54(i10, iconst_2147483647, env, static) -{0,0}> overflow_GT_56(i10, 2147483647, env, static) :|: iconst_2147483647 = 2147483647 && 2147483648 <= i10
overflow_GT_79(i9, iconst_2147483648, iconst_2147483647, env, static) -{0,0}> overflow_GT_83(i9, 2147483648, iconst_2147483647, env, static) :|: i9 <= 2147483647 && iconst_2147483648 = 2147483648

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

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

(26) Obligation:

Set of 37 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(28) Obligation:

IntTrs with 37 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
overflow_Load_1(i2, env, static) -{0,0}> overflow_Load_4(i2, env, static) :|: 0 >= 0
overflow_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> overflow_Load_41(i2, env, static) :|: 0 >= 0
overflow_Load_41(i2, env, static) -{0,0}> overflow_Load_42(i2, env, static) :|: 0 >= 0
overflow_Load_42(i2, env, static) -{0,0}> overflow_Load_44(i2, env, static) :|: 0 <= static
overflow_Load_44(i2, env, static) -{0,0}> overflow_Load_46(i2, env, static) :|: 0 >= 0
overflow_Load_46(i2, env, static) -{0,0}> overflow_Load_48(i2, env, static) :|: 0 >= 0
overflow_Load_48(i2, env, static) -{1,1}> overflow_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
overflow_ConstantStackPush_50(i2, env, static) -{1,1}> overflow_GT_54(i2, iconst_2147483647, env, static) :|: 0 >= 0
overflow_GT_54(i9, iconst_2147483647, env, static) -{0,0}> overflow_GT_55(i9, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && i9 <= 2147483647
overflow_GT_55(i9, iconst_2147483647, env, static) -{1,1}> overflow_Inc_58(i9, env, static) :|: i9 <= iconst_2147483647 && i9 <= 2147483647
overflow_Inc_58(i9, env, static) -{1,1}> overflow_JMP_62(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647 && i9 + 1 = i12
overflow_JMP_62(i9, i12, env, static) -{1,1}> overflow_Load_68(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_68(i9, i12, env, static) -{1,1}> overflow_ConstantStackPush_69(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i26, i25, iconst_2147483647, env, static) -{0,0}> overflow_GT_82(i26, i25, iconst_2147483647, env, static) :|: i25 <= 2147483647 && i25 <= 2147483648 && i26 <= 2147483647 && iconst_2147483647 = 2147483647 && i26 <= 2147483646
overflow_GT_82(i26, i25, iconst_2147483647, env, static) -{1,1}> overflow_Inc_85(i26, i25, env, static) :|: i25 <= 2147483647 && i25 <= iconst_2147483647 && i26 <= 2147483646
overflow_Inc_85(i26, i25, env, static) -{1,1}> overflow_JMP_93(i26, i28, env, static) :|: i25 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648 && i25 + 1 = i28
overflow_JMP_93(i26, i28, env, static) -{1,1}> overflow_Load_95(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_Load_95(i26, i28, env, static) -{1,1}> overflow_ConstantStackPush_108(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_ConstantStackPush_108(i26, i28, env, static) -{0,0}> overflow_ConstantStackPush_69(i26, i28, env, static) :|: i26 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648

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

obtained
overflow_Load_1(i2, env, static) -{21,21}> overflow_ConstantStackPush_69(i2, i12', env, static'1) :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
overflow_Load_1(i2, env, static) -{0,0}> overflow_Load_4(i2, env, static) :|: 0 >= 0
overflow_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> overflow_Load_41(i2, env, static) :|: 0 >= 0
overflow_Load_41(i2, env, static) -{0,0}> overflow_Load_42(i2, env, static) :|: 0 >= 0
overflow_Load_42(i2, env, static) -{0,0}> overflow_Load_44(i2, env, static) :|: 0 <= static
overflow_Load_44(i2, env, static) -{0,0}> overflow_Load_46(i2, env, static) :|: 0 >= 0
overflow_Load_46(i2, env, static) -{0,0}> overflow_Load_48(i2, env, static) :|: 0 >= 0
overflow_Load_48(i2, env, static) -{1,1}> overflow_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
overflow_ConstantStackPush_50(i2, env, static) -{1,1}> overflow_GT_54(i2, iconst_2147483647, env, static) :|: 0 >= 0
overflow_GT_54(i9, iconst_2147483647, env, static) -{0,0}> overflow_GT_55(i9, iconst_2147483647, env, static) :|: iconst_2147483647 = 2147483647 && i9 <= 2147483647
overflow_GT_55(i9, iconst_2147483647, env, static) -{1,1}> overflow_Inc_58(i9, env, static) :|: i9 <= iconst_2147483647 && i9 <= 2147483647
overflow_Inc_58(i9, env, static) -{1,1}> overflow_JMP_62(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647 && i9 + 1 = i12
overflow_JMP_62(i9, i12, env, static) -{1,1}> overflow_Load_68(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_Load_68(i9, i12, env, static) -{1,1}> overflow_ConstantStackPush_69(i9, i12, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647

obtained
overflow_ConstantStackPush_69(i9, i12, env, static) -{5,5}> overflow_ConstantStackPush_69(i9, i28', env, static) :|: i12 <= 2147483647 && i28' <= 2147483648 && i12 <= 2147483648 && i9 <= 2147483647 && i9 <= 2147483646 && i12 + 1 = i28'
by chaining
overflow_ConstantStackPush_69(i9, i12, env, static) -{1,1}> overflow_GT_79(i9, i12, iconst_2147483647, env, static) :|: i12 <= 2147483648 && i9 <= 2147483647
overflow_GT_79(i26, i25, iconst_2147483647, env, static) -{0,0}> overflow_GT_82(i26, i25, iconst_2147483647, env, static) :|: i25 <= 2147483647 && i25 <= 2147483648 && i26 <= 2147483647 && iconst_2147483647 = 2147483647 && i26 <= 2147483646
overflow_GT_82(i26, i25, iconst_2147483647, env, static) -{1,1}> overflow_Inc_85(i26, i25, env, static) :|: i25 <= 2147483647 && i25 <= iconst_2147483647 && i26 <= 2147483646
overflow_Inc_85(i26, i25, env, static) -{1,1}> overflow_JMP_93(i26, i28, env, static) :|: i25 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648 && i25 + 1 = i28
overflow_JMP_93(i26, i28, env, static) -{1,1}> overflow_Load_95(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_Load_95(i26, i28, env, static) -{1,1}> overflow_ConstantStackPush_108(i26, i28, env, static) :|: i26 <= 2147483646 && i28 <= 2147483648
overflow_ConstantStackPush_108(i26, i28, env, static) -{0,0}> overflow_ConstantStackPush_69(i26, i28, env, static) :|: i26 <= 2147483647 && i26 <= 2147483646 && i28 <= 2147483648

(30) Obligation:

IntTrs with 2 rules
Start term: overflow_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
overflow_Load_1(i2, env, static) -{21,21}> overflow_ConstantStackPush_69(i2, i12', env, static'1) :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
overflow_ConstantStackPush_69(i9, i12, env, static) -{5,5}> overflow_ConstantStackPush_69(i9, i28', env, static) :|: i12 <= 2147483647 && i28' <= 2147483648 && i12 <= 2147483648 && i9 <= 2147483647 && i9 <= 2147483646 && i12 + 1 = i28'

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

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

overflow_Load_1(x1, x2, x3) → overflow_Load_1(x1, x3)
overflow_ConstantStackPush_69(x1, x2, x3, x4) → overflow_ConstantStackPush_69(x1, x2)

(32) Obligation:

IntTrs with 2 rules
Start term: overflow_Load_1(#0, static)
Considered paths: all paths from start
Rules:
overflow_Load_1(i2, static) -{21,21}> overflow_ConstantStackPush_69(i2, i12') :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
overflow_ConstantStackPush_69(i9, i12) -{5,5}> overflow_ConstantStackPush_69(i9, i28') :|: i12 <= 2147483647 && i28' <= 2147483648 && i12 <= 2147483648 && i9 <= 2147483647 && i9 <= 2147483646 && i12 + 1 = i28'

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

Moved arithmethic from constraints to rhss.

overflow_ConstantStackPush_69(i9, i12) -{5,5}> overflow_ConstantStackPush_69(i9, i28') :|: i12 <= 2147483647 && i28' <= 2147483648 && i12 <= 2147483648 && i9 <= 2147483647 && i9 <= 2147483646 && i12 + 1 = i28'
was transformed to
overflow_ConstantStackPush_69(i9, i12) -{5,5}> overflow_ConstantStackPush_69(i9, i12 + 1) :|: i12 <= 2147483647 && i28' <= 2147483648 && i12 <= 2147483648 && i9 <= 2147483647 && i9 <= 2147483646 && i12 + 1 = i28'

overflow_Load_1(i2, static) -{21,21}> overflow_ConstantStackPush_69(i2, i12') :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
overflow_Load_1(i2, static) -{21,21}> overflow_ConstantStackPush_69(i2, i2 + 1) :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2

(34) Obligation:

IntTrs with 2 rules
Start term: overflow_Load_1(#0, static)
Considered paths: all paths from start
Rules:
overflow_ConstantStackPush_69(i9, i12) -{5,5}> overflow_ConstantStackPush_69(i9, i12 + 1) :|: i12 <= 2147483647 && i28' <= 2147483648 && i12 <= 2147483648 && i9 <= 2147483647 && i9 <= 2147483646 && i12 + 1 = i28'
overflow_Load_1(i2, static) -{21,21}> overflow_ConstantStackPush_69(i2, i2 + 1) :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2

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

Simplified expressions.

overflow_Load_1(i2, static) -{21,21}> overflow_ConstantStackPush_69(i2, i2 + 1) :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
overflow_Load_1(i2, static) -{21,21}> overflow_ConstantStackPush_69(i2, i2 + 1) :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(36) Obligation:

IntTrs with 2 rules
Start term: overflow_Load_1(#0, static)
Considered paths: all paths from start
Rules:
overflow_ConstantStackPush_69(i9, i12) -{5,5}> overflow_ConstantStackPush_69(i9, i12 + 1) :|: i12 <= 2147483647 && i28' <= 2147483648 && i12 <= 2147483648 && i9 <= 2147483647 && i9 <= 2147483646 && i12 + 1 = i28'
overflow_Load_1(i2, static) -{21,21}> overflow_ConstantStackPush_69(i2, i2 + 1) :|: i2 + 1 = i12' && i12' <= 2147483648 && i2 <= 2147483647 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(37) koat Proof (EQUIVALENT transformation)

YES(?, 5*ar_0 + 10737418256)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 5) overflow_ConstantStackPush_69(ar_0, ar_1) -> Com_1(overflow_ConstantStackPush_69(ar_0, ar_1 + 1)) [ ar_1 <= 2147483647 /\ i28' <= 2147483648 /\ ar_1 <= 2147483648 /\ ar_0 <= 2147483647 /\ ar_0 <= 2147483646 /\ ar_1 + 1 = i28' ]
(Comp: ?, Cost: 21) overflow_Load_1(ar_0, ar_1) -> Com_1(overflow_ConstantStackPush_69(ar_0, ar_0 + 1)) [ ar_0 + 1 = i12' /\ i12' <= 2147483648 /\ ar_0 <= 2147483647 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(overflow_Load_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 5) overflow_ConstantStackPush_69(ar_0, ar_1) -> Com_1(overflow_ConstantStackPush_69(ar_0, ar_1 + 1)) [ ar_1 <= 2147483647 /\ i28' <= 2147483648 /\ ar_1 <= 2147483648 /\ ar_0 <= 2147483647 /\ ar_0 <= 2147483646 /\ ar_1 + 1 = i28' ]
(Comp: 1, Cost: 21) overflow_Load_1(ar_0, ar_1) -> Com_1(overflow_ConstantStackPush_69(ar_0, ar_0 + 1)) [ ar_0 + 1 = i12' /\ i12' <= 2147483648 /\ ar_0 <= 2147483647 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(overflow_Load_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(overflow_ConstantStackPush_69) = -V_2 + 2147483648
Pol(overflow_Load_1) = -V_1 + 2147483647
Pol(koat_start) = -V_1 + 2147483647
orients all transitions weakly and the transition
overflow_ConstantStackPush_69(ar_0, ar_1) -> Com_1(overflow_ConstantStackPush_69(ar_0, ar_1 + 1)) [ ar_1 <= 2147483647 /\ i28' <= 2147483648 /\ ar_1 <= 2147483648 /\ ar_0 <= 2147483647 /\ ar_0 <= 2147483646 /\ ar_1 + 1 = i28' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0 + 2147483647, Cost: 5) overflow_ConstantStackPush_69(ar_0, ar_1) -> Com_1(overflow_ConstantStackPush_69(ar_0, ar_1 + 1)) [ ar_1 <= 2147483647 /\ i28' <= 2147483648 /\ ar_1 <= 2147483648 /\ ar_0 <= 2147483647 /\ ar_0 <= 2147483646 /\ ar_1 + 1 = i28' ]
(Comp: 1, Cost: 21) overflow_Load_1(ar_0, ar_1) -> Com_1(overflow_ConstantStackPush_69(ar_0, ar_0 + 1)) [ ar_0 + 1 = i12' /\ i12' <= 2147483648 /\ ar_0 <= 2147483647 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(overflow_Load_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 5*ar_0 + 10737418256

Time: 0.078 sec (SMT: 0.074 sec)

(38) BOUNDS(CONSTANT, 10737418256 + 5 * |#0|)