unknown Initial ITS Start location: l10 Program variables: __const_100^0 i^0 j^0 k^0 tmp^0 tmp___0^0 0: l0 -> l1 : __const_100^0'=__const_100^post1, i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (0 == 0 /\ i^post1 == 0 /\ k^0-__const_100^0 <= 0 /\ -tmp^post1+tmp^0 == 0 /\ j^0-j^post1 == 0 /\ k^0-k^post1 == 0 /\ -__const_100^post1+__const_100^0 == 0), cost: 1 1: l0 -> l2 : __const_100^0'=__const_100^post2, i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-k^post2+k^0 == 0 /\ j^0-j^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ -__const_100^post2+__const_100^0 == 0 /\ 1-k^0+__const_100^0 <= 0 /\ i^0-i^post2 == 0), cost: 1 4: l1 -> l4 : __const_100^0'=__const_100^post5, i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-i^post5+i^0 == 0 /\ -k^post5+k^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ j^0-j^post5 == 0), cost: 1 2: l3 -> l0 : __const_100^0'=__const_100^post3, i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (1-k^0 <= 0 /\ tmp^0-tmp^post3 == 0 /\ -j^post3+j^0 == 0 /\ -k^post3+k^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ i^0-i^post3 == 0 /\ -__const_100^post3+__const_100^0 == 0), cost: 1 3: l3 -> l2 : __const_100^0'=__const_100^post4, i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (j^0-j^post4 == 0 /\ tmp^0-tmp^post4 == 0 /\ -i^post4+i^0 == 0 /\ k^0 <= 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -k^post4+k^0 == 0 /\ -__const_100^post4+__const_100^0 == 0), cost: 1 11: l4 -> l7 : __const_100^0'=__const_100^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-k^0+i^0 <= 0 /\ -k^post12+k^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ j^0-j^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ k^0-i^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ i^0-i^post12 == 0), cost: 1 12: l4 -> l8 : __const_100^0'=__const_100^post13, i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ -__const_100^post13+__const_100^0 == 0 /\ -j^post13+j^0 == 0 /\ 1+k^0-i^0 <= 0 /\ tmp^0-tmp^post13 == 0 /\ -k^post13+k^0 == 0 /\ i^0-i^post13 == 0), cost: 1 13: l4 -> l8 : __const_100^0'=__const_100^post14, i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-i^post14+i^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ j^0-j^post14 == 0 /\ 1-k^0+i^0 <= 0 /\ -__const_100^post14+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ -k^post14+k^0 == 0), cost: 1 5: l5 -> l2 : __const_100^0'=__const_100^post6, i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-__const_100^post6+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ k^0-k^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -j^0+i^0 <= 0 /\ -i^post6+i^0 == 0 /\ j^0-j^post6 == 0), cost: 1 6: l5 -> l6 : __const_100^0'=__const_100^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (1+j^0-i^0 <= 0 /\ -1-j^0+j^post7 == 0 /\ -i^post7+i^0 == 0 /\ -__const_100^post7+__const_100^0 == 0 /\ k^0-k^post7 == 0 /\ tmp^0-tmp^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 8: l6 -> l5 : __const_100^0'=__const_100^post9, i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (k^0-k^post9 == 0 /\ -__const_100^post9+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ j^0-j^post9 == 0 /\ tmp^0-tmp^post9 == 0 /\ -i^post9+i^0 == 0), cost: 1 7: l7 -> l6 : __const_100^0'=__const_100^post8, i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp^post8+tmp^0 == 0 /\ j^post8 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ k^0-k^post8 == 0 /\ 1+i^post8-i^0 == 0 /\ -__const_100^post8+__const_100^0 == 0), cost: 1 9: l8 -> l1 : __const_100^0'=__const_100^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (-tmp^post10+tmp^0 == 0 /\ j^0-j^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -__const_100^post10+__const_100^0 == 0 /\ -1+i^post10-i^0 == 0 /\ k^0-k^post10 == 0), cost: 1 10: l8 -> l7 : __const_100^0'=__const_100^post11, i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-k^post11+k^0 == 0 /\ j^0-j^post11 == 0 /\ -__const_100^post11+__const_100^0 == 0 /\ -tmp^post11+tmp^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ i^0-i^post11 == 0), cost: 1 14: l9 -> l3 : __const_100^0'=__const_100^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ -i^post15+i^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -__const_100^post15+__const_100^0 == 0 /\ j^0-j^post15 == 0 /\ k^post15-tmp^post15 == 0), cost: 1 15: l10 -> l9 : __const_100^0'=__const_100^post16, i^0'=i^post16, j^0'=j^post16, k^0'=k^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (-__const_100^post16+__const_100^0 == 0 /\ k^0-k^post16 == 0 /\ j^0-j^post16 == 0 /\ -i^post16+i^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ tmp___0^0-tmp___0^post16 == 0), cost: 1 Chained Linear Paths Start location: l10 Program variables: __const_100^0 i^0 j^0 k^0 tmp^0 tmp___0^0 0: l0 -> l1 : __const_100^0'=__const_100^post1, i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (0 == 0 /\ i^post1 == 0 /\ k^0-__const_100^0 <= 0 /\ -tmp^post1+tmp^0 == 0 /\ j^0-j^post1 == 0 /\ k^0-k^post1 == 0 /\ -__const_100^post1+__const_100^0 == 0), cost: 1 1: l0 -> l2 : __const_100^0'=__const_100^post2, i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-k^post2+k^0 == 0 /\ j^0-j^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ -__const_100^post2+__const_100^0 == 0 /\ 1-k^0+__const_100^0 <= 0 /\ i^0-i^post2 == 0), cost: 1 4: l1 -> l4 : __const_100^0'=__const_100^post5, i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-i^post5+i^0 == 0 /\ -k^post5+k^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ j^0-j^post5 == 0), cost: 1 2: l3 -> l0 : __const_100^0'=__const_100^post3, i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (1-k^0 <= 0 /\ tmp^0-tmp^post3 == 0 /\ -j^post3+j^0 == 0 /\ -k^post3+k^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ i^0-i^post3 == 0 /\ -__const_100^post3+__const_100^0 == 0), cost: 1 3: l3 -> l2 : __const_100^0'=__const_100^post4, i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (j^0-j^post4 == 0 /\ tmp^0-tmp^post4 == 0 /\ -i^post4+i^0 == 0 /\ k^0 <= 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -k^post4+k^0 == 0 /\ -__const_100^post4+__const_100^0 == 0), cost: 1 11: l4 -> l7 : __const_100^0'=__const_100^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-k^0+i^0 <= 0 /\ -k^post12+k^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ j^0-j^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ k^0-i^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ i^0-i^post12 == 0), cost: 1 12: l4 -> l8 : __const_100^0'=__const_100^post13, i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ -__const_100^post13+__const_100^0 == 0 /\ -j^post13+j^0 == 0 /\ 1+k^0-i^0 <= 0 /\ tmp^0-tmp^post13 == 0 /\ -k^post13+k^0 == 0 /\ i^0-i^post13 == 0), cost: 1 13: l4 -> l8 : __const_100^0'=__const_100^post14, i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-i^post14+i^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ j^0-j^post14 == 0 /\ 1-k^0+i^0 <= 0 /\ -__const_100^post14+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ -k^post14+k^0 == 0), cost: 1 5: l5 -> l2 : __const_100^0'=__const_100^post6, i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-__const_100^post6+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ k^0-k^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -j^0+i^0 <= 0 /\ -i^post6+i^0 == 0 /\ j^0-j^post6 == 0), cost: 1 6: l5 -> l6 : __const_100^0'=__const_100^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (1+j^0-i^0 <= 0 /\ -1-j^0+j^post7 == 0 /\ -i^post7+i^0 == 0 /\ -__const_100^post7+__const_100^0 == 0 /\ k^0-k^post7 == 0 /\ tmp^0-tmp^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 8: l6 -> l5 : __const_100^0'=__const_100^post9, i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (k^0-k^post9 == 0 /\ -__const_100^post9+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ j^0-j^post9 == 0 /\ tmp^0-tmp^post9 == 0 /\ -i^post9+i^0 == 0), cost: 1 7: l7 -> l6 : __const_100^0'=__const_100^post8, i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp^post8+tmp^0 == 0 /\ j^post8 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ k^0-k^post8 == 0 /\ 1+i^post8-i^0 == 0 /\ -__const_100^post8+__const_100^0 == 0), cost: 1 9: l8 -> l1 : __const_100^0'=__const_100^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (-tmp^post10+tmp^0 == 0 /\ j^0-j^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -__const_100^post10+__const_100^0 == 0 /\ -1+i^post10-i^0 == 0 /\ k^0-k^post10 == 0), cost: 1 10: l8 -> l7 : __const_100^0'=__const_100^post11, i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-k^post11+k^0 == 0 /\ j^0-j^post11 == 0 /\ -__const_100^post11+__const_100^0 == 0 /\ -tmp^post11+tmp^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ i^0-i^post11 == 0), cost: 1 16: l10 -> l3 : __const_100^0'=__const_100^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ j^post16-j^post15 == 0 /\ k^0-k^post16 == 0 /\ j^0-j^post16 == 0 /\ -__const_100^post15+__const_100^post16 == 0 /\ -i^post16+i^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ i^post16-i^post15 == 0 /\ k^post15-tmp^post15 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ tmp___0^post16-tmp___0^post15 == 0), cost: 1 Eliminating location l9 by chaining: Applied chaining First rule: l10 -> l9 : __const_100^0'=__const_100^post16, i^0'=i^post16, j^0'=j^post16, k^0'=k^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (-__const_100^post16+__const_100^0 == 0 /\ k^0-k^post16 == 0 /\ j^0-j^post16 == 0 /\ -i^post16+i^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ tmp___0^0-tmp___0^post16 == 0), cost: 1 Second rule: l9 -> l3 : __const_100^0'=__const_100^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ -i^post15+i^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -__const_100^post15+__const_100^0 == 0 /\ j^0-j^post15 == 0 /\ k^post15-tmp^post15 == 0), cost: 1 New rule: l10 -> l3 : __const_100^0'=__const_100^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ j^post16-j^post15 == 0 /\ k^0-k^post16 == 0 /\ j^0-j^post16 == 0 /\ -__const_100^post15+__const_100^post16 == 0 /\ -i^post16+i^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ i^post16-i^post15 == 0 /\ k^post15-tmp^post15 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ tmp___0^post16-tmp___0^post15 == 0), cost: 1 Applied deletion Removed the following rules: 14 15 Simplified Transitions Start location: l10 Program variables: __const_100^0 i^0 j^0 k^0 tmp^0 tmp___0^0 17: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, k^0-__const_100^0 <= 0, cost: 1 18: l0 -> l2 : 1-k^0+__const_100^0 <= 0, cost: 1 21: l1 -> l4 : T, cost: 1 19: l3 -> l0 : 1-k^0 <= 0, cost: 1 20: l3 -> l2 : k^0 <= 0, cost: 1 28: l4 -> l7 : (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 29: l4 -> l8 : 1+k^0-i^0 <= 0, cost: 1 30: l4 -> l8 : 1-k^0+i^0 <= 0, cost: 1 22: l5 -> l2 : -j^0+i^0 <= 0, cost: 1 23: l5 -> l6 : j^0'=1+j^0, 1+j^0-i^0 <= 0, cost: 1 25: l6 -> l5 : T, cost: 1 24: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 26: l8 -> l1 : i^0'=1+i^0, T, cost: 1 27: l8 -> l7 : T, cost: 1 31: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __const_100^0'=__const_100^post1, i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (0 == 0 /\ i^post1 == 0 /\ k^0-__const_100^0 <= 0 /\ -tmp^post1+tmp^0 == 0 /\ j^0-j^post1 == 0 /\ k^0-k^post1 == 0 /\ -__const_100^post1+__const_100^0 == 0), cost: 1 New rule: l0 -> l1 : __const_100^0'=__const_100^0, i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, (0 == 0 /\ k^0-__const_100^0 <= 0), cost: 1 propagated equality i^post1 = 0 propagated equality tmp^post1 = tmp^0 propagated equality j^post1 = j^0 propagated equality k^post1 = k^0 propagated equality __const_100^post1 = __const_100^0 Simplified Guard Original rule: l0 -> l1 : __const_100^0'=__const_100^0, i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, (0 == 0 /\ k^0-__const_100^0 <= 0), cost: 1 New rule: l0 -> l1 : __const_100^0'=__const_100^0, i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, k^0-__const_100^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __const_100^0'=__const_100^0, i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, k^0-__const_100^0 <= 0, cost: 1 New rule: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, k^0-__const_100^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : __const_100^0'=__const_100^post2, i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-k^post2+k^0 == 0 /\ j^0-j^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ -__const_100^post2+__const_100^0 == 0 /\ 1-k^0+__const_100^0 <= 0 /\ i^0-i^post2 == 0), cost: 1 New rule: l0 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0+__const_100^0 <= 0), cost: 1 propagated equality k^post2 = k^0 propagated equality j^post2 = j^0 propagated equality tmp^post2 = tmp^0 propagated equality tmp___0^post2 = tmp___0^0 propagated equality __const_100^post2 = __const_100^0 propagated equality i^post2 = i^0 Simplified Guard Original rule: l0 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0+__const_100^0 <= 0), cost: 1 New rule: l0 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0+__const_100^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0+__const_100^0 <= 0, cost: 1 New rule: l0 -> l2 : 1-k^0+__const_100^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : __const_100^0'=__const_100^post3, i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (1-k^0 <= 0 /\ tmp^0-tmp^post3 == 0 /\ -j^post3+j^0 == 0 /\ -k^post3+k^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ i^0-i^post3 == 0 /\ -__const_100^post3+__const_100^0 == 0), cost: 1 New rule: l3 -> l0 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0 <= 0), cost: 1 propagated equality tmp^post3 = tmp^0 propagated equality j^post3 = j^0 propagated equality k^post3 = k^0 propagated equality tmp___0^post3 = tmp___0^0 propagated equality i^post3 = i^0 propagated equality __const_100^post3 = __const_100^0 Simplified Guard Original rule: l3 -> l0 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0 <= 0), cost: 1 New rule: l3 -> l0 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0 <= 0, cost: 1 New rule: l3 -> l0 : 1-k^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : __const_100^0'=__const_100^post4, i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (j^0-j^post4 == 0 /\ tmp^0-tmp^post4 == 0 /\ -i^post4+i^0 == 0 /\ k^0 <= 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -k^post4+k^0 == 0 /\ -__const_100^post4+__const_100^0 == 0), cost: 1 New rule: l3 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ k^0 <= 0), cost: 1 propagated equality j^post4 = j^0 propagated equality tmp^post4 = tmp^0 propagated equality i^post4 = i^0 propagated equality tmp___0^post4 = tmp___0^0 propagated equality k^post4 = k^0 propagated equality __const_100^post4 = __const_100^0 Simplified Guard Original rule: l3 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ k^0 <= 0), cost: 1 New rule: l3 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, k^0 <= 0, cost: 1 New rule: l3 -> l2 : k^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l4 : __const_100^0'=__const_100^post5, i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-i^post5+i^0 == 0 /\ -k^post5+k^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ j^0-j^post5 == 0), cost: 1 New rule: l1 -> l4 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality i^post5 = i^0 propagated equality k^post5 = k^0 propagated equality tmp^post5 = tmp^0 propagated equality tmp___0^post5 = tmp___0^0 propagated equality __const_100^post5 = __const_100^0 propagated equality j^post5 = j^0 Simplified Guard Original rule: l1 -> l4 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l1 -> l4 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l1 -> l4 : T, cost: 1 Propagated Equalities Original rule: l5 -> l2 : __const_100^0'=__const_100^post6, i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-__const_100^post6+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ k^0-k^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -j^0+i^0 <= 0 /\ -i^post6+i^0 == 0 /\ j^0-j^post6 == 0), cost: 1 New rule: l5 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -j^0+i^0 <= 0), cost: 1 propagated equality __const_100^post6 = __const_100^0 propagated equality tmp___0^post6 = tmp___0^0 propagated equality k^post6 = k^0 propagated equality tmp^post6 = tmp^0 propagated equality i^post6 = i^0 propagated equality j^post6 = j^0 Simplified Guard Original rule: l5 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -j^0+i^0 <= 0), cost: 1 New rule: l5 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -j^0+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l2 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -j^0+i^0 <= 0, cost: 1 New rule: l5 -> l2 : -j^0+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : __const_100^0'=__const_100^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (1+j^0-i^0 <= 0 /\ -1-j^0+j^post7 == 0 /\ -i^post7+i^0 == 0 /\ -__const_100^post7+__const_100^0 == 0 /\ k^0-k^post7 == 0 /\ tmp^0-tmp^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 New rule: l5 -> l6 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+j^0-i^0 <= 0), cost: 1 propagated equality j^post7 = 1+j^0 propagated equality i^post7 = i^0 propagated equality __const_100^post7 = __const_100^0 propagated equality k^post7 = k^0 propagated equality tmp^post7 = tmp^0 propagated equality tmp___0^post7 = tmp___0^0 Simplified Guard Original rule: l5 -> l6 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+j^0-i^0 <= 0), cost: 1 New rule: l5 -> l6 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+j^0-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+j^0-i^0 <= 0, cost: 1 New rule: l5 -> l6 : j^0'=1+j^0, 1+j^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : __const_100^0'=__const_100^post8, i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp^post8+tmp^0 == 0 /\ j^post8 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ k^0-k^post8 == 0 /\ 1+i^post8-i^0 == 0 /\ -__const_100^post8+__const_100^0 == 0), cost: 1 New rule: l7 -> l6 : __const_100^0'=__const_100^0, i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality tmp^post8 = tmp^0 propagated equality j^post8 = 0 propagated equality tmp___0^post8 = tmp___0^0 propagated equality k^post8 = k^0 propagated equality i^post8 = -1+i^0 propagated equality __const_100^post8 = __const_100^0 Simplified Guard Original rule: l7 -> l6 : __const_100^0'=__const_100^0, i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l7 -> l6 : __const_100^0'=__const_100^0, i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : __const_100^0'=__const_100^0, i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 Propagated Equalities Original rule: l6 -> l5 : __const_100^0'=__const_100^post9, i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (k^0-k^post9 == 0 /\ -__const_100^post9+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ j^0-j^post9 == 0 /\ tmp^0-tmp^post9 == 0 /\ -i^post9+i^0 == 0), cost: 1 New rule: l6 -> l5 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality k^post9 = k^0 propagated equality __const_100^post9 = __const_100^0 propagated equality tmp___0^post9 = tmp___0^0 propagated equality j^post9 = j^0 propagated equality tmp^post9 = tmp^0 propagated equality i^post9 = i^0 Simplified Guard Original rule: l6 -> l5 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l6 -> l5 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l5 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l6 -> l5 : T, cost: 1 Propagated Equalities Original rule: l8 -> l1 : __const_100^0'=__const_100^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (-tmp^post10+tmp^0 == 0 /\ j^0-j^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -__const_100^post10+__const_100^0 == 0 /\ -1+i^post10-i^0 == 0 /\ k^0-k^post10 == 0), cost: 1 New rule: l8 -> l1 : __const_100^0'=__const_100^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality tmp^post10 = tmp^0 propagated equality j^post10 = j^0 propagated equality tmp___0^post10 = tmp___0^0 propagated equality __const_100^post10 = __const_100^0 propagated equality i^post10 = 1+i^0 propagated equality k^post10 = k^0 Simplified Guard Original rule: l8 -> l1 : __const_100^0'=__const_100^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l8 -> l1 : __const_100^0'=__const_100^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l1 : __const_100^0'=__const_100^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l8 -> l1 : i^0'=1+i^0, T, cost: 1 Propagated Equalities Original rule: l8 -> l7 : __const_100^0'=__const_100^post11, i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-k^post11+k^0 == 0 /\ j^0-j^post11 == 0 /\ -__const_100^post11+__const_100^0 == 0 /\ -tmp^post11+tmp^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ i^0-i^post11 == 0), cost: 1 New rule: l8 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality k^post11 = k^0 propagated equality j^post11 = j^0 propagated equality __const_100^post11 = __const_100^0 propagated equality tmp^post11 = tmp^0 propagated equality tmp___0^post11 = tmp___0^0 propagated equality i^post11 = i^0 Simplified Guard Original rule: l8 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l8 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l8 -> l7 : T, cost: 1 made implied equalities explicit Original rule: l4 -> l7 : __const_100^0'=__const_100^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-k^0+i^0 <= 0 /\ -k^post12+k^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ j^0-j^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ k^0-i^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ i^0-i^post12 == 0), cost: 1 New rule: l4 -> l7 : __const_100^0'=__const_100^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ -k^post12+k^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ j^0-j^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ k^0-i^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ i^0-i^post12 == 0), cost: 1 Propagated Equalities Original rule: l4 -> l7 : __const_100^0'=__const_100^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ -k^post12+k^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ j^0-j^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ k^0-i^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ i^0-i^post12 == 0), cost: 1 New rule: l4 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 propagated equality k^post12 = k^0 propagated equality tmp^post12 = tmp^0 propagated equality j^post12 = j^0 propagated equality __const_100^post12 = __const_100^0 propagated equality tmp___0^post12 = tmp___0^0 propagated equality i^post12 = i^0 Simplified Guard Original rule: l4 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 New rule: l4 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 made implied equalities explicit Original rule: l4 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 New rule: l4 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l4 -> l7 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 New rule: l4 -> l7 : (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l8 : __const_100^0'=__const_100^post13, i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ -__const_100^post13+__const_100^0 == 0 /\ -j^post13+j^0 == 0 /\ 1+k^0-i^0 <= 0 /\ tmp^0-tmp^post13 == 0 /\ -k^post13+k^0 == 0 /\ i^0-i^post13 == 0), cost: 1 New rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+k^0-i^0 <= 0), cost: 1 propagated equality tmp___0^post13 = tmp___0^0 propagated equality __const_100^post13 = __const_100^0 propagated equality j^post13 = j^0 propagated equality tmp^post13 = tmp^0 propagated equality k^post13 = k^0 propagated equality i^post13 = i^0 Simplified Guard Original rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+k^0-i^0 <= 0), cost: 1 New rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+k^0-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+k^0-i^0 <= 0, cost: 1 New rule: l4 -> l8 : 1+k^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l8 : __const_100^0'=__const_100^post14, i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-i^post14+i^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ j^0-j^post14 == 0 /\ 1-k^0+i^0 <= 0 /\ -__const_100^post14+__const_100^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ -k^post14+k^0 == 0), cost: 1 New rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0+i^0 <= 0), cost: 1 propagated equality i^post14 = i^0 propagated equality tmp^post14 = tmp^0 propagated equality j^post14 = j^0 propagated equality __const_100^post14 = __const_100^0 propagated equality tmp___0^post14 = tmp___0^0 propagated equality k^post14 = k^0 Simplified Guard Original rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0+i^0 <= 0), cost: 1 New rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l8 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0+i^0 <= 0, cost: 1 New rule: l4 -> l8 : 1-k^0+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l3 : __const_100^0'=__const_100^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ j^post16-j^post15 == 0 /\ k^0-k^post16 == 0 /\ j^0-j^post16 == 0 /\ -__const_100^post15+__const_100^post16 == 0 /\ -i^post16+i^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ i^post16-i^post15 == 0 /\ k^post15-tmp^post15 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ tmp___0^post16-tmp___0^post15 == 0), cost: 1 New rule: l10 -> l3 : __const_100^0'=__const_100^post16, i^0'=i^post16, j^0'=j^post16, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post16, (0 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ k^0-k^post16 == 0 /\ j^0-j^post16 == 0 /\ -i^post16+i^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ tmp___0^0-tmp___0^post16 == 0), cost: 1 propagated equality j^post15 = j^post16 propagated equality __const_100^post15 = __const_100^post16 propagated equality i^post15 = i^post16 propagated equality k^post15 = tmp^post15 propagated equality tmp___0^post15 = tmp___0^post16 Propagated Equalities Original rule: l10 -> l3 : __const_100^0'=__const_100^post16, i^0'=i^post16, j^0'=j^post16, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post16, (0 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ k^0-k^post16 == 0 /\ j^0-j^post16 == 0 /\ -i^post16+i^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ tmp___0^0-tmp___0^post16 == 0), cost: 1 New rule: l10 -> l3 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality __const_100^post16 = __const_100^0 propagated equality k^post16 = k^0 propagated equality j^post16 = j^0 propagated equality i^post16 = i^0 propagated equality tmp^post16 = tmp^0 propagated equality tmp___0^post16 = tmp___0^0 Simplified Guard Original rule: l10 -> l3 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l10 -> l3 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l10 -> l3 : __const_100^0'=__const_100^0, i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Step with 31 Trace 31[T] Blocked [{}, {}] Step with 19 Trace 31[T], 19[(1-k^0 <= 0)] Blocked [{}, {}, {}] Step with 17 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 21 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T] Blocked [{}, {}, {}, {}, {}] Step with 30 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}] Step with 27 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T], 22[(-j^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}, {22[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {25[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {27[T]}] Step with 26 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 26[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {27[T]}, {}] Accelerate Start location: l10 Program variables: __const_100^0 i^0 j^0 k^0 tmp^0 tmp___0^0 17: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, k^0-__const_100^0 <= 0, cost: 1 18: l0 -> l2 : 1-k^0+__const_100^0 <= 0, cost: 1 21: l1 -> l4 : T, cost: 1 32: l1 -> l1 : i^0'=i^0+n, (k^0-i^0-n >= 0 /\ -1+n >= 0), cost: 1 19: l3 -> l0 : 1-k^0 <= 0, cost: 1 20: l3 -> l2 : k^0 <= 0, cost: 1 28: l4 -> l7 : (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 29: l4 -> l8 : 1+k^0-i^0 <= 0, cost: 1 30: l4 -> l8 : 1-k^0+i^0 <= 0, cost: 1 22: l5 -> l2 : -j^0+i^0 <= 0, cost: 1 23: l5 -> l6 : j^0'=1+j^0, 1+j^0-i^0 <= 0, cost: 1 25: l6 -> l5 : T, cost: 1 24: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 26: l8 -> l1 : i^0'=1+i^0, T, cost: 1 27: l8 -> l7 : T, cost: 1 31: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Loop Acceleration Original rule: l1 -> l1 : i^0'=1+i^0, 1-k^0+i^0 <= 0, cost: 1 New rule: l1 -> l1 : i^0'=i^0+n, (k^0-i^0-n >= 0 /\ -1+n >= 0), cost: 1 -1+k^0-i^0 >= 0 [0]: montonic decrease yields k^0-i^0-n >= 0 -1+k^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+k^0-i^0 >= 0) Replacement map: {-1+k^0-i^0 >= 0 -> k^0-i^0-n >= 0} Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {}, {}, {32[T]}] Step with 21 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T] Blocked [{}, {}, {}, {}, {32[T]}, {}] Step with 30 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {}] Step with 26 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 26[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}] Step with 27 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T], 22[(-j^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {22[T]}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T], 23[(1+j^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {22[T]}, {}] Accelerate Start location: l10 Program variables: __const_100^0 i^0 j^0 k^0 tmp^0 tmp___0^0 17: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, k^0-__const_100^0 <= 0, cost: 1 18: l0 -> l2 : 1-k^0+__const_100^0 <= 0, cost: 1 21: l1 -> l4 : T, cost: 1 32: l1 -> l1 : i^0'=i^0+n, (k^0-i^0-n >= 0 /\ -1+n >= 0), cost: 1 19: l3 -> l0 : 1-k^0 <= 0, cost: 1 20: l3 -> l2 : k^0 <= 0, cost: 1 28: l4 -> l7 : (-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0), cost: 1 29: l4 -> l8 : 1+k^0-i^0 <= 0, cost: 1 30: l4 -> l8 : 1-k^0+i^0 <= 0, cost: 1 22: l5 -> l2 : -j^0+i^0 <= 0, cost: 1 23: l5 -> l6 : j^0'=1+j^0, 1+j^0-i^0 <= 0, cost: 1 25: l6 -> l5 : T, cost: 1 33: l6 -> l6 : j^0'=n2+j^0, (-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0), cost: 1 24: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 26: l8 -> l1 : i^0'=1+i^0, T, cost: 1 27: l8 -> l7 : T, cost: 1 31: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Loop Acceleration Original rule: l6 -> l6 : j^0'=1+j^0, 1+j^0-i^0 <= 0, cost: 1 New rule: l6 -> l6 : j^0'=n2+j^0, (-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0), cost: 1 -1-j^0+i^0 >= 0 [0]: montonic decrease yields -n2-j^0+i^0 >= 0 -1-j^0+i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-j^0+i^0 >= 0) Replacement map: {-1-j^0+i^0 >= 0 -> -n2-j^0+i^0 >= 0} Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T], 23[(1+j^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {23[T]}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T], 22[(-j^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {23[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T], 22[(-j^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {22[T]}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T], 23[(1+j^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {22[T]}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T], 27[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}] Step with 28 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 25[T], 23[(1+j^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {23[T]}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 25[T], 22[(-j^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {23[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}] Step with 33 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T], 22[(-j^0+i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {22[T]}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T], 23[(1+j^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {22[T]}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T], 33[(-n2-j^0+i^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T], 28[(-k^0+i^0 <= 0 /\ -k^0+i^0 == 0 /\ k^0-i^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)], 21[T] Blocked [{}, {}, {}, {}, {32[T]}, {28[T], 30[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 32[(k^0-i^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {}, {}, {21[T], 32[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)] Blocked [{}, {}, {}, {32[T]}] Step with 21 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T] Blocked [{}, {}, {}, {32[T]}, {}] Step with 30 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}] Step with 27 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T], 22[(-j^0+i^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}, {23[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {25[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 27[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {27[T]}] Step with 26 Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)], 26[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {27[T]}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T], 30[(1-k^0+i^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {26[T], 27[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)], 21[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T], 30[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(k^0-__const_100^0 <= 0)] Blocked [{}, {}, {}, {21[T], 32[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)] Blocked [{}, {}, {17[T]}] Step with 18 Trace 31[T], 19[(1-k^0 <= 0)], 18[(1-k^0+__const_100^0 <= 0)] Blocked [{}, {}, {17[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)] Blocked [{}, {}, {17[T], 18[T]}] Backtrack Trace 31[T] Blocked [{}, {19[T]}] Step with 20 Trace 31[T], 20[(k^0 <= 0)] Blocked [{}, {19[T]}, {}] Backtrack Trace 31[T] Blocked [{}, {19[T], 20[T]}] Backtrack Trace Blocked [{31[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b