NO Initial ITS Start location: l7 Program variables: __const_10^0 __const_5^0 i^0 j^0 0: l0 -> l1 : __const_10^0'=__const_10^post1, __const_5^0'=__const_5^post1, i^0'=i^post1, j^0'=j^post1, (j^post1-i^0 == 0 /\ -i^post1+i^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0), cost: 1 1: l1 -> l2 : __const_10^0'=__const_10^post2, __const_5^0'=__const_5^post2, i^0'=i^post2, j^0'=j^post2, (-j^post2+j^0 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -1+i^post2-i^0 == 0), cost: 1 7: l2 -> l4 : __const_10^0'=__const_10^post8, __const_5^0'=__const_5^post8, i^0'=i^post8, j^0'=j^post8, (-i^post8+i^0 == 0 /\ -__const_5^post8+__const_5^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0), cost: 1 2: l3 -> l0 : __const_10^0'=__const_10^post3, __const_5^0'=__const_5^post3, i^0'=i^post3, j^0'=j^post3, (1+__const_5^0-i^0 <= 0 /\ -i^post3+i^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -__const_5^post3+__const_5^0 == 0 /\ j^0-j^post3 == 0), cost: 1 3: l3 -> l0 : __const_10^0'=__const_10^post4, __const_5^0'=__const_5^post4, i^0'=i^post4, j^0'=j^post4, (-j^post4+j^0 == 0 /\ -i^post4+i^0 == 0 /\ 1-__const_5^0+i^0 <= 0 /\ -__const_10^post4+__const_10^0 == 0 /\ -__const_5^post4+__const_5^0 == 0), cost: 1 4: l3 -> l1 : __const_10^0'=__const_10^post5, __const_5^0'=__const_5^post5, i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -j^post5+j^0 == 0 /\ __const_5^0-i^0 <= 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_5^0+i^0 <= 0 /\ -__const_5^post5+__const_5^0 == 0), cost: 1 5: l4 -> l5 : __const_10^0'=__const_10^post6, __const_5^0'=__const_5^post6, i^0'=i^post6, j^0'=j^post6, (__const_10^0-__const_10^post6 == 0 /\ __const_5^0-__const_5^post6 == 0 /\ -j^post6+j^0 == 0 /\ __const_10^0-i^0 <= 0 /\ -i^post6+i^0 == 0), cost: 1 6: l4 -> l3 : __const_10^0'=__const_10^post7, __const_5^0'=__const_5^post7, i^0'=i^post7, j^0'=j^post7, (-i^post7+i^0 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ -j^post7+j^0 == 0 /\ 1-__const_10^0+i^0 <= 0 /\ __const_10^0-__const_10^post7 == 0), cost: 1 8: l6 -> l2 : __const_10^0'=__const_10^post9, __const_5^0'=__const_5^post9, i^0'=i^post9, j^0'=j^post9, (-__const_5^post9+__const_5^0 == 0 /\ -j^post9+j^0 == 0 /\ __const_10^0-__const_10^post9 == 0 /\ i^post9 == 0), cost: 1 9: l7 -> l6 : __const_10^0'=__const_10^post10, __const_5^0'=__const_5^post10, i^0'=i^post10, j^0'=j^post10, (__const_10^0-__const_10^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -i^post10+i^0 == 0 /\ -j^post10+j^0 == 0), cost: 1 Chained Linear Paths Start location: l7 Program variables: __const_10^0 __const_5^0 i^0 j^0 0: l0 -> l1 : __const_10^0'=__const_10^post1, __const_5^0'=__const_5^post1, i^0'=i^post1, j^0'=j^post1, (j^post1-i^0 == 0 /\ -i^post1+i^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0), cost: 1 1: l1 -> l2 : __const_10^0'=__const_10^post2, __const_5^0'=__const_5^post2, i^0'=i^post2, j^0'=j^post2, (-j^post2+j^0 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -1+i^post2-i^0 == 0), cost: 1 7: l2 -> l4 : __const_10^0'=__const_10^post8, __const_5^0'=__const_5^post8, i^0'=i^post8, j^0'=j^post8, (-i^post8+i^0 == 0 /\ -__const_5^post8+__const_5^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0), cost: 1 2: l3 -> l0 : __const_10^0'=__const_10^post3, __const_5^0'=__const_5^post3, i^0'=i^post3, j^0'=j^post3, (1+__const_5^0-i^0 <= 0 /\ -i^post3+i^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -__const_5^post3+__const_5^0 == 0 /\ j^0-j^post3 == 0), cost: 1 3: l3 -> l0 : __const_10^0'=__const_10^post4, __const_5^0'=__const_5^post4, i^0'=i^post4, j^0'=j^post4, (-j^post4+j^0 == 0 /\ -i^post4+i^0 == 0 /\ 1-__const_5^0+i^0 <= 0 /\ -__const_10^post4+__const_10^0 == 0 /\ -__const_5^post4+__const_5^0 == 0), cost: 1 4: l3 -> l1 : __const_10^0'=__const_10^post5, __const_5^0'=__const_5^post5, i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -j^post5+j^0 == 0 /\ __const_5^0-i^0 <= 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_5^0+i^0 <= 0 /\ -__const_5^post5+__const_5^0 == 0), cost: 1 5: l4 -> l5 : __const_10^0'=__const_10^post6, __const_5^0'=__const_5^post6, i^0'=i^post6, j^0'=j^post6, (__const_10^0-__const_10^post6 == 0 /\ __const_5^0-__const_5^post6 == 0 /\ -j^post6+j^0 == 0 /\ __const_10^0-i^0 <= 0 /\ -i^post6+i^0 == 0), cost: 1 6: l4 -> l3 : __const_10^0'=__const_10^post7, __const_5^0'=__const_5^post7, i^0'=i^post7, j^0'=j^post7, (-i^post7+i^0 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ -j^post7+j^0 == 0 /\ 1-__const_10^0+i^0 <= 0 /\ __const_10^0-__const_10^post7 == 0), cost: 1 10: l7 -> l2 : __const_10^0'=__const_10^post9, __const_5^0'=__const_5^post9, i^0'=i^post9, j^0'=j^post9, (-j^post9+j^post10 == 0 /\ -__const_10^post9+__const_10^post10 == 0 /\ __const_10^0-__const_10^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -__const_5^post9+__const_5^post10 == 0 /\ -i^post10+i^0 == 0 /\ i^post9 == 0 /\ -j^post10+j^0 == 0), cost: 1 Eliminating location l6 by chaining: Applied chaining First rule: l7 -> l6 : __const_10^0'=__const_10^post10, __const_5^0'=__const_5^post10, i^0'=i^post10, j^0'=j^post10, (__const_10^0-__const_10^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -i^post10+i^0 == 0 /\ -j^post10+j^0 == 0), cost: 1 Second rule: l6 -> l2 : __const_10^0'=__const_10^post9, __const_5^0'=__const_5^post9, i^0'=i^post9, j^0'=j^post9, (-__const_5^post9+__const_5^0 == 0 /\ -j^post9+j^0 == 0 /\ __const_10^0-__const_10^post9 == 0 /\ i^post9 == 0), cost: 1 New rule: l7 -> l2 : __const_10^0'=__const_10^post9, __const_5^0'=__const_5^post9, i^0'=i^post9, j^0'=j^post9, (-j^post9+j^post10 == 0 /\ -__const_10^post9+__const_10^post10 == 0 /\ __const_10^0-__const_10^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -__const_5^post9+__const_5^post10 == 0 /\ -i^post10+i^0 == 0 /\ i^post9 == 0 /\ -j^post10+j^0 == 0), cost: 1 Applied deletion Removed the following rules: 8 9 Simplified Transitions Start location: l7 Program variables: __const_10^0 __const_5^0 i^0 j^0 11: l0 -> l1 : j^0'=i^0, T, cost: 1 12: l1 -> l2 : i^0'=1+i^0, T, cost: 1 18: l2 -> l4 : T, cost: 1 13: l3 -> l0 : 1+__const_5^0-i^0 <= 0, cost: 1 14: l3 -> l0 : 1-__const_5^0+i^0 <= 0, cost: 1 15: l3 -> l1 : i^0'=i^post5, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 16: l4 -> l5 : __const_10^0-i^0 <= 0, cost: 1 17: l4 -> l3 : 1-__const_10^0+i^0 <= 0, cost: 1 19: l7 -> l2 : i^0'=0, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __const_10^0'=__const_10^post1, __const_5^0'=__const_5^post1, i^0'=i^post1, j^0'=j^post1, (j^post1-i^0 == 0 /\ -i^post1+i^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0), cost: 1 New rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=i^0, 0 == 0, cost: 1 propagated equality j^post1 = i^0 propagated equality i^post1 = i^0 propagated equality __const_10^post1 = __const_10^0 propagated equality __const_5^post1 = __const_5^0 Simplified Guard Original rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=i^0, 0 == 0, cost: 1 New rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=i^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=i^0, T, cost: 1 New rule: l0 -> l1 : j^0'=i^0, T, cost: 1 Propagated Equalities Original rule: l1 -> l2 : __const_10^0'=__const_10^post2, __const_5^0'=__const_5^post2, i^0'=i^post2, j^0'=j^post2, (-j^post2+j^0 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -1+i^post2-i^0 == 0), cost: 1 New rule: l1 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=1+i^0, j^0'=j^0, 0 == 0, cost: 1 propagated equality j^post2 = j^0 propagated equality __const_5^post2 = __const_5^0 propagated equality __const_10^post2 = __const_10^0 propagated equality i^post2 = 1+i^0 Simplified Guard Original rule: l1 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=1+i^0, j^0'=j^0, 0 == 0, cost: 1 New rule: l1 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=1+i^0, j^0'=j^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=1+i^0, j^0'=j^0, T, cost: 1 New rule: l1 -> l2 : i^0'=1+i^0, T, cost: 1 Propagated Equalities Original rule: l3 -> l0 : __const_10^0'=__const_10^post3, __const_5^0'=__const_5^post3, i^0'=i^post3, j^0'=j^post3, (1+__const_5^0-i^0 <= 0 /\ -i^post3+i^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -__const_5^post3+__const_5^0 == 0 /\ j^0-j^post3 == 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ 1+__const_5^0-i^0 <= 0), cost: 1 propagated equality i^post3 = i^0 propagated equality __const_10^post3 = __const_10^0 propagated equality __const_5^post3 = __const_5^0 propagated equality j^post3 = j^0 Simplified Guard Original rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ 1+__const_5^0-i^0 <= 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 1+__const_5^0-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 1+__const_5^0-i^0 <= 0, cost: 1 New rule: l3 -> l0 : 1+__const_5^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : __const_10^0'=__const_10^post4, __const_5^0'=__const_5^post4, i^0'=i^post4, j^0'=j^post4, (-j^post4+j^0 == 0 /\ -i^post4+i^0 == 0 /\ 1-__const_5^0+i^0 <= 0 /\ -__const_10^post4+__const_10^0 == 0 /\ -__const_5^post4+__const_5^0 == 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ 1-__const_5^0+i^0 <= 0), cost: 1 propagated equality j^post4 = j^0 propagated equality i^post4 = i^0 propagated equality __const_10^post4 = __const_10^0 propagated equality __const_5^post4 = __const_5^0 Simplified Guard Original rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ 1-__const_5^0+i^0 <= 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 1-__const_5^0+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 1-__const_5^0+i^0 <= 0, cost: 1 New rule: l3 -> l0 : 1-__const_5^0+i^0 <= 0, cost: 1 made implied equalities explicit Original rule: l3 -> l1 : __const_10^0'=__const_10^post5, __const_5^0'=__const_5^post5, i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -j^post5+j^0 == 0 /\ __const_5^0-i^0 <= 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_5^0+i^0 <= 0 /\ -__const_5^post5+__const_5^0 == 0), cost: 1 New rule: l3 -> l1 : __const_10^0'=__const_10^post5, __const_5^0'=__const_5^post5, i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -j^post5+j^0 == 0 /\ __const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_5^0+i^0 <= 0 /\ -__const_5^post5+__const_5^0 == 0), cost: 1 Propagated Equalities Original rule: l3 -> l1 : __const_10^0'=__const_10^post5, __const_5^0'=__const_5^post5, i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -j^post5+j^0 == 0 /\ __const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_5^0+i^0 <= 0 /\ -__const_5^post5+__const_5^0 == 0), cost: 1 New rule: l3 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^post5, j^0'=j^0, (0 == 0 /\ __const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 propagated equality j^post5 = j^0 propagated equality __const_10^post5 = __const_10^0 propagated equality __const_5^post5 = __const_5^0 Simplified Guard Original rule: l3 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^post5, j^0'=j^0, (0 == 0 /\ __const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 New rule: l3 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^post5, j^0'=j^0, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 made implied equalities explicit Original rule: l3 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^post5, j^0'=j^0, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 New rule: l3 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^post5, j^0'=j^0, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^post5, j^0'=j^0, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 New rule: l3 -> l1 : i^0'=i^post5, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l5 : __const_10^0'=__const_10^post6, __const_5^0'=__const_5^post6, i^0'=i^post6, j^0'=j^post6, (__const_10^0-__const_10^post6 == 0 /\ __const_5^0-__const_5^post6 == 0 /\ -j^post6+j^0 == 0 /\ __const_10^0-i^0 <= 0 /\ -i^post6+i^0 == 0), cost: 1 New rule: l4 -> l5 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ __const_10^0-i^0 <= 0), cost: 1 propagated equality __const_10^post6 = __const_10^0 propagated equality __const_5^post6 = __const_5^0 propagated equality j^post6 = j^0 propagated equality i^post6 = i^0 Simplified Guard Original rule: l4 -> l5 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ __const_10^0-i^0 <= 0), cost: 1 New rule: l4 -> l5 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, __const_10^0-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l5 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, __const_10^0-i^0 <= 0, cost: 1 New rule: l4 -> l5 : __const_10^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l3 : __const_10^0'=__const_10^post7, __const_5^0'=__const_5^post7, i^0'=i^post7, j^0'=j^post7, (-i^post7+i^0 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ -j^post7+j^0 == 0 /\ 1-__const_10^0+i^0 <= 0 /\ __const_10^0-__const_10^post7 == 0), cost: 1 New rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ 1-__const_10^0+i^0 <= 0), cost: 1 propagated equality i^post7 = i^0 propagated equality __const_5^post7 = __const_5^0 propagated equality j^post7 = j^0 propagated equality __const_10^post7 = __const_10^0 Simplified Guard Original rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, (0 == 0 /\ 1-__const_10^0+i^0 <= 0), cost: 1 New rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 1-__const_10^0+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 1-__const_10^0+i^0 <= 0, cost: 1 New rule: l4 -> l3 : 1-__const_10^0+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l4 : __const_10^0'=__const_10^post8, __const_5^0'=__const_5^post8, i^0'=i^post8, j^0'=j^post8, (-i^post8+i^0 == 0 /\ -__const_5^post8+__const_5^0 == 0 /\ -j^post8+j^0 == 0 /\ -__const_10^post8+__const_10^0 == 0), cost: 1 New rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 0 == 0, cost: 1 propagated equality i^post8 = i^0 propagated equality __const_5^post8 = __const_5^0 propagated equality j^post8 = j^0 propagated equality __const_10^post8 = __const_10^0 Simplified Guard Original rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, 0 == 0, cost: 1 New rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=i^0, j^0'=j^0, T, cost: 1 New rule: l2 -> l4 : T, cost: 1 Propagated Equalities Original rule: l7 -> l2 : __const_10^0'=__const_10^post9, __const_5^0'=__const_5^post9, i^0'=i^post9, j^0'=j^post9, (-j^post9+j^post10 == 0 /\ -__const_10^post9+__const_10^post10 == 0 /\ __const_10^0-__const_10^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -__const_5^post9+__const_5^post10 == 0 /\ -i^post10+i^0 == 0 /\ i^post9 == 0 /\ -j^post10+j^0 == 0), cost: 1 New rule: l7 -> l2 : __const_10^0'=__const_10^post10, __const_5^0'=__const_5^post10, i^0'=0, j^0'=j^post10, (0 == 0 /\ __const_10^0-__const_10^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -i^post10+i^0 == 0 /\ -j^post10+j^0 == 0), cost: 1 propagated equality j^post9 = j^post10 propagated equality __const_10^post9 = __const_10^post10 propagated equality __const_5^post9 = __const_5^post10 propagated equality i^post9 = 0 Propagated Equalities Original rule: l7 -> l2 : __const_10^0'=__const_10^post10, __const_5^0'=__const_5^post10, i^0'=0, j^0'=j^post10, (0 == 0 /\ __const_10^0-__const_10^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -i^post10+i^0 == 0 /\ -j^post10+j^0 == 0), cost: 1 New rule: l7 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=0, j^0'=j^0, 0 == 0, cost: 1 propagated equality __const_10^post10 = __const_10^0 propagated equality __const_5^post10 = __const_5^0 propagated equality i^post10 = i^0 propagated equality j^post10 = j^0 Simplified Guard Original rule: l7 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=0, j^0'=j^0, 0 == 0, cost: 1 New rule: l7 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=0, j^0'=j^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l2 : __const_10^0'=__const_10^0, __const_5^0'=__const_5^0, i^0'=0, j^0'=j^0, T, cost: 1 New rule: l7 -> l2 : i^0'=0, T, cost: 1 Step with 19 Trace 19[T] Blocked [{}, {}] Step with 18 Trace 19[T], 18[T] Blocked [{}, {}, {}] Step with 16 Trace 19[T], 18[T], 16[(__const_10^0-i^0 <= 0)] Blocked [{}, {}, {}, {}] Backtrack Trace 19[T], 18[T] Blocked [{}, {}, {16[T]}] Step with 17 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)] Blocked [{}, {}, {16[T]}, {}] Step with 13 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)] Blocked [{}, {}, {16[T]}, {}, {}] Step with 11 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T] Blocked [{}, {}, {16[T]}, {}, {}, {}] Step with 12 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T], 12[T] Blocked [{}, {}, {16[T]}, {}, {}, {}, {}] Accelerate Start location: l7 Program variables: __const_10^0 __const_5^0 i^0 j^0 11: l0 -> l1 : j^0'=i^0, T, cost: 1 12: l1 -> l2 : i^0'=1+i^0, T, cost: 1 18: l2 -> l4 : T, cost: 1 20: l2 -> l2 : i^0'=n+i^0, j^0'=-1+n+i^0, (__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0), cost: 1 13: l3 -> l0 : 1+__const_5^0-i^0 <= 0, cost: 1 14: l3 -> l0 : 1-__const_5^0+i^0 <= 0, cost: 1 15: l3 -> l1 : i^0'=i^post5, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 16: l4 -> l5 : __const_10^0-i^0 <= 0, cost: 1 17: l4 -> l3 : 1-__const_10^0+i^0 <= 0, cost: 1 19: l7 -> l2 : i^0'=0, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : i^0'=1+i^0, j^0'=i^0, (1+__const_5^0-i^0 <= 0 /\ 1-__const_10^0+i^0 <= 0), cost: 1 New rule: l2 -> l2 : i^0'=n+i^0, j^0'=-1+n+i^0, (__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0), cost: 1 -1+__const_10^0-i^0 >= 0 [0]: montonic decrease yields __const_10^0-n-i^0 >= 0 -1+__const_10^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+__const_10^0-i^0 >= 0) -1-__const_5^0+i^0 >= 0 [0]: monotonic increase yields -1-__const_5^0+i^0 >= 0 Replacement map: {-1+__const_10^0-i^0 >= 0 -> __const_10^0-n-i^0 >= 0, -1-__const_5^0+i^0 >= 0 -> -1-__const_5^0+i^0 >= 0} Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {20[T]}] Step with 18 Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T] Blocked [{}, {}, {20[T]}, {}] Step with 17 Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {}] Step with 13 Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {}, {}] Step with 11 Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T] Blocked [{}, {}, {20[T]}, {}, {}, {}, {}] Step with 12 Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T], 12[T] Blocked [{}, {}, {20[T]}, {}, {}, {}, {}, {}] Covered Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T] Blocked [{}, {}, {20[T]}, {}, {}, {}, {12[T]}] Backtrack Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {}, {11[T]}] Backtrack Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {13[T]}] Backtrack Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T] Blocked [{}, {}, {20[T]}, {17[T]}] Step with 16 Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T], 16[(__const_10^0-i^0 <= 0)] Blocked [{}, {}, {20[T]}, {17[T]}, {}] Backtrack Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)], 18[T] Blocked [{}, {}, {20[T]}, {16[T], 17[T]}] Backtrack Trace 19[T], 20[(__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {18[T], 20[T]}] Backtrack Trace 19[T] Blocked [{}, {20[T]}] Step with 18 Trace 19[T], 18[T] Blocked [{}, {20[T]}, {}] Step with 16 Trace 19[T], 18[T], 16[(__const_10^0-i^0 <= 0)] Blocked [{}, {20[T]}, {}, {}] Backtrack Trace 19[T], 18[T] Blocked [{}, {20[T]}, {16[T]}] Step with 17 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)] Blocked [{}, {20[T]}, {16[T]}, {}] Step with 13 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)] Blocked [{}, {20[T]}, {16[T]}, {}, {}] Step with 11 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T] Blocked [{}, {20[T]}, {16[T]}, {}, {}, {}] Step with 12 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T], 12[T] Blocked [{}, {20[T]}, {16[T]}, {}, {}, {}, {}] Covered Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)], 11[T] Blocked [{}, {20[T]}, {16[T]}, {}, {}, {12[T]}] Backtrack Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 13[(1+__const_5^0-i^0 <= 0)] Blocked [{}, {20[T]}, {16[T]}, {}, {11[T]}] Backtrack Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)] Blocked [{}, {20[T]}, {16[T]}, {13[T]}] Step with 14 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)] Blocked [{}, {20[T]}, {16[T]}, {13[T]}, {}] Step with 11 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)], 11[T] Blocked [{}, {20[T]}, {16[T]}, {13[T]}, {}, {}] Step with 12 Trace 19[T], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)], 11[T], 12[T] Blocked [{}, {20[T]}, {16[T]}, {13[T]}, {}, {}, {}] Accelerate Start location: l7 Program variables: __const_10^0 __const_5^0 i^0 j^0 11: l0 -> l1 : j^0'=i^0, T, cost: 1 12: l1 -> l2 : i^0'=1+i^0, T, cost: 1 18: l2 -> l4 : T, cost: 1 20: l2 -> l2 : i^0'=n+i^0, j^0'=-1+n+i^0, (__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0), cost: 1 21: l2 -> l2 : i^0'=n2+i^0, j^0'=-1+n2+i^0, (-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0), cost: 1 13: l3 -> l0 : 1+__const_5^0-i^0 <= 0, cost: 1 14: l3 -> l0 : 1-__const_5^0+i^0 <= 0, cost: 1 15: l3 -> l1 : i^0'=i^post5, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 16: l4 -> l5 : __const_10^0-i^0 <= 0, cost: 1 17: l4 -> l3 : 1-__const_10^0+i^0 <= 0, cost: 1 19: l7 -> l2 : i^0'=0, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : i^0'=1+i^0, j^0'=i^0, (1-__const_5^0+i^0 <= 0 /\ 1-__const_10^0+i^0 <= 0), cost: 1 New rule: l2 -> l2 : i^0'=n2+i^0, j^0'=-1+n2+i^0, (-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0), cost: 1 -1+__const_10^0-i^0 >= 0 [0]: montonic decrease yields __const_10^0-n2-i^0 >= 0 -1+__const_10^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+__const_10^0-i^0 >= 0) -1+__const_5^0-i^0 >= 0 [0]: montonic decrease yields -n2+__const_5^0-i^0 >= 0 -1+__const_5^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+__const_5^0-i^0 >= 0) Replacement map: {-1+__const_10^0-i^0 >= 0 -> __const_10^0-n2-i^0 >= 0, -1+__const_5^0-i^0 >= 0 -> -n2+__const_5^0-i^0 >= 0} Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)] Blocked [{}, {20[T]}, {21[T]}] Step with 18 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T] Blocked [{}, {20[T]}, {21[T]}, {}] Step with 17 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)] Blocked [{}, {20[T]}, {21[T]}, {}, {}] Step with 14 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)] Blocked [{}, {20[T]}, {21[T]}, {}, {}, {}] Step with 11 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)], 11[T] Blocked [{}, {20[T]}, {21[T]}, {}, {}, {}, {}] Step with 12 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)], 11[T], 12[T] Blocked [{}, {20[T]}, {21[T]}, {}, {}, {}, {}, {}] Covered Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)], 11[T] Blocked [{}, {20[T]}, {21[T]}, {}, {}, {}, {12[T]}] Backtrack Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 14[(1-__const_5^0+i^0 <= 0)] Blocked [{}, {20[T]}, {21[T]}, {}, {}, {11[T]}] Backtrack Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)] Blocked [{}, {20[T]}, {21[T]}, {}, {14[T]}] Step with 15 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 15[(__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0)] Blocked [{}, {20[T]}, {21[T]}, {}, {14[T]}, {}] Step with 12 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 18[T], 17[(1-__const_10^0+i^0 <= 0)], 15[(__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0)], 12[T] Blocked [{}, {20[T]}, {21[T]}, {}, {14[T]}, {}, {}] Nonterm Start location: l7 Program variables: __const_10^0 __const_5^0 i^0 j^0 11: l0 -> l1 : j^0'=i^0, T, cost: 1 12: l1 -> l2 : i^0'=1+i^0, T, cost: 1 18: l2 -> l4 : T, cost: 1 20: l2 -> l2 : i^0'=n+i^0, j^0'=-1+n+i^0, (__const_10^0-n-i^0 >= 0 /\ -1-__const_5^0+i^0 >= 0 /\ -1+n >= 0), cost: 1 21: l2 -> l2 : i^0'=n2+i^0, j^0'=-1+n2+i^0, (-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0), cost: 1 22: l2 -> LoAT_sink : (1+i^post51-i^0 <= 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -1-i^post51+i^0 <= 0), cost: NONTERM 23: l2 -> l2 : i^0'=__const_5^0, (__const_5^0-i^0 >= 0 /\ -1+__const_10^0-__const_5^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0), cost: 1 13: l3 -> l0 : 1+__const_5^0-i^0 <= 0, cost: 1 14: l3 -> l0 : 1-__const_5^0+i^0 <= 0, cost: 1 15: l3 -> l1 : i^0'=i^post5, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0), cost: 1 16: l4 -> l5 : __const_10^0-i^0 <= 0, cost: 1 17: l4 -> l3 : 1-__const_10^0+i^0 <= 0, cost: 1 19: l7 -> l2 : i^0'=0, T, cost: 1 Certificate of Non-Termination Original rule: l2 -> l2 : i^0'=1+i^post51, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0 /\ 1-__const_10^0+i^0 <= 0), cost: 1 New rule: l2 -> LoAT_sink : (1+i^post51-i^0 <= 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -1-i^post51+i^0 <= 0), cost: NONTERM __const_5^0-i^0 >= 0 [0]: eventual decrease yields (__const_5^0-i^0 >= 0 /\ -1-i^post51+__const_5^0 >= 0) __const_5^0-i^0 >= 0 [1]: eventual increase yields (1+i^post51-i^0 <= 0 /\ __const_5^0-i^0 >= 0) -1+__const_10^0-i^0 >= 0 [0]: eventual decrease yields (-1+__const_10^0-i^0 >= 0 /\ -2+__const_10^0-i^post51 >= 0) -1+__const_10^0-i^0 >= 0 [1]: eventual increase yields (1+i^post51-i^0 <= 0 /\ -1+__const_10^0-i^0 >= 0) -__const_5^0+i^0 >= 0 [0]: eventual decrease yields (1+i^post51-__const_5^0 >= 0 /\ -__const_5^0+i^0 >= 0) -__const_5^0+i^0 >= 0 [1]: eventual increase yields (-__const_5^0+i^0 >= 0 /\ -1-i^post51+i^0 <= 0) Replacement map: {__const_5^0-i^0 >= 0 -> (1+i^post51-i^0 <= 0 /\ __const_5^0-i^0 >= 0), -1+__const_10^0-i^0 >= 0 -> (1+i^post51-i^0 <= 0 /\ -1+__const_10^0-i^0 >= 0), -__const_5^0+i^0 >= 0 -> (-__const_5^0+i^0 >= 0 /\ -1-i^post51+i^0 <= 0)} Loop Acceleration Original rule: l2 -> l2 : i^0'=1+i^post51, (__const_5^0-i^0 <= 0 /\ __const_5^0-i^0 == 0 /\ -__const_5^0+i^0 <= 0 /\ 1-__const_10^0+i^0 <= 0), cost: 1 New rule: l2 -> l2 : i^0'=1+i^post51, (1+i^post51-__const_5^0 >= 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -1-i^post51+__const_5^0 >= 0 /\ -2+__const_10^0-i^post51 >= 0 /\ -1+n3 >= 0), cost: 1 __const_5^0-i^0 >= 0 [0]: eventual decrease yields (__const_5^0-i^0 >= 0 /\ -1-i^post51+__const_5^0 >= 0) __const_5^0-i^0 >= 0 [1]: eventual increase yields (1+i^post51-i^0 <= 0 /\ __const_5^0-i^0 >= 0) -1+__const_10^0-i^0 >= 0 [0]: eventual decrease yields (-1+__const_10^0-i^0 >= 0 /\ -2+__const_10^0-i^post51 >= 0) -1+__const_10^0-i^0 >= 0 [1]: eventual increase yields (1+i^post51-i^0 <= 0 /\ -1+__const_10^0-i^0 >= 0) -__const_5^0+i^0 >= 0 [0]: eventual decrease yields (1+i^post51-__const_5^0 >= 0 /\ -__const_5^0+i^0 >= 0) -__const_5^0+i^0 >= 0 [1]: eventual increase yields (-__const_5^0+i^0 >= 0 /\ -1-i^post51+i^0 <= 0) Replacement map: {__const_5^0-i^0 >= 0 -> (__const_5^0-i^0 >= 0 /\ -1-i^post51+__const_5^0 >= 0), -1+__const_10^0-i^0 >= 0 -> (-1+__const_10^0-i^0 >= 0 /\ -2+__const_10^0-i^post51 >= 0), -__const_5^0+i^0 >= 0 -> (1+i^post51-__const_5^0 >= 0 /\ -__const_5^0+i^0 >= 0)} made implied equalities explicit Original rule: l2 -> l2 : i^0'=1+i^post51, (1+i^post51-__const_5^0 >= 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -1-i^post51+__const_5^0 >= 0 /\ -2+__const_10^0-i^post51 >= 0 /\ -1+n3 >= 0), cost: 1 New rule: l2 -> l2 : i^0'=1+i^post51, (1+i^post51-__const_5^0 >= 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0 /\ -1-i^post51+__const_5^0 >= 0 /\ -1-i^post51+__const_5^0 == 0 /\ -2+__const_10^0-i^post51 >= 0 /\ -1+n3 >= 0), cost: 1 Propagated Equalities Original rule: l2 -> l2 : i^0'=1+i^post51, (1+i^post51-__const_5^0 >= 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0 /\ -1-i^post51+__const_5^0 >= 0 /\ -1-i^post51+__const_5^0 == 0 /\ -2+__const_10^0-i^post51 >= 0 /\ -1+n3 >= 0), cost: 1 New rule: l2 -> l2 : i^0'=__const_5^0, (0 >= 0 /\ 0 == 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-__const_5^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0 /\ -1+n3 >= 0), cost: 1 propagated equality i^post51 = -1+__const_5^0 Simplified Guard Original rule: l2 -> l2 : i^0'=__const_5^0, (0 >= 0 /\ 0 == 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-__const_5^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0 /\ -1+n3 >= 0), cost: 1 New rule: l2 -> l2 : i^0'=__const_5^0, (__const_5^0-i^0 >= 0 /\ -1+__const_10^0-__const_5^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0 /\ -1+n3 >= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l2 -> l2 : i^0'=__const_5^0, (__const_5^0-i^0 >= 0 /\ -1+__const_10^0-__const_5^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0 /\ -1+n3 >= 0), cost: 1 New rule: l2 -> l2 : i^0'=__const_5^0, (__const_5^0-i^0 >= 0 /\ -1+__const_10^0-__const_5^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -__const_5^0+i^0 == 0), cost: 1 Step with 22 Trace 19[T], 21[(-n2+__const_5^0-i^0 >= 0 /\ -1+n2 >= 0 /\ __const_10^0-n2-i^0 >= 0)], 22[(1+i^post51-i^0 <= 0 /\ __const_5^0-i^0 >= 0 /\ -1+__const_10^0-i^0 >= 0 /\ -__const_5^0+i^0 >= 0 /\ -1-i^post51+i^0 <= 0)] Blocked [{}, {20[T]}, {21[T]}, {22[T]}] Refute Counterexample [ __const_10^0=2 __const_5^0=1 i^0=0 j^0=0 ] 19 [ __const_10^0=2 __const_5^0=1 i^0=1 j^0=0 ] 21 [ __const_10^0=2 __const_5^0=1 i^0=i^0 j^0=0 ] 22 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b