time complexity proof of /tmp/tmpgsc5YJ/LogBuiltIn.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 32 + 9 * |#0|).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 36 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), 0 ms)

        ↳16 WeightedIntTrs

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

    ↳18 WeightedIntTrs

        ↳19 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 19 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 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

        ↳29 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 14 ms)

        ↳30 WeightedIntTrs

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

↳32 JBCComplexityEdges

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

    ↳43 koat Proof (⇔, 62 ms)

    ↳44 BOUNDS(CONSTANT, 26 + 9 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class LogBuiltIn{
  public static int log(int x) {

    int res = 0;

    while (x > 1) {

      x = x/2;
      res++;

    }

    return res;

  }


}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
LogBuiltIn.log(I)I: Graph of 57 nodes with 1 SCC.

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

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

(4) Obligation:

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

(6) Obligation:

IntTrs with 51 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_3(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_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: NULL = 0 && 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_Load_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> log_ConstantStackPush_43(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_43(i2, env, static) -{0,0}> log_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_45(i2, env, static) -{0,0}> log_ConstantStackPush_48(i2, env, static) :|: 0 <= static
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_50(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_58(i10, iconst_1, iconst_0, env, static) -{0,0}> log_LE_60(i10, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_LE_60(i10, iconst_1, iconst_0, env, static) -{1,1}> log_Load_64(i10, iconst_0, env, static) :|: iconst_1 < i10 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_Load_64(i10, iconst_0, env, static) -{1,1}> log_ConstantStackPush_69(i10, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10
log_ConstantStackPush_69(i10, iconst_0, env, static) -{1,1}> log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2
log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) -{1,1}> log_Store_81(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2 && 1 <= i12 && i12 < i10
log_Store_81(i10, i12, iconst_0, env, static) -{1,1}> log_Inc_82(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_Inc_82(i10, i12, iconst_0, env, static) -{1,1}> log_JMP_83(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_JMP_83(i10, i12, iconst_1, env, static) -{1,1}> log_Load_84(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_84(i10, i12, iconst_1, env, static) -{0,0}> log_Load_130(i10, i12, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_130(i10, i31, i32, env, static) -{0,0}> log_Load_184(i10, i31, i32, env, static) :|: i32 <= 2 && i32 <= 3 && 2 <= i10 && 1 <= i32 && 1 <= i31
log_Load_184(i10, i59, i60, env, static) -{0,0}> log_Load_230(i10, i59, i60, env, static) :|: i60 <= 3 && 2 <= i10 && 1 <= i60 && 1 <= i59
log_Load_230(i10, i89, i90, env, static) -{1,1}> log_ConstantStackPush_234(i10, i89, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 1 <= i89
log_ConstantStackPush_234(i10, i89, i90, env, static) -{1,1}> log_LE_245(i10, i89, iconst_1, i90, env, static) :|: 1 <= i90 && iconst_1 = 1 && 2 <= i10 && 1 <= i89
log_LE_245(i10, iconst_1, iconst_1, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10
log_LE_245(i10, i102, iconst_1, i90, env, static) -{0,0}> log_LE_251(i10, i102, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_LE_251(i10, i102, iconst_1, i90, env, static) -{1,1}> log_Load_262(i10, i102, i90, env, static) :|: 1 <= i90 && iconst_1 < i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_Load_262(i10, i102, i90, env, static) -{1,1}> log_ConstantStackPush_264(i10, i102, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102
log_ConstantStackPush_264(i10, i102, i90, env, static) -{1,1}> log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) -{1,1}> log_Store_269(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && i106 < i102 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_Store_269(i10, i106, i90, env, static) -{1,1}> log_Inc_273(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && 2 <= i10
log_Inc_273(i10, i106, i90, env, static) -{1,1}> log_JMP_276(i10, i106, i109, env, static) :|: i90 + 1 = i109 && 1 <= i106 && 1 <= i90 && 2 <= i109 && 2 <= i10
log_JMP_276(i10, i106, i109, env, static) -{1,1}> log_Load_281(i10, i106, i109, env, static) :|: 1 <= i106 && 2 <= i109 && 2 <= i10
log_Load_281(i10, i106, i109, env, static) -{0,0}> log_Load_230(i10, i106, i109, env, static) :|: 1 <= i106 && 1 <= i109 && 2 <= i109 && 2 <= i10

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

obtained
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_3(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_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: NULL = 0 && 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_Load_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> log_ConstantStackPush_43(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_43(i2, env, static) -{0,0}> log_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_45(i2, env, static) -{0,0}> log_ConstantStackPush_48(i2, env, static) :|: 0 <= static
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_50(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0

obtained
log_LE_58(i10, 1, 0, env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2
by chaining
log_LE_58(i10, iconst_1, iconst_0, env, static) -{0,0}> log_LE_60(i10, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_LE_60(i10, iconst_1, iconst_0, env, static) -{1,1}> log_Load_64(i10, iconst_0, env, static) :|: iconst_1 < i10 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_Load_64(i10, iconst_0, env, static) -{1,1}> log_ConstantStackPush_69(i10, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10
log_ConstantStackPush_69(i10, iconst_0, env, static) -{1,1}> log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2
log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) -{1,1}> log_Store_81(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2 && 1 <= i12 && i12 < i10
log_Store_81(i10, i12, iconst_0, env, static) -{1,1}> log_Inc_82(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_Inc_82(i10, i12, iconst_0, env, static) -{1,1}> log_JMP_83(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_JMP_83(i10, i12, iconst_1, env, static) -{1,1}> log_Load_84(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_84(i10, i12, iconst_1, env, static) -{0,0}> log_Load_130(i10, i12, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_130(i10, i31, i32, env, static) -{0,0}> log_Load_184(i10, i31, i32, env, static) :|: i32 <= 2 && i32 <= 3 && 2 <= i10 && 1 <= i32 && 1 <= i31
log_Load_184(i10, i59, i60, env, static) -{0,0}> log_Load_230(i10, i59, i60, env, static) :|: i60 <= 3 && 2 <= i10 && 1 <= i60 && 1 <= i59

obtained
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
by chaining
log_Load_230(i10, i89, i90, env, static) -{1,1}> log_ConstantStackPush_234(i10, i89, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 1 <= i89
log_ConstantStackPush_234(i10, i89, i90, env, static) -{1,1}> log_LE_245(i10, i89, iconst_1, i90, env, static) :|: 1 <= i90 && iconst_1 = 1 && 2 <= i10 && 1 <= i89

obtained
log_LE_245(i10, i102, 1, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102
by chaining
log_LE_245(i10, i102, iconst_1, i90, env, static) -{0,0}> log_LE_251(i10, i102, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_LE_251(i10, i102, iconst_1, i90, env, static) -{1,1}> log_Load_262(i10, i102, i90, env, static) :|: 1 <= i90 && iconst_1 < i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_Load_262(i10, i102, i90, env, static) -{1,1}> log_ConstantStackPush_264(i10, i102, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102
log_ConstantStackPush_264(i10, i102, i90, env, static) -{1,1}> log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) -{1,1}> log_Store_269(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && i106 < i102 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_Store_269(i10, i106, i90, env, static) -{1,1}> log_Inc_273(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && 2 <= i10
log_Inc_273(i10, i106, i90, env, static) -{1,1}> log_JMP_276(i10, i106, i109, env, static) :|: i90 + 1 = i109 && 1 <= i106 && 1 <= i90 && 2 <= i109 && 2 <= i10
log_JMP_276(i10, i106, i109, env, static) -{1,1}> log_Load_281(i10, i106, i109, env, static) :|: 1 <= i106 && 2 <= i109 && 2 <= i10
log_Load_281(i10, i106, i109, env, static) -{0,0}> log_Load_230(i10, i106, i109, env, static) :|: 1 <= i106 && 1 <= i109 && 2 <= i109 && 2 <= i10

(8) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_58(i10, 1, 0, env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
log_LE_245(i10, iconst_1, iconst_1, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10
log_LE_245(i10, i102, 1, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102

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

Moved arithmethic from lhss to constraints.

log_LE_58(i10, 1, 0, env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2
was transformed to
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2 && x = 1 && x' = 0

log_LE_245(i10, i102, 1, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102
was transformed to
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102 && x = 1

(10) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2 && x = 1 && x' = 0
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102 && x = 1
log_LE_245(i10, iconst_1, iconst_1, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0

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

Linearized lhss.

log_LE_245(i10, iconst_1, iconst_1, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10
was transformed to
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1

(12) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2 && x = 1 && x' = 0
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102 && x = 1
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10

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

Moved arithmethic from constraints to rhss.

log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
was transformed to
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, 1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1

log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
was transformed to
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, 1, 0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0

(14) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, 1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2 && x = 1 && x' = 0
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102 && x = 1
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, 1, 0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0

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

Simplified expressions.

log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i12' < i10 && 1 <= 2 && x = 1 && x' = 0
was transformed to
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 2 <= i10 && i12' < i10 && x = 1 && x' = 0

log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102 && x = 1
was transformed to
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102 && x = 1

(16) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 2 <= i10 && i12' < i10 && x = 1 && x' = 0
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, 1, 0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, 1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i102 && x = 1
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10

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

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

(18) Obligation:

IntTrs with 51 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_3(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_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: NULL = 0 && 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_Load_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> log_ConstantStackPush_43(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_43(i2, env, static) -{0,0}> log_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_45(i2, env, static) -{0,0}> log_ConstantStackPush_48(i2, env, static) :|: 0 <= static
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_50(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_58(i10, iconst_1, iconst_0, env, static) -{0,0}> log_LE_60(i10, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_LE_60(i10, iconst_1, iconst_0, env, static) -{1,1}> log_Load_64(i10, iconst_0, env, static) :|: iconst_1 < i10 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_Load_64(i10, iconst_0, env, static) -{1,1}> log_ConstantStackPush_69(i10, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10
log_ConstantStackPush_69(i10, iconst_0, env, static) -{1,1}> log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2
log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) -{1,1}> log_Store_81(i10, i12, iconst_0, env, static) :|: i10 / iconst_2 = i12 && iconst_0 = 0 && 2 <= i10 && iconst_2 = 2 && 1 <= i12
log_Store_81(i10, i12, iconst_0, env, static) -{1,1}> log_Inc_82(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_Inc_82(i10, i12, iconst_0, env, static) -{1,1}> log_JMP_83(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_JMP_83(i10, i12, iconst_1, env, static) -{1,1}> log_Load_84(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_84(i10, i12, iconst_1, env, static) -{0,0}> log_Load_130(i10, i12, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_130(i10, i31, i32, env, static) -{0,0}> log_Load_184(i10, i31, i32, env, static) :|: i32 <= 2 && i32 <= 3 && 2 <= i10 && 1 <= i32 && 1 <= i31
log_Load_184(i10, i59, i60, env, static) -{0,0}> log_Load_230(i10, i59, i60, env, static) :|: i60 <= 3 && 2 <= i10 && 1 <= i60 && 1 <= i59
log_Load_230(i10, i89, i90, env, static) -{1,1}> log_ConstantStackPush_234(i10, i89, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 1 <= i89
log_ConstantStackPush_234(i10, i89, i90, env, static) -{1,1}> log_LE_245(i10, i89, iconst_1, i90, env, static) :|: 1 <= i90 && iconst_1 = 1 && 2 <= i10 && 1 <= i89
log_LE_245(i10, iconst_1, iconst_1, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10
log_LE_245(i10, i102, iconst_1, i90, env, static) -{0,0}> log_LE_251(i10, i102, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_LE_251(i10, i102, iconst_1, i90, env, static) -{1,1}> log_Load_262(i10, i102, i90, env, static) :|: 1 <= i90 && iconst_1 < i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_Load_262(i10, i102, i90, env, static) -{1,1}> log_ConstantStackPush_264(i10, i102, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102
log_ConstantStackPush_264(i10, i102, i90, env, static) -{1,1}> log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) -{1,1}> log_Store_269(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && i102 / iconst_2 = i106 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_Store_269(i10, i106, i90, env, static) -{1,1}> log_Inc_273(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && 2 <= i10
log_Inc_273(i10, i106, i90, env, static) -{1,1}> log_JMP_276(i10, i106, i109, env, static) :|: i90 + 1 = i109 && 1 <= i106 && 1 <= i90 && 2 <= i109 && 2 <= i10
log_JMP_276(i10, i106, i109, env, static) -{1,1}> log_Load_281(i10, i106, i109, env, static) :|: 1 <= i106 && 2 <= i109 && 2 <= i10
log_Load_281(i10, i106, i109, env, static) -{0,0}> log_Load_230(i10, i106, i109, env, static) :|: 1 <= i106 && 1 <= i109 && 2 <= i109 && 2 <= i10

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

obtained
log_LE_58(i10, 1, 0, env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i10 / 2 = i12' && 1 <= 2
by chaining
log_LE_58(i10, iconst_1, iconst_0, env, static) -{0,0}> log_LE_60(i10, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_LE_60(i10, iconst_1, iconst_0, env, static) -{1,1}> log_Load_64(i10, iconst_0, env, static) :|: iconst_1 < i10 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_Load_64(i10, iconst_0, env, static) -{1,1}> log_ConstantStackPush_69(i10, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10
log_ConstantStackPush_69(i10, iconst_0, env, static) -{1,1}> log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2
log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) -{1,1}> log_Store_81(i10, i12, iconst_0, env, static) :|: i10 / iconst_2 = i12 && iconst_0 = 0 && 2 <= i10 && iconst_2 = 2 && 1 <= i12
log_Store_81(i10, i12, iconst_0, env, static) -{1,1}> log_Inc_82(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_Inc_82(i10, i12, iconst_0, env, static) -{1,1}> log_JMP_83(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_JMP_83(i10, i12, iconst_1, env, static) -{1,1}> log_Load_84(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_84(i10, i12, iconst_1, env, static) -{0,0}> log_Load_130(i10, i12, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_130(i10, i31, i32, env, static) -{0,0}> log_Load_184(i10, i31, i32, env, static) :|: i32 <= 2 && i32 <= 3 && 2 <= i10 && 1 <= i32 && 1 <= i31
log_Load_184(i10, i59, i60, env, static) -{0,0}> log_Load_230(i10, i59, i60, env, static) :|: i60 <= 3 && 2 <= i10 && 1 <= i60 && 1 <= i59

obtained
log_LE_245(i10, i102, 1, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i102 / 2 = i106'
by chaining
log_LE_245(i10, i102, iconst_1, i90, env, static) -{0,0}> log_LE_251(i10, i102, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_LE_251(i10, i102, iconst_1, i90, env, static) -{1,1}> log_Load_262(i10, i102, i90, env, static) :|: 1 <= i90 && iconst_1 < i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_Load_262(i10, i102, i90, env, static) -{1,1}> log_ConstantStackPush_264(i10, i102, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102
log_ConstantStackPush_264(i10, i102, i90, env, static) -{1,1}> log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) -{1,1}> log_Store_269(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && i102 / iconst_2 = i106 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_Store_269(i10, i106, i90, env, static) -{1,1}> log_Inc_273(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && 2 <= i10
log_Inc_273(i10, i106, i90, env, static) -{1,1}> log_JMP_276(i10, i106, i109, env, static) :|: i90 + 1 = i109 && 1 <= i106 && 1 <= i90 && 2 <= i109 && 2 <= i10
log_JMP_276(i10, i106, i109, env, static) -{1,1}> log_Load_281(i10, i106, i109, env, static) :|: 1 <= i106 && 2 <= i109 && 2 <= i10
log_Load_281(i10, i106, i109, env, static) -{0,0}> log_Load_230(i10, i106, i109, env, static) :|: 1 <= i106 && 1 <= i109 && 2 <= i109 && 2 <= i10

(20) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_58(i10, 1, 0, env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i10 / 2 = i12' && 1 <= 2
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
log_LE_245(i10, iconst_1, iconst_1, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10
log_LE_245(i10, i102, 1, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i102 / 2 = i106'

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

Moved arithmethic from lhss to constraints.

log_LE_245(i10, i102, 1, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i102 / 2 = i106'
was transformed to
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i102 / 2 = i106' && x = 1

log_LE_58(i10, 1, 0, env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i10 / 2 = i12' && 1 <= 2
was transformed to
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i10 / 2 = i12' && 1 <= 2 && x = 1 && x' = 0

(22) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i102 / 2 = i106' && x = 1
log_LE_245(i10, iconst_1, iconst_1, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i10 / 2 = i12' && 1 <= 2 && x = 1 && x' = 0
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0

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

Linearized lhss.

(24) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i102 / 2 = i106' && x = 1
log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i10 / 2 = i12' && 1 <= 2 && x = 1 && x' = 0
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10

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

Removed div and mod.

log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i102 / 2 = i106' && x = 1
was transformed to
log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: i102 - 2 * div < 2 && i102 - 2 * div + 2 > 0 && 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, x, i90, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1

log_LE_58(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && i10 / 2 = i12' && 1 <= 2 && x = 1 && x' = 0
was transformed to
log_LE_58'(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, x, x', env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0

(26) Obligation:

IntTrs with 8 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
log_LE_58'(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: i102 - 2 * div < 2 && i102 - 2 * div + 2 > 0 && 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, x, i90, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, x, x', env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, iconst_1, iconst_0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0

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

Moved arithmethic from constraints to rhss.

log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i109', env, static) :|: i102 - 2 * div < 2 && i102 - 2 * div + 2 > 0 && 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
was transformed to
log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: i102 - 2 * div < 2 && i102 - 2 * div + 2 > 0 && 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1

log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, x, i90, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
was transformed to
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, 1, i90, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1

log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, x, x', env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
was transformed to
log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, 1, 0, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0

(28) Obligation:

IntTrs with 8 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, 1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
log_LE_58'(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, 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
log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: i102 - 2 * div < 2 && i102 - 2 * div + 2 > 0 && 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, 1, i90, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, 1, 0, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, 1, 0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10

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

Simplified expressions.

log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: i102 - 2 * div < 2 && i102 - 2 * div + 2 > 0 && 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
was transformed to
log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: i102 + -2 * div < 2 && 0 < i102 + -2 * div + 2 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1

log_LE_58'(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
was transformed to
log_LE_58'(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: i10 + -2 * div < 2 && 0 < i10 + -2 * div + 2 && 1 < i10 && 1 <= i12' && 2 <= i10 && div = i12' && x = 1 && x' = 0

log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, 1, i90, env, static) :|: 1 <= i102 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
was transformed to
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, 1, i90, env, static) :|: 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1

log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, 1, 0, env, static) :|: 1 < i10 && 1 <= i12' && 1 <= 3 && 1 <= 1 && 2 <= i10 && div = i12' && 1 <= 2 && x = 1 && x' = 0
was transformed to
log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, 1, 0, env, static) :|: 1 < i10 && 1 <= i12' && 2 <= i10 && div = i12' && x = 1 && x' = 0

(30) Obligation:

IntTrs with 8 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_245(i10, i102, x, i90, env, static) -{7,7}> log_LE_245'(i10, i102, 1, i90, env, static) :|: 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
log_LE_58(i9, iconst_1, iconst_0, env, static) -{0,0}> log_LE_59(i9, 1, 0, env, static) :|: i9 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_245(i10, iconst_1, x, i90, env, static) -{0,0}> log_LE_250(i10, 1, i90, env, static) :|: 1 <= i90 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && x = iconst_1
log_LE_245'(i10, i102, x, i90, env, static) -{7,7}> log_Load_230(i10, i106', i90 + 1, env, static) :|: i102 + -2 * div < 2 && 0 < i102 + -2 * div + 2 && 2 <= i10 && 1 < i102 && 2 <= i109' && 2 <= i102 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && div = i106' && x = 1
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_58(i2, 1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
log_LE_58'(i10, x, x', env, static) -{7,7}> log_Load_230(i10, i12', 1, env, static) :|: i10 + -2 * div < 2 && 0 < i10 + -2 * div + 2 && 1 < i10 && 1 <= i12' && 2 <= i10 && div = i12' && x = 1 && x' = 0
log_Load_230(i10, i89, i90, env, static) -{2,2}> log_LE_245(i10, i89, 1, i90, env, static) :|: 1 <= i89 && 1 <= i90 && 2 <= i10
log_LE_58(i10, x, x', env, static) -{7,7}> log_LE_58'(i10, 1, 0, env, static) :|: 1 < i10 && 1 <= i12' && 2 <= i10 && div = i12' && x = 1 && x' = 0

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

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

(32) Obligation:

Set of 49 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 49 jbc graph edges to a weighted ITS with 49 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 49 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_3(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_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: NULL = 0 && 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_Load_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> log_ConstantStackPush_43(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_43(i2, env, static) -{0,0}> log_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_45(i2, env, static) -{0,0}> log_ConstantStackPush_48(i2, env, static) :|: 0 <= static
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_50(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i10, iconst_1, iconst_0, env, static) -{0,0}> log_LE_60(i10, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_LE_60(i10, iconst_1, iconst_0, env, static) -{1,1}> log_Load_64(i10, iconst_0, env, static) :|: iconst_1 < i10 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_Load_64(i10, iconst_0, env, static) -{1,1}> log_ConstantStackPush_69(i10, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10
log_ConstantStackPush_69(i10, iconst_0, env, static) -{1,1}> log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2
log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) -{1,1}> log_Store_81(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2 && 1 <= i12 && i12 < i10
log_Store_81(i10, i12, iconst_0, env, static) -{1,1}> log_Inc_82(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_Inc_82(i10, i12, iconst_0, env, static) -{1,1}> log_JMP_83(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_JMP_83(i10, i12, iconst_1, env, static) -{1,1}> log_Load_84(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_84(i10, i12, iconst_1, env, static) -{0,0}> log_Load_130(i10, i12, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_130(i10, i31, i32, env, static) -{0,0}> log_Load_184(i10, i31, i32, env, static) :|: i32 <= 2 && i32 <= 3 && 2 <= i10 && 1 <= i32 && 1 <= i31
log_Load_184(i10, i59, i60, env, static) -{0,0}> log_Load_230(i10, i59, i60, env, static) :|: i60 <= 3 && 2 <= i10 && 1 <= i60 && 1 <= i59
log_Load_230(i10, i89, i90, env, static) -{1,1}> log_ConstantStackPush_234(i10, i89, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 1 <= i89
log_ConstantStackPush_234(i10, i89, i90, env, static) -{1,1}> log_LE_245(i10, i89, iconst_1, i90, env, static) :|: 1 <= i90 && iconst_1 = 1 && 2 <= i10 && 1 <= i89
log_LE_245(i10, i102, iconst_1, i90, env, static) -{0,0}> log_LE_251(i10, i102, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_LE_251(i10, i102, iconst_1, i90, env, static) -{1,1}> log_Load_262(i10, i102, i90, env, static) :|: 1 <= i90 && iconst_1 < i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_Load_262(i10, i102, i90, env, static) -{1,1}> log_ConstantStackPush_264(i10, i102, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102
log_ConstantStackPush_264(i10, i102, i90, env, static) -{1,1}> log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) -{1,1}> log_Store_269(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && i106 < i102 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_Store_269(i10, i106, i90, env, static) -{1,1}> log_Inc_273(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && 2 <= i10
log_Inc_273(i10, i106, i90, env, static) -{1,1}> log_JMP_276(i10, i106, i109, env, static) :|: i90 + 1 = i109 && 1 <= i106 && 1 <= i90 && 2 <= i109 && 2 <= i10
log_JMP_276(i10, i106, i109, env, static) -{1,1}> log_Load_281(i10, i106, i109, env, static) :|: 1 <= i106 && 2 <= i109 && 2 <= i10
log_Load_281(i10, i106, i109, env, static) -{0,0}> log_Load_230(i10, i106, i109, env, static) :|: 1 <= i106 && 1 <= i109 && 2 <= i109 && 2 <= i10

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

obtained
log_ConstantStackPush_2(i2, env, static) -{26,26}> log_Load_230(i2, i12', 1, env, static'1) :|: i12' < i2 && 1 <= i12' && static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 2 <= i2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 1 <= 2 && 1 < i2 && 0 <= static'1 && 0 < 2 && 0 >= 0
by chaining
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_3(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_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: NULL = 0 && 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_Load_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> log_ConstantStackPush_43(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_43(i2, env, static) -{0,0}> log_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_45(i2, env, static) -{0,0}> log_ConstantStackPush_48(i2, env, static) :|: 0 <= static
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_50(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i10, iconst_1, iconst_0, env, static) -{0,0}> log_LE_60(i10, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_LE_60(i10, iconst_1, iconst_0, env, static) -{1,1}> log_Load_64(i10, iconst_0, env, static) :|: iconst_1 < i10 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i10
log_Load_64(i10, iconst_0, env, static) -{1,1}> log_ConstantStackPush_69(i10, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10
log_ConstantStackPush_69(i10, iconst_0, env, static) -{1,1}> log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2
log_IntArithmetic_74(i10, iconst_2, iconst_0, env, static) -{1,1}> log_Store_81(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && iconst_2 = 2 && 1 <= i12 && i12 < i10
log_Store_81(i10, i12, iconst_0, env, static) -{1,1}> log_Inc_82(i10, i12, iconst_0, env, static) :|: iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_Inc_82(i10, i12, iconst_0, env, static) -{1,1}> log_JMP_83(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 2 <= i10 && 1 <= i12
log_JMP_83(i10, i12, iconst_1, env, static) -{1,1}> log_Load_84(i10, i12, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_84(i10, i12, iconst_1, env, static) -{0,0}> log_Load_130(i10, i12, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 2 <= i10 && 1 <= i12
log_Load_130(i10, i31, i32, env, static) -{0,0}> log_Load_184(i10, i31, i32, env, static) :|: i32 <= 2 && i32 <= 3 && 2 <= i10 && 1 <= i32 && 1 <= i31
log_Load_184(i10, i59, i60, env, static) -{0,0}> log_Load_230(i10, i59, i60, env, static) :|: i60 <= 3 && 2 <= i10 && 1 <= i60 && 1 <= i59

obtained
log_Load_230(i10, i89, i90, env, static) -{9,9}> log_Load_230(i10, i106', i109', env, static) :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i89 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89
by chaining
log_Load_230(i10, i89, i90, env, static) -{1,1}> log_ConstantStackPush_234(i10, i89, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 1 <= i89
log_ConstantStackPush_234(i10, i89, i90, env, static) -{1,1}> log_LE_245(i10, i89, iconst_1, i90, env, static) :|: 1 <= i90 && iconst_1 = 1 && 2 <= i10 && 1 <= i89
log_LE_245(i10, i102, iconst_1, i90, env, static) -{0,0}> log_LE_251(i10, i102, iconst_1, i90, env, static) :|: 1 <= i90 && 1 <= i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_LE_251(i10, i102, iconst_1, i90, env, static) -{1,1}> log_Load_262(i10, i102, i90, env, static) :|: 1 <= i90 && iconst_1 < i102 && iconst_1 = 1 && 2 <= i10 && 2 <= i102
log_Load_262(i10, i102, i90, env, static) -{1,1}> log_ConstantStackPush_264(i10, i102, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102
log_ConstantStackPush_264(i10, i102, i90, env, static) -{1,1}> log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) :|: 1 <= i90 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_IntArithmetic_266(i10, i102, iconst_2, i90, env, static) -{1,1}> log_Store_269(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && i106 < i102 && 2 <= i10 && 2 <= i102 && iconst_2 = 2
log_Store_269(i10, i106, i90, env, static) -{1,1}> log_Inc_273(i10, i106, i90, env, static) :|: 1 <= i106 && 1 <= i90 && 2 <= i10
log_Inc_273(i10, i106, i90, env, static) -{1,1}> log_JMP_276(i10, i106, i109, env, static) :|: i90 + 1 = i109 && 1 <= i106 && 1 <= i90 && 2 <= i109 && 2 <= i10
log_JMP_276(i10, i106, i109, env, static) -{1,1}> log_Load_281(i10, i106, i109, env, static) :|: 1 <= i106 && 2 <= i109 && 2 <= i10
log_Load_281(i10, i106, i109, env, static) -{0,0}> log_Load_230(i10, i106, i109, env, static) :|: 1 <= i106 && 1 <= i109 && 2 <= i109 && 2 <= i10

(36) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i2, env, static) -{26,26}> log_Load_230(i2, i12', 1, env, static'1) :|: i12' < i2 && 1 <= i12' && static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 2 <= i2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 1 <= 2 && 1 < i2 && 0 <= static'1 && 0 < 2 && 0 >= 0
log_Load_230(i10, i89, i90, env, static) -{9,9}> log_Load_230(i10, i106', i109', env, static) :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i89 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89

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

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

log_ConstantStackPush_2(x1, x2, x3) → log_ConstantStackPush_2(x1, x3)
log_Load_230(x1, x2, x3, x4, x5) → log_Load_230(x1, x2, x3)

(38) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i2, static) -{26,26}> log_Load_230(i2, i12', 1) :|: i12' < i2 && 1 <= i12' && static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 2 <= i2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 1 <= 2 && 1 < i2 && 0 <= static'1 && 0 < 2 && 0 >= 0
log_Load_230(i10, i89, i90) -{9,9}> log_Load_230(i10, i106', i109') :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i89 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89

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

Moved arithmethic from constraints to rhss.

log_Load_230(i10, i89, i90) -{9,9}> log_Load_230(i10, i106', i109') :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i89 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89
was transformed to
log_Load_230(i10, i89, i90) -{9,9}> log_Load_230(i10, i106', i90 + 1) :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i89 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89

(40) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i2, static) -{26,26}> log_Load_230(i2, i12', 1) :|: i12' < i2 && 1 <= i12' && static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 2 <= i2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 1 <= 2 && 1 < i2 && 0 <= static'1 && 0 < 2 && 0 >= 0
log_Load_230(i10, i89, i90) -{9,9}> log_Load_230(i10, i106', i90 + 1) :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i89 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89

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

Simplified expressions.

log_ConstantStackPush_2(i2, static) -{26,26}> log_Load_230(i2, i12', 1) :|: i12' < i2 && 1 <= i12' && static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 2 <= i2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 1 <= 2 && 1 < i2 && 0 <= static'1 && 0 < 2 && 0 >= 0
was transformed to
log_ConstantStackPush_2(i2, static) -{26,26}> log_Load_230(i2, i12', 1) :|: i12' < i2 && 1 <= i12' && static'1 <= static''' + 1 && 2 <= i2 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 1 < i2 && 0 <= static'1

log_Load_230(i10, i89, i90) -{9,9}> log_Load_230(i10, i106', i90 + 1) :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i89 && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89
was transformed to
log_Load_230(i10, i89, i90) -{9,9}> log_Load_230(i10, i106', i90 + 1) :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89

(42) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
log_Load_230(i10, i89, i90) -{9,9}> log_Load_230(i10, i106', i90 + 1) :|: 1 < i89 && 2 <= i10 && 2 <= i89 && 2 <= i109' && 1 <= i106' && 1 <= i109' && 1 <= i90 && i90 + 1 = i109' && i106' < i89
log_ConstantStackPush_2(i2, static) -{26,26}> log_Load_230(i2, i12', 1) :|: i12' < i2 && 1 <= i12' && static'1 <= static''' + 1 && 2 <= i2 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 1 < i2 && 0 <= static'1

(43) koat Proof (EQUIVALENT transformation)

YES(?, 9*ar_0 + 26)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 9) log_Load_230(ar_0, ar_1, ar_2) -> Com_1(log_Load_230(ar_0, i106', ar_2 + 1)) [ 1 < ar_1 /\ 2 <= ar_0 /\ 2 <= ar_1 /\ 2 <= i109' /\ 1 <= i106' /\ 1 <= i109' /\ 1 <= ar_2 /\ ar_2 + 1 = i109' /\ i106' < ar_1 ]
(Comp: ?, Cost: 26) log_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(log_Load_230(ar_0, i12', 1)) [ i12' < ar_0 /\ 1 <= i12' /\ static'1 <= static''' + 1 /\ 2 <= ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 1 < ar_0 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(log_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 9) log_Load_230(ar_0, ar_1, ar_2) -> Com_1(log_Load_230(ar_0, i106', ar_2 + 1)) [ 1 < ar_1 /\ 2 <= ar_0 /\ 2 <= ar_1 /\ 2 <= i109' /\ 1 <= i106' /\ 1 <= i109' /\ 1 <= ar_2 /\ ar_2 + 1 = i109' /\ i106' < ar_1 ]
(Comp: 1, Cost: 26) log_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(log_Load_230(ar_0, i12', 1)) [ i12' < ar_0 /\ 1 <= i12' /\ static'1 <= static''' + 1 /\ 2 <= ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 1 < ar_0 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(log_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(log_Load_230) = V_2
Pol(log_ConstantStackPush_2) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
log_Load_230(ar_0, ar_1, ar_2) -> Com_1(log_Load_230(ar_0, i106', ar_2 + 1)) [ 1 < ar_1 /\ 2 <= ar_0 /\ 2 <= ar_1 /\ 2 <= i109' /\ 1 <= i106' /\ 1 <= i109' /\ 1 <= ar_2 /\ ar_2 + 1 = i109' /\ i106' < ar_1 ]
strictly and produces the following problem:
3: T:
(Comp: ar_0, Cost: 9) log_Load_230(ar_0, ar_1, ar_2) -> Com_1(log_Load_230(ar_0, i106', ar_2 + 1)) [ 1 < ar_1 /\ 2 <= ar_0 /\ 2 <= ar_1 /\ 2 <= i109' /\ 1 <= i106' /\ 1 <= i109' /\ 1 <= ar_2 /\ ar_2 + 1 = i109' /\ i106' < ar_1 ]
(Comp: 1, Cost: 26) log_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(log_Load_230(ar_0, i12', 1)) [ i12' < ar_0 /\ 1 <= i12' /\ static'1 <= static''' + 1 /\ 2 <= ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 1 < ar_0 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(log_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 9*ar_0 + 26

Time: 0.160 sec (SMT: 0.151 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

(43) koat Proof (EQUIVALENT transformation)

(44) BOUNDS(CONSTANT, 26 + 9 * |#0|)