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