(0) Obligation:
Need to prove time_complexity of the following program:
public class LogIterative {
public static int log(int x, int y) {
int res = 0;
while (x >= y && y > 1) {
res++;
x = x/y;
}
return res;
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
LogIterative.log(II)I: Graph of 61 nodes with 1 SCC.
(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)) transformation)
Extracted set of 49 edges for the analysis of TIME complexity. Dropped leaves.
(4) 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
(5) 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.
(6) Obligation:
IntTrs with 49 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104
(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
log_ConstantStackPush_1(
i1,
i4,
env,
static) -{22,22}>
log_LE_299(
i1,
i4,
1,
i1,
0,
env,
static'1) :|:
static'1 <=
static''' +
1 &&
0 <=
0 &&
0 <=
static''' &&
0 <=
2 &&
static''' <=
static +
2 &&
0 <
1 &&
0 <=
static &&
0 <=
static'1 && 0 >= 0 &&
i4 <=
i1 &&
0 <
2 &&
0 <=
1by chaining
log_ConstantStackPush_1(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_3(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_3(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_14(
a2,
i1,
i4,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_14(
a2,
i1,
i4,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_16(
i1,
i4,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_16(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
i1,
i4,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_18(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_New_19(
i1,
i4,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_19(
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o2,
i1,
i4,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_21(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_22(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_22(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i1,
i4,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Load_26(
o2,
i1,
i4,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_26(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_28(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_28(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Load_29(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Load_29(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_32(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_32(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Return_35(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Return_37(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Return_37(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_44(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_44(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_Return_47(
i1,
i4,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_47(
i1,
i4,
env,
static) -{1,1}>
log_ConstantStackPush_48(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_48(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_49(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_49(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_50(
i1,
i4,
env,
static) :|:
0 <=
staticlog_ConstantStackPush_50(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_51(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_51(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_52(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_52(
i1,
i4,
env,
static) -{1,1}>
log_Store_53(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Store_53(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_Load_54(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Load_54(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_Load_55(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Load_55(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_LT_58(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_LT_58(
i1,
i4,
iconst_0,
env,
static) -{0,0}>
log_LT_63(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0 &&
i4 <=
i1log_LT_63(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_Load_68(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0 &&
i4 <=
i1log_Load_68(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_ConstantStackPush_72(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_ConstantStackPush_72(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_LE_74(
i1,
i4,
iconst_1,
iconst_0,
env,
static) :|:
iconst_1 =
1 &&
iconst_0 =
0log_LE_74(
i1,
i4,
iconst_1,
iconst_0,
env,
static) -{0,0}>
log_LE_159(
i1,
i4,
iconst_1,
i1,
iconst_0,
env,
static) :|:
0 <=
iconst_0 &&
iconst_0 <=
1 &&
iconst_1 =
1 &&
iconst_0 =
0log_LE_159(
i29,
i30,
iconst_1,
i31,
i32,
env,
static) -{0,0}>
log_LE_225(
i29,
i30,
iconst_1,
i31,
i32,
env,
static) :|:
i32 <=
2 &&
iconst_1 =
1 &&
0 <=
i32 &&
i32 <=
1log_LE_225(
i60,
i61,
iconst_1,
i62,
i63,
env,
static) -{0,0}>
log_LE_299(
i60,
i61,
iconst_1,
i62,
i63,
env,
static) :|:
i63 <=
2 &&
iconst_1 =
1 &&
0 <=
i63obtained
log_LE_299(i105, i104, 1, i106, i94, env, static) -{12,12}> log_LE_299(i105, i104, 1, i111', i110', env, static) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
by chaining
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104
(8) Obligation:
IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{22,22}> log_LE_299(i1, i4, 1, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
log_LE_299(i105, i104, 1, i106, i94, env, static) -{12,12}> log_LE_299(i105, i104, 1, i111', i110', env, static) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
(9) 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_1(x1, x2, x3, x4) → log_ConstantStackPush_1(x1, x2, x4)
log_LE_299(x1, x2, x3, x4, x5, x6, x7) → log_LE_299(x1, x2, x4, x5)
(10) Obligation:
IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i110') :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
(11) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i110') :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
was transformed to
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i94 + 1) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
(12) Obligation:
IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i94 + 1) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
(13) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
was transformed to
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 <= i1
(14) Obligation:
IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i94 + 1) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 <= i1
(15) koat Proof (EQUIVALENT transformation)
YES(?, 12*ar_0 + 22)
Initial complexity problem:
1: T:
(Comp: ?, Cost: 12) log_LE_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, i111', ar_3 + 1)) [ 1 < ar_1 /\ 2 <= ar_1 /\ 2 <= ar_2 /\ 2 <= i111' /\ ar_1 <= i111' /\ 0 <= i110' /\ 1 <= i110' /\ 2 <= ar_0 /\ i111' < ar_2 /\ 0 <= i111' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: ?, Cost: 22) log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, ar_0, 0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 12) log_LE_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, i111', ar_3 + 1)) [ 1 < ar_1 /\ 2 <= ar_1 /\ 2 <= ar_2 /\ 2 <= i111' /\ ar_1 <= i111' /\ 0 <= i110' /\ 1 <= i110' /\ 2 <= ar_0 /\ i111' < ar_2 /\ 0 <= i111' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: 1, Cost: 22) log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, ar_0, 0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
A polynomial rank function with
Pol(log_LE_299) = V_3
Pol(log_ConstantStackPush_1) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
log_LE_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, i111', ar_3 + 1)) [ 1 < ar_1 /\ 2 <= ar_1 /\ 2 <= ar_2 /\ 2 <= i111' /\ ar_1 <= i111' /\ 0 <= i110' /\ 1 <= i110' /\ 2 <= ar_0 /\ i111' < ar_2 /\ 0 <= i111' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0, Cost: 12) log_LE_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, i111', ar_3 + 1)) [ 1 < ar_1 /\ 2 <= ar_1 /\ 2 <= ar_2 /\ 2 <= i111' /\ ar_1 <= i111' /\ 0 <= i110' /\ 1 <= i110' /\ 2 <= ar_0 /\ i111' < ar_2 /\ 0 <= i111' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: 1, Cost: 22) log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, ar_0, 0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Complexity upper bound 12*ar_0 + 22
Time: 0.110 sec (SMT: 0.102 sec)
(16) BOUNDS(CONSTANT, 22 + 12 * |#0|)
(17) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)) transformation)
Extracted set of 52 edges for the analysis of TIME complexity. Kept leaves.
(18) Obligation:
Set of 52 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
(19) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 52 jbc graph edges to a weighted ITS with 52 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.
(20) Obligation:
IntTrs with 52 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104
(21) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
log_ConstantStackPush_1(
i1,
i4,
env,
static) -{19,19}>
log_LT_58(
i1,
i4,
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''' +
1by chaining
log_ConstantStackPush_1(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_3(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_3(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_14(
a2,
i1,
i4,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_14(
a2,
i1,
i4,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_16(
i1,
i4,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_16(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
i1,
i4,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_18(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_New_19(
i1,
i4,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_19(
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o2,
i1,
i4,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_21(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_22(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_22(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i1,
i4,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Load_26(
o2,
i1,
i4,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_26(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_28(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_28(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Load_29(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Load_29(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_32(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_32(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Return_35(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Return_37(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Return_37(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_44(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_44(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_Return_47(
i1,
i4,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_47(
i1,
i4,
env,
static) -{1,1}>
log_ConstantStackPush_48(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_48(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_49(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_49(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_50(
i1,
i4,
env,
static) :|:
0 <=
staticlog_ConstantStackPush_50(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_51(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_51(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_52(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_52(
i1,
i4,
env,
static) -{1,1}>
log_Store_53(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Store_53(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_Load_54(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Load_54(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_Load_55(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Load_55(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_LT_58(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0obtained
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
by chaining
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
obtained
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
by chaining
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
obtained
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
by chaining
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104
(22) Obligation:
IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
(23) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from lhss to constraints.
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
was transformed to
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
(24) Obligation:
IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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
(25) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
was transformed to
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
was transformed to
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
(26) Obligation:
IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
(27) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
was transformed to
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: i4 <= i1 && x = 0
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
(28) Obligation:
IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: i4 <= i1 && x = 0
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
(29) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 52 jbc graph edges to a weighted ITS with 52 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.
(30) Obligation:
IntTrs with 52 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i106 / i104 = i111 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104
(31) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
log_ConstantStackPush_1(
i1,
i4,
env,
static) -{19,19}>
log_LT_58(
i1,
i4,
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''' +
1by chaining
log_ConstantStackPush_1(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_3(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_3(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_14(
a2,
i1,
i4,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_14(
a2,
i1,
i4,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_16(
i1,
i4,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_16(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
i1,
i4,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_18(
i1,
i4,
env,
static) -{0,0}>
langle_clinit_rangle_New_19(
i1,
i4,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_19(
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o2,
i1,
i4,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_21(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_22(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_22(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i1,
i4,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Load_26(
o2,
i1,
i4,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_26(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_28(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_28(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Load_29(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Load_29(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_32(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_32(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Return_35(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_init_rangle_Return_37(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_init_rangle_Return_37(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_44(
o2,
i1,
i4,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_44(
o2,
i1,
i4,
env,
static) -{1,1}>
langle_clinit_rangle_Return_47(
i1,
i4,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_47(
i1,
i4,
env,
static) -{1,1}>
log_ConstantStackPush_48(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_48(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_49(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_49(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_50(
i1,
i4,
env,
static) :|:
0 <=
staticlog_ConstantStackPush_50(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_51(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_51(
i1,
i4,
env,
static) -{0,0}>
log_ConstantStackPush_52(
i1,
i4,
env,
static) :|: 0 >= 0
log_ConstantStackPush_52(
i1,
i4,
env,
static) -{1,1}>
log_Store_53(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Store_53(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_Load_54(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Load_54(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_Load_55(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0log_Load_55(
i1,
i4,
iconst_0,
env,
static) -{1,1}>
log_LT_58(
i1,
i4,
iconst_0,
env,
static) :|:
iconst_0 =
0obtained
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
by chaining
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
obtained
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
by chaining
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i106 / i104 = i111 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
obtained
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
by chaining
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104
(32) Obligation:
IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
(33) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from lhss to constraints.
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
was transformed to
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
(34) Obligation:
IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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
(35) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)
Removed div and mod.
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, x, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
(36) Obligation:
IntTrs with 8 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, x, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
(37) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
was transformed to
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
was transformed to
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, x, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, 1, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
(38) Obligation:
IntTrs with 8 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, 1, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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
(39) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
was transformed to
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: i4 <= i1 && x = 0
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 + -1 * i104 * div < i104 && 0 < i106 + -1 * i104 * div + i104 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 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_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
(40) Obligation:
IntTrs with 8 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, 1, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: i4 <= i1 && x = 0
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 + -1 * i104 * div < i104 && 0 < i106 + -1 * i104 * div + i104 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1