unknown Initial ITS Start location: l6 Program variables: __const_50^0 i5^0 i^0 tmp^0 0: l0 -> l1 : __const_50^0'=__const_50^post1, i5^0'=i5^post1, i^0'=i^post1, tmp^0'=tmp^post1, (i^post1 == 0 /\ __const_50^0-i5^0 <= 0 /\ tmp^0-tmp^post1 == 0 /\ -__const_50^post1+__const_50^0 == 0 /\ -i5^post1+i5^0 == 0), cost: 1 1: l0 -> l2 : __const_50^0'=__const_50^post2, i5^0'=i5^post2, i^0'=i^post2, tmp^0'=tmp^post2, (-i^post2+i^0 == 0 /\ -1+i5^post2-i5^0 == 0 /\ __const_50^0-__const_50^post2 == 0 /\ 1-__const_50^0+i5^0 <= 0 /\ tmp^0-tmp^post2 == 0), cost: 1 3: l1 -> l3 : __const_50^0'=__const_50^post4, i5^0'=i5^post4, i^0'=i^post4, tmp^0'=tmp^post4, (-__const_50^post4+__const_50^0 == 0 /\ -i5^post4+i5^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ i^0-i^post4 == 0), cost: 1 2: l2 -> l0 : __const_50^0'=__const_50^post3, i5^0'=i5^post3, i^0'=i^post3, tmp^0'=tmp^post3, (-i^post3+i^0 == 0 /\ -__const_50^post3+__const_50^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ -i5^post3+i5^0 == 0), cost: 1 4: l3 -> l4 : __const_50^0'=__const_50^post5, i5^0'=i5^post5, i^0'=i^post5, tmp^0'=tmp^post5, (-i^post5+i^0 == 0 /\ __const_50^0-i^0 <= 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_50^post5+__const_50^0 == 0 /\ -i5^post5+i5^0 == 0), cost: 1 5: l3 -> l1 : __const_50^0'=__const_50^post6, i5^0'=i5^post6, i^0'=i^post6, tmp^0'=tmp^post6, (-i5^post6+i5^0 == 0 /\ -1+i^post6-i^0 == 0 /\ 1-__const_50^0+i^0 <= 0 /\ tmp^0-tmp^post6 == 0 /\ -__const_50^post6+__const_50^0 == 0), cost: 1 6: l5 -> l2 : __const_50^0'=__const_50^post7, i5^0'=i5^post7, i^0'=i^post7, tmp^0'=tmp^post7, (0 == 0 /\ i5^post7 == 0 /\ -__const_50^post7+__const_50^0 == 0 /\ i^post7 == 0 /\ i5^1 == 0), cost: 1 7: l6 -> l5 : __const_50^0'=__const_50^post8, i5^0'=i5^post8, i^0'=i^post8, tmp^0'=tmp^post8, (tmp^0-tmp^post8 == 0 /\ -i5^post8+i5^0 == 0 /\ -i^post8+i^0 == 0 /\ -__const_50^post8+__const_50^0 == 0), cost: 1 Chained Linear Paths Start location: l6 Program variables: __const_50^0 i5^0 i^0 tmp^0 0: l0 -> l1 : __const_50^0'=__const_50^post1, i5^0'=i5^post1, i^0'=i^post1, tmp^0'=tmp^post1, (i^post1 == 0 /\ __const_50^0-i5^0 <= 0 /\ tmp^0-tmp^post1 == 0 /\ -__const_50^post1+__const_50^0 == 0 /\ -i5^post1+i5^0 == 0), cost: 1 1: l0 -> l2 : __const_50^0'=__const_50^post2, i5^0'=i5^post2, i^0'=i^post2, tmp^0'=tmp^post2, (-i^post2+i^0 == 0 /\ -1+i5^post2-i5^0 == 0 /\ __const_50^0-__const_50^post2 == 0 /\ 1-__const_50^0+i5^0 <= 0 /\ tmp^0-tmp^post2 == 0), cost: 1 3: l1 -> l3 : __const_50^0'=__const_50^post4, i5^0'=i5^post4, i^0'=i^post4, tmp^0'=tmp^post4, (-__const_50^post4+__const_50^0 == 0 /\ -i5^post4+i5^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ i^0-i^post4 == 0), cost: 1 2: l2 -> l0 : __const_50^0'=__const_50^post3, i5^0'=i5^post3, i^0'=i^post3, tmp^0'=tmp^post3, (-i^post3+i^0 == 0 /\ -__const_50^post3+__const_50^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ -i5^post3+i5^0 == 0), cost: 1 4: l3 -> l4 : __const_50^0'=__const_50^post5, i5^0'=i5^post5, i^0'=i^post5, tmp^0'=tmp^post5, (-i^post5+i^0 == 0 /\ __const_50^0-i^0 <= 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_50^post5+__const_50^0 == 0 /\ -i5^post5+i5^0 == 0), cost: 1 5: l3 -> l1 : __const_50^0'=__const_50^post6, i5^0'=i5^post6, i^0'=i^post6, tmp^0'=tmp^post6, (-i5^post6+i5^0 == 0 /\ -1+i^post6-i^0 == 0 /\ 1-__const_50^0+i^0 <= 0 /\ tmp^0-tmp^post6 == 0 /\ -__const_50^post6+__const_50^0 == 0), cost: 1 8: l6 -> l2 : __const_50^0'=__const_50^post7, i5^0'=i5^post7, i^0'=i^post7, tmp^0'=tmp^post7, (0 == 0 /\ tmp^0-tmp^post8 == 0 /\ -i5^post8+i5^0 == 0 /\ -__const_50^post7+__const_50^post8 == 0 /\ i5^post7 == 0 /\ -i^post8+i^0 == 0 /\ i^post7 == 0 /\ -__const_50^post8+__const_50^0 == 0 /\ i5^1 == 0), cost: 1 Eliminating location l5 by chaining: Applied chaining First rule: l6 -> l5 : __const_50^0'=__const_50^post8, i5^0'=i5^post8, i^0'=i^post8, tmp^0'=tmp^post8, (tmp^0-tmp^post8 == 0 /\ -i5^post8+i5^0 == 0 /\ -i^post8+i^0 == 0 /\ -__const_50^post8+__const_50^0 == 0), cost: 1 Second rule: l5 -> l2 : __const_50^0'=__const_50^post7, i5^0'=i5^post7, i^0'=i^post7, tmp^0'=tmp^post7, (0 == 0 /\ i5^post7 == 0 /\ -__const_50^post7+__const_50^0 == 0 /\ i^post7 == 0 /\ i5^1 == 0), cost: 1 New rule: l6 -> l2 : __const_50^0'=__const_50^post7, i5^0'=i5^post7, i^0'=i^post7, tmp^0'=tmp^post7, (0 == 0 /\ tmp^0-tmp^post8 == 0 /\ -i5^post8+i5^0 == 0 /\ -__const_50^post7+__const_50^post8 == 0 /\ i5^post7 == 0 /\ -i^post8+i^0 == 0 /\ i^post7 == 0 /\ -__const_50^post8+__const_50^0 == 0 /\ i5^1 == 0), cost: 1 Applied deletion Removed the following rules: 6 7 Simplified Transitions Start location: l6 Program variables: __const_50^0 i5^0 i^0 tmp^0 9: l0 -> l1 : i^0'=0, __const_50^0-i5^0 <= 0, cost: 1 10: l0 -> l2 : i5^0'=1+i5^0, 1-__const_50^0+i5^0 <= 0, cost: 1 12: l1 -> l3 : T, cost: 1 11: l2 -> l0 : T, cost: 1 13: l3 -> l4 : __const_50^0-i^0 <= 0, cost: 1 14: l3 -> l1 : i^0'=1+i^0, 1-__const_50^0+i^0 <= 0, cost: 1 15: l6 -> l2 : i5^0'=0, i^0'=0, tmp^0'=tmp^post7, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __const_50^0'=__const_50^post1, i5^0'=i5^post1, i^0'=i^post1, tmp^0'=tmp^post1, (i^post1 == 0 /\ __const_50^0-i5^0 <= 0 /\ tmp^0-tmp^post1 == 0 /\ -__const_50^post1+__const_50^0 == 0 /\ -i5^post1+i5^0 == 0), cost: 1 New rule: l0 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=0, tmp^0'=tmp^0, (0 == 0 /\ __const_50^0-i5^0 <= 0), cost: 1 propagated equality i^post1 = 0 propagated equality tmp^post1 = tmp^0 propagated equality __const_50^post1 = __const_50^0 propagated equality i5^post1 = i5^0 Simplified Guard Original rule: l0 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=0, tmp^0'=tmp^0, (0 == 0 /\ __const_50^0-i5^0 <= 0), cost: 1 New rule: l0 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=0, tmp^0'=tmp^0, __const_50^0-i5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=0, tmp^0'=tmp^0, __const_50^0-i5^0 <= 0, cost: 1 New rule: l0 -> l1 : i^0'=0, __const_50^0-i5^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : __const_50^0'=__const_50^post2, i5^0'=i5^post2, i^0'=i^post2, tmp^0'=tmp^post2, (-i^post2+i^0 == 0 /\ -1+i5^post2-i5^0 == 0 /\ __const_50^0-__const_50^post2 == 0 /\ 1-__const_50^0+i5^0 <= 0 /\ tmp^0-tmp^post2 == 0), cost: 1 New rule: l0 -> l2 : __const_50^0'=__const_50^0, i5^0'=1+i5^0, i^0'=i^0, tmp^0'=tmp^0, (0 == 0 /\ 1-__const_50^0+i5^0 <= 0), cost: 1 propagated equality i^post2 = i^0 propagated equality i5^post2 = 1+i5^0 propagated equality __const_50^post2 = __const_50^0 propagated equality tmp^post2 = tmp^0 Simplified Guard Original rule: l0 -> l2 : __const_50^0'=__const_50^0, i5^0'=1+i5^0, i^0'=i^0, tmp^0'=tmp^0, (0 == 0 /\ 1-__const_50^0+i5^0 <= 0), cost: 1 New rule: l0 -> l2 : __const_50^0'=__const_50^0, i5^0'=1+i5^0, i^0'=i^0, tmp^0'=tmp^0, 1-__const_50^0+i5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : __const_50^0'=__const_50^0, i5^0'=1+i5^0, i^0'=i^0, tmp^0'=tmp^0, 1-__const_50^0+i5^0 <= 0, cost: 1 New rule: l0 -> l2 : i5^0'=1+i5^0, 1-__const_50^0+i5^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l0 : __const_50^0'=__const_50^post3, i5^0'=i5^post3, i^0'=i^post3, tmp^0'=tmp^post3, (-i^post3+i^0 == 0 /\ -__const_50^post3+__const_50^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ -i5^post3+i5^0 == 0), cost: 1 New rule: l2 -> l0 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, 0 == 0, cost: 1 propagated equality i^post3 = i^0 propagated equality __const_50^post3 = __const_50^0 propagated equality tmp^post3 = tmp^0 propagated equality i5^post3 = i5^0 Simplified Guard Original rule: l2 -> l0 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, 0 == 0, cost: 1 New rule: l2 -> l0 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, T, cost: 1 New rule: l2 -> l0 : T, cost: 1 Propagated Equalities Original rule: l1 -> l3 : __const_50^0'=__const_50^post4, i5^0'=i5^post4, i^0'=i^post4, tmp^0'=tmp^post4, (-__const_50^post4+__const_50^0 == 0 /\ -i5^post4+i5^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ i^0-i^post4 == 0), cost: 1 New rule: l1 -> l3 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, 0 == 0, cost: 1 propagated equality __const_50^post4 = __const_50^0 propagated equality i5^post4 = i5^0 propagated equality tmp^post4 = tmp^0 propagated equality i^post4 = i^0 Simplified Guard Original rule: l1 -> l3 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, 0 == 0, cost: 1 New rule: l1 -> l3 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l3 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, T, cost: 1 New rule: l1 -> l3 : T, cost: 1 Propagated Equalities Original rule: l3 -> l4 : __const_50^0'=__const_50^post5, i5^0'=i5^post5, i^0'=i^post5, tmp^0'=tmp^post5, (-i^post5+i^0 == 0 /\ __const_50^0-i^0 <= 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_50^post5+__const_50^0 == 0 /\ -i5^post5+i5^0 == 0), cost: 1 New rule: l3 -> l4 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, (0 == 0 /\ __const_50^0-i^0 <= 0), cost: 1 propagated equality i^post5 = i^0 propagated equality tmp^post5 = tmp^0 propagated equality __const_50^post5 = __const_50^0 propagated equality i5^post5 = i5^0 Simplified Guard Original rule: l3 -> l4 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, (0 == 0 /\ __const_50^0-i^0 <= 0), cost: 1 New rule: l3 -> l4 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, __const_50^0-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=i^0, tmp^0'=tmp^0, __const_50^0-i^0 <= 0, cost: 1 New rule: l3 -> l4 : __const_50^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l1 : __const_50^0'=__const_50^post6, i5^0'=i5^post6, i^0'=i^post6, tmp^0'=tmp^post6, (-i5^post6+i5^0 == 0 /\ -1+i^post6-i^0 == 0 /\ 1-__const_50^0+i^0 <= 0 /\ tmp^0-tmp^post6 == 0 /\ -__const_50^post6+__const_50^0 == 0), cost: 1 New rule: l3 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=1+i^0, tmp^0'=tmp^0, (0 == 0 /\ 1-__const_50^0+i^0 <= 0), cost: 1 propagated equality i5^post6 = i5^0 propagated equality i^post6 = 1+i^0 propagated equality tmp^post6 = tmp^0 propagated equality __const_50^post6 = __const_50^0 Simplified Guard Original rule: l3 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=1+i^0, tmp^0'=tmp^0, (0 == 0 /\ 1-__const_50^0+i^0 <= 0), cost: 1 New rule: l3 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=1+i^0, tmp^0'=tmp^0, 1-__const_50^0+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : __const_50^0'=__const_50^0, i5^0'=i5^0, i^0'=1+i^0, tmp^0'=tmp^0, 1-__const_50^0+i^0 <= 0, cost: 1 New rule: l3 -> l1 : i^0'=1+i^0, 1-__const_50^0+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l2 : __const_50^0'=__const_50^post7, i5^0'=i5^post7, i^0'=i^post7, tmp^0'=tmp^post7, (0 == 0 /\ tmp^0-tmp^post8 == 0 /\ -i5^post8+i5^0 == 0 /\ -__const_50^post7+__const_50^post8 == 0 /\ i5^post7 == 0 /\ -i^post8+i^0 == 0 /\ i^post7 == 0 /\ -__const_50^post8+__const_50^0 == 0 /\ i5^1 == 0), cost: 1 New rule: l6 -> l2 : __const_50^0'=__const_50^post8, i5^0'=0, i^0'=0, tmp^0'=tmp^post7, (0 == 0 /\ tmp^0-tmp^post8 == 0 /\ -i5^post8+i5^0 == 0 /\ -i^post8+i^0 == 0 /\ -__const_50^post8+__const_50^0 == 0 /\ i5^1 == 0), cost: 1 propagated equality __const_50^post7 = __const_50^post8 propagated equality i5^post7 = 0 propagated equality i^post7 = 0 Propagated Equalities Original rule: l6 -> l2 : __const_50^0'=__const_50^post8, i5^0'=0, i^0'=0, tmp^0'=tmp^post7, (0 == 0 /\ tmp^0-tmp^post8 == 0 /\ -i5^post8+i5^0 == 0 /\ -i^post8+i^0 == 0 /\ -__const_50^post8+__const_50^0 == 0 /\ i5^1 == 0), cost: 1 New rule: l6 -> l2 : __const_50^0'=__const_50^0, i5^0'=0, i^0'=0, tmp^0'=tmp^post7, 0 == 0, cost: 1 propagated equality tmp^post8 = tmp^0 propagated equality i5^post8 = i5^0 propagated equality i^post8 = i^0 propagated equality __const_50^post8 = __const_50^0 propagated equality i5^1 = 0 Simplified Guard Original rule: l6 -> l2 : __const_50^0'=__const_50^0, i5^0'=0, i^0'=0, tmp^0'=tmp^post7, 0 == 0, cost: 1 New rule: l6 -> l2 : __const_50^0'=__const_50^0, i5^0'=0, i^0'=0, tmp^0'=tmp^post7, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l2 : __const_50^0'=__const_50^0, i5^0'=0, i^0'=0, tmp^0'=tmp^post7, T, cost: 1 New rule: l6 -> l2 : i5^0'=0, i^0'=0, tmp^0'=tmp^post7, T, cost: 1 Step with 15 Trace 15[T] Blocked [{}, {}] Step with 11 Trace 15[T], 11[T] Blocked [{}, {}, {}] Step with 9 Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 12 Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T] Blocked [{}, {}, {}, {}, {}] Step with 13 Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T], 13[(__const_50^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}] Backtrack Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T] Blocked [{}, {}, {}, {}, {13[T]}] Backtrack Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)] Blocked [{}, {}, {}, {12[T]}] Backtrack Trace 15[T], 11[T] Blocked [{}, {}, {9[T]}] Step with 10 Trace 15[T], 11[T], 10[(1-__const_50^0+i5^0 <= 0)] Blocked [{}, {}, {9[T]}, {}] Accelerate Start location: l6 Program variables: __const_50^0 i5^0 i^0 tmp^0 9: l0 -> l1 : i^0'=0, __const_50^0-i5^0 <= 0, cost: 1 10: l0 -> l2 : i5^0'=1+i5^0, 1-__const_50^0+i5^0 <= 0, cost: 1 12: l1 -> l3 : T, cost: 1 11: l2 -> l0 : T, cost: 1 16: l2 -> l2 : i5^0'=n+i5^0, (-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0), cost: 1 13: l3 -> l4 : __const_50^0-i^0 <= 0, cost: 1 14: l3 -> l1 : i^0'=1+i^0, 1-__const_50^0+i^0 <= 0, cost: 1 15: l6 -> l2 : i5^0'=0, i^0'=0, tmp^0'=tmp^post7, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : i5^0'=1+i5^0, 1-__const_50^0+i5^0 <= 0, cost: 1 New rule: l2 -> l2 : i5^0'=n+i5^0, (-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0), cost: 1 -1+__const_50^0-i5^0 >= 0 [0]: montonic decrease yields -n+__const_50^0-i5^0 >= 0 -1+__const_50^0-i5^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+__const_50^0-i5^0 >= 0) Replacement map: {-1+__const_50^0-i5^0 >= 0 -> -n+__const_50^0-i5^0 >= 0} Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)] Blocked [{}, {}, {16[T]}] Step with 11 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T] Blocked [{}, {}, {16[T]}, {}] Step with 10 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 10[(1-__const_50^0+i5^0 <= 0)] Blocked [{}, {}, {16[T]}, {}, {}] Covered Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T] Blocked [{}, {}, {16[T]}, {10[T]}] Step with 9 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}] Step with 12 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {}] Step with 14 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T], 14[(1-__const_50^0+i^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {13[T]}, {}] Accelerate Start location: l6 Program variables: __const_50^0 i5^0 i^0 tmp^0 9: l0 -> l1 : i^0'=0, __const_50^0-i5^0 <= 0, cost: 1 10: l0 -> l2 : i5^0'=1+i5^0, 1-__const_50^0+i5^0 <= 0, cost: 1 12: l1 -> l3 : T, cost: 1 17: l1 -> l1 : i^0'=i^0+n2, (__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 11: l2 -> l0 : T, cost: 1 16: l2 -> l2 : i5^0'=n+i5^0, (-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0), cost: 1 13: l3 -> l4 : __const_50^0-i^0 <= 0, cost: 1 14: l3 -> l1 : i^0'=1+i^0, 1-__const_50^0+i^0 <= 0, cost: 1 15: l6 -> l2 : i5^0'=0, i^0'=0, tmp^0'=tmp^post7, T, cost: 1 Loop Acceleration Original rule: l1 -> l1 : i^0'=1+i^0, 1-__const_50^0+i^0 <= 0, cost: 1 New rule: l1 -> l1 : i^0'=i^0+n2, (__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 -1+__const_50^0-i^0 >= 0 [0]: montonic decrease yields __const_50^0-i^0-n2 >= 0 -1+__const_50^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+__const_50^0-i^0 >= 0) Replacement map: {-1+__const_50^0-i^0 >= 0 -> __const_50^0-i^0-n2 >= 0} Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 17[(__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}] Step with 12 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 17[(__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0)], 12[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {}] Step with 14 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 17[(__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0)], 12[T], 14[(1-__const_50^0+i^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {}, {}] Covered Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 17[(__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0)], 12[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {14[T]}] Step with 13 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 17[(__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0)], 12[T], 13[(__const_50^0-i^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {14[T]}, {}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 17[(__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0)], 12[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {13[T], 14[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 17[(__const_50^0-i^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {12[T], 17[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}] Step with 12 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {}] Step with 14 Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T], 14[(1-__const_50^0+i^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {13[T]}, {}] Covered Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {13[T], 14[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T], 9[(__const_50^0-i5^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {12[T], 17[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)], 11[T] Blocked [{}, {}, {16[T]}, {9[T], 10[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ -n+__const_50^0-i5^0 >= 0)] Blocked [{}, {}, {11[T], 16[T]}] Backtrack Trace 15[T] Blocked [{}, {16[T]}] Step with 11 Trace 15[T], 11[T] Blocked [{}, {16[T]}, {}] Step with 9 Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)] Blocked [{}, {16[T]}, {}, {}] Step with 12 Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T] Blocked [{}, {16[T]}, {}, {}, {}] Step with 13 Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T], 13[(__const_50^0-i^0 <= 0)] Blocked [{}, {16[T]}, {}, {}, {14[T]}, {}] Backtrack Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)], 12[T] Blocked [{}, {16[T]}, {}, {}, {13[T], 14[T]}] Backtrack Trace 15[T], 11[T], 9[(__const_50^0-i5^0 <= 0)] Blocked [{}, {16[T]}, {}, {12[T]}] Backtrack Trace 15[T], 11[T] Blocked [{}, {16[T]}, {9[T]}] Step with 10 Trace 15[T], 11[T], 10[(1-__const_50^0+i5^0 <= 0)] Blocked [{}, {16[T]}, {9[T]}, {}] Covered Trace 15[T], 11[T] Blocked [{}, {16[T]}, {9[T], 10[T]}] Backtrack Trace 15[T] Blocked [{}, {11[T], 16[T]}] Backtrack Trace Blocked [{15[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b