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