unknown Initial ITS Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 0: l0 -> l1 : i11^0'=i11^post1, i13^0'=i13^post1, i7^0'=i7^post1, i9^0'=i9^post1, i^0'=i^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (-i7^post1+i7^0 == 0 /\ -i13^post1+i13^0 == 0 /\ i9^0-i9^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ i11^0-i11^post1 == 0 /\ -i^post1+i^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0), cost: 1 16: l1 -> l5 : i11^0'=i11^post17, i13^0'=i13^post17, i7^0'=i7^post17, i9^0'=i9^post17, i^0'=i^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, (i11^0-i11^post17 == 0 /\ i^0-i^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ i9^1 == 0 /\ i9^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ 50-i7^0 <= 0 /\ -i13^post17+i13^0 == 0), cost: 1 17: l1 -> l0 : i11^0'=i11^post18, i13^0'=i13^post18, i7^0'=i7^post18, i9^0'=i9^post18, i^0'=i^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, (-i13^post18+i13^0 == 0 /\ -49+i7^0 <= 0 /\ i9^0-i9^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ i11^0-i11^post18 == 0 /\ -i^post18+i^0 == 0 /\ -tmp^post18+tmp^0 == 0 /\ -1+i7^post18-i7^0 == 0), cost: 1 1: l2 -> l3 : i11^0'=i11^post2, i13^0'=i13^post2, i7^0'=i7^post2, i9^0'=i9^post2, i^0'=i^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-tmp^post2+tmp^0 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ i11^0-i11^post2 == 0 /\ i^0-i^post2 == 0 /\ -i13^post2+i13^0 == 0 /\ 50-i^0 <= 0 /\ -i7^post2+i7^0 == 0 /\ i9^0-i9^post2 == 0), cost: 1 2: l2 -> l4 : i11^0'=i11^post3, i13^0'=i13^post3, i7^0'=i7^post3, i9^0'=i9^post3, i^0'=i^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (i11^0-i11^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ i13^0-i13^post3 == 0 /\ -i7^post3+i7^0 == 0 /\ -49+i^0 <= 0 /\ -1-i^0+i^post3 == 0 /\ i9^0-i9^post3 == 0), cost: 1 15: l4 -> l2 : i11^0'=i11^post16, i13^0'=i13^post16, i7^0'=i7^post16, i9^0'=i9^post16, i^0'=i^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (-i13^post16+i13^0 == 0 /\ i7^0-i7^post16 == 0 /\ -i^post16+i^0 == 0 /\ i9^0-i9^post16 == 0 /\ i11^0-i11^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 3: l5 -> l6 : i11^0'=i11^post4, i13^0'=i13^post4, i7^0'=i7^post4, i9^0'=i9^post4, i^0'=i^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (-i^post4+i^0 == 0 /\ -i7^post4+i7^0 == 0 /\ i9^0-i9^post4 == 0 /\ -i13^post4+i13^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ i11^0-i11^post4 == 0 /\ -tmp^post4+tmp^0 == 0), cost: 1 13: l6 -> l9 : i11^0'=i11^post14, i13^0'=i13^post14, i7^0'=i7^post14, i9^0'=i9^post14, i^0'=i^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (tmp___0^0-tmp___0^post14 == 0 /\ i13^0-i13^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ 50-i9^0 <= 0 /\ i11^0-i11^post14 == 0 /\ -i7^post14+i7^0 == 0 /\ i^post14 == 0 /\ i9^0-i9^post14 == 0), cost: 1 14: l6 -> l5 : i11^0'=i11^post15, i13^0'=i13^post15, i7^0'=i7^post15, i9^0'=i9^post15, i^0'=i^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (-1-i9^0+i9^post15 == 0 /\ -i^post15+i^0 == 0 /\ -49+i9^0 <= 0 /\ -tmp^post15+tmp^0 == 0 /\ -i7^post15+i7^0 == 0 /\ -i13^post15+i13^0 == 0 /\ i11^0-i11^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1 4: l7 -> l4 : i11^0'=i11^post5, i13^0'=i13^post5, i7^0'=i7^post5, i9^0'=i9^post5, i^0'=i^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (50-i13^0 <= 0 /\ i9^0-i9^post5 == 0 /\ i7^0-i7^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ i^post5 == 0 /\ i11^0-i11^post5 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -i13^post5+i13^0 == 0), cost: 1 5: l7 -> l8 : i11^0'=i11^post6, i13^0'=i13^post6, i7^0'=i7^post6, i9^0'=i9^post6, i^0'=i^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-1+i13^post6-i13^0 == 0 /\ -i11^post6+i11^0 == 0 /\ -i^post6+i^0 == 0 /\ i9^0-i9^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ i7^0-i7^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -49+i13^0 <= 0), cost: 1 12: l8 -> l7 : i11^0'=i11^post13, i13^0'=i13^post13, i7^0'=i7^post13, i9^0'=i9^post13, i^0'=i^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i^post13+i^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ i9^0-i9^post13 == 0 /\ -i13^post13+i13^0 == 0 /\ i7^0-i7^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ i11^0-i11^post13 == 0), cost: 1 6: l9 -> l10 : i11^0'=i11^post7, i13^0'=i13^post7, i7^0'=i7^post7, i9^0'=i9^post7, i^0'=i^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-i13^post7+i13^0 == 0 /\ -i7^post7+i7^0 == 0 /\ i^0-i^post7 == 0 /\ i9^0-i9^post7 == 0 /\ i11^0-i11^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 10: l10 -> l12 : i11^0'=i11^post11, i13^0'=i13^post11, i7^0'=i7^post11, i9^0'=i9^post11, i^0'=i^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-tmp^post11+tmp^0 == 0 /\ i7^0-i7^post11 == 0 /\ -i^post11+i^0 == 0 /\ i11^post11 == 0 /\ -i9^post11+i9^0 == 0 /\ -i13^post11+i13^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ 50-i^0 <= 0 /\ i11^1 == 0), cost: 1 11: l10 -> l9 : i11^0'=i11^post12, i13^0'=i13^post12, i7^0'=i7^post12, i9^0'=i9^post12, i^0'=i^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-i13^post12+i13^0 == 0 /\ -i11^post12+i11^0 == 0 /\ -i9^post12+i9^0 == 0 /\ -49+i^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ -1+i^post12-i^0 == 0 /\ i7^0-i7^post12 == 0 /\ -tmp___0^post12+tmp___0^0 == 0), cost: 1 7: l11 -> l8 : i11^0'=i11^post8, i13^0'=i13^post8, i7^0'=i7^post8, i9^0'=i9^post8, i^0'=i^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (50-i11^0 <= 0 /\ -tmp^post8+tmp^0 == 0 /\ -i11^post8+i11^0 == 0 /\ i13^post8 == 0 /\ -i^post8+i^0 == 0 /\ i7^0-i7^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ i13^1 == 0 /\ -i9^post8+i9^0 == 0), cost: 1 8: l11 -> l12 : i11^0'=i11^post9, i13^0'=i13^post9, i7^0'=i7^post9, i9^0'=i9^post9, i^0'=i^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (-i^post9+i^0 == 0 /\ -i13^post9+i13^0 == 0 /\ i9^0-i9^post9 == 0 /\ -1-i11^0+i11^post9 == 0 /\ i7^0-i7^post9 == 0 /\ -49+i11^0 <= 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 9: l12 -> l11 : i11^0'=i11^post10, i13^0'=i13^post10, i7^0'=i7^post10, i9^0'=i9^post10, i^0'=i^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (i11^0-i11^post10 == 0 /\ i^0-i^post10 == 0 /\ -tmp^post10+tmp^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ i13^0-i13^post10 == 0 /\ -i7^post10+i7^0 == 0 /\ i9^0-i9^post10 == 0), cost: 1 18: l13 -> l0 : i11^0'=i11^post19, i13^0'=i13^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (0 == 0 /\ i7^post19 == 0 /\ i9^0-i9^post19 == 0 /\ i7^1 == 0 /\ i^post19 == 0 /\ i11^0-i11^post19 == 0 /\ -i13^post19+i13^0 == 0), cost: 1 19: l14 -> l13 : i11^0'=i11^post20, i13^0'=i13^post20, i7^0'=i7^post20, i9^0'=i9^post20, i^0'=i^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, (i11^0-i11^post20 == 0 /\ i^0-i^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i13^0-i13^post20 == 0 /\ i9^0-i9^post20 == 0 /\ -tmp^post20+tmp^0 == 0), cost: 1 Chained Linear Paths Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 0: l0 -> l1 : i11^0'=i11^post1, i13^0'=i13^post1, i7^0'=i7^post1, i9^0'=i9^post1, i^0'=i^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (-i7^post1+i7^0 == 0 /\ -i13^post1+i13^0 == 0 /\ i9^0-i9^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ i11^0-i11^post1 == 0 /\ -i^post1+i^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0), cost: 1 16: l1 -> l5 : i11^0'=i11^post17, i13^0'=i13^post17, i7^0'=i7^post17, i9^0'=i9^post17, i^0'=i^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, (i11^0-i11^post17 == 0 /\ i^0-i^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ i9^1 == 0 /\ i9^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ 50-i7^0 <= 0 /\ -i13^post17+i13^0 == 0), cost: 1 17: l1 -> l0 : i11^0'=i11^post18, i13^0'=i13^post18, i7^0'=i7^post18, i9^0'=i9^post18, i^0'=i^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, (-i13^post18+i13^0 == 0 /\ -49+i7^0 <= 0 /\ i9^0-i9^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ i11^0-i11^post18 == 0 /\ -i^post18+i^0 == 0 /\ -tmp^post18+tmp^0 == 0 /\ -1+i7^post18-i7^0 == 0), cost: 1 1: l2 -> l3 : i11^0'=i11^post2, i13^0'=i13^post2, i7^0'=i7^post2, i9^0'=i9^post2, i^0'=i^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-tmp^post2+tmp^0 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ i11^0-i11^post2 == 0 /\ i^0-i^post2 == 0 /\ -i13^post2+i13^0 == 0 /\ 50-i^0 <= 0 /\ -i7^post2+i7^0 == 0 /\ i9^0-i9^post2 == 0), cost: 1 2: l2 -> l4 : i11^0'=i11^post3, i13^0'=i13^post3, i7^0'=i7^post3, i9^0'=i9^post3, i^0'=i^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (i11^0-i11^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ i13^0-i13^post3 == 0 /\ -i7^post3+i7^0 == 0 /\ -49+i^0 <= 0 /\ -1-i^0+i^post3 == 0 /\ i9^0-i9^post3 == 0), cost: 1 15: l4 -> l2 : i11^0'=i11^post16, i13^0'=i13^post16, i7^0'=i7^post16, i9^0'=i9^post16, i^0'=i^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (-i13^post16+i13^0 == 0 /\ i7^0-i7^post16 == 0 /\ -i^post16+i^0 == 0 /\ i9^0-i9^post16 == 0 /\ i11^0-i11^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 3: l5 -> l6 : i11^0'=i11^post4, i13^0'=i13^post4, i7^0'=i7^post4, i9^0'=i9^post4, i^0'=i^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (-i^post4+i^0 == 0 /\ -i7^post4+i7^0 == 0 /\ i9^0-i9^post4 == 0 /\ -i13^post4+i13^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ i11^0-i11^post4 == 0 /\ -tmp^post4+tmp^0 == 0), cost: 1 13: l6 -> l9 : i11^0'=i11^post14, i13^0'=i13^post14, i7^0'=i7^post14, i9^0'=i9^post14, i^0'=i^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (tmp___0^0-tmp___0^post14 == 0 /\ i13^0-i13^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ 50-i9^0 <= 0 /\ i11^0-i11^post14 == 0 /\ -i7^post14+i7^0 == 0 /\ i^post14 == 0 /\ i9^0-i9^post14 == 0), cost: 1 14: l6 -> l5 : i11^0'=i11^post15, i13^0'=i13^post15, i7^0'=i7^post15, i9^0'=i9^post15, i^0'=i^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (-1-i9^0+i9^post15 == 0 /\ -i^post15+i^0 == 0 /\ -49+i9^0 <= 0 /\ -tmp^post15+tmp^0 == 0 /\ -i7^post15+i7^0 == 0 /\ -i13^post15+i13^0 == 0 /\ i11^0-i11^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1 4: l7 -> l4 : i11^0'=i11^post5, i13^0'=i13^post5, i7^0'=i7^post5, i9^0'=i9^post5, i^0'=i^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (50-i13^0 <= 0 /\ i9^0-i9^post5 == 0 /\ i7^0-i7^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ i^post5 == 0 /\ i11^0-i11^post5 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -i13^post5+i13^0 == 0), cost: 1 5: l7 -> l8 : i11^0'=i11^post6, i13^0'=i13^post6, i7^0'=i7^post6, i9^0'=i9^post6, i^0'=i^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-1+i13^post6-i13^0 == 0 /\ -i11^post6+i11^0 == 0 /\ -i^post6+i^0 == 0 /\ i9^0-i9^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ i7^0-i7^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -49+i13^0 <= 0), cost: 1 12: l8 -> l7 : i11^0'=i11^post13, i13^0'=i13^post13, i7^0'=i7^post13, i9^0'=i9^post13, i^0'=i^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i^post13+i^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ i9^0-i9^post13 == 0 /\ -i13^post13+i13^0 == 0 /\ i7^0-i7^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ i11^0-i11^post13 == 0), cost: 1 6: l9 -> l10 : i11^0'=i11^post7, i13^0'=i13^post7, i7^0'=i7^post7, i9^0'=i9^post7, i^0'=i^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-i13^post7+i13^0 == 0 /\ -i7^post7+i7^0 == 0 /\ i^0-i^post7 == 0 /\ i9^0-i9^post7 == 0 /\ i11^0-i11^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 10: l10 -> l12 : i11^0'=i11^post11, i13^0'=i13^post11, i7^0'=i7^post11, i9^0'=i9^post11, i^0'=i^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-tmp^post11+tmp^0 == 0 /\ i7^0-i7^post11 == 0 /\ -i^post11+i^0 == 0 /\ i11^post11 == 0 /\ -i9^post11+i9^0 == 0 /\ -i13^post11+i13^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ 50-i^0 <= 0 /\ i11^1 == 0), cost: 1 11: l10 -> l9 : i11^0'=i11^post12, i13^0'=i13^post12, i7^0'=i7^post12, i9^0'=i9^post12, i^0'=i^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-i13^post12+i13^0 == 0 /\ -i11^post12+i11^0 == 0 /\ -i9^post12+i9^0 == 0 /\ -49+i^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ -1+i^post12-i^0 == 0 /\ i7^0-i7^post12 == 0 /\ -tmp___0^post12+tmp___0^0 == 0), cost: 1 7: l11 -> l8 : i11^0'=i11^post8, i13^0'=i13^post8, i7^0'=i7^post8, i9^0'=i9^post8, i^0'=i^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (50-i11^0 <= 0 /\ -tmp^post8+tmp^0 == 0 /\ -i11^post8+i11^0 == 0 /\ i13^post8 == 0 /\ -i^post8+i^0 == 0 /\ i7^0-i7^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ i13^1 == 0 /\ -i9^post8+i9^0 == 0), cost: 1 8: l11 -> l12 : i11^0'=i11^post9, i13^0'=i13^post9, i7^0'=i7^post9, i9^0'=i9^post9, i^0'=i^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (-i^post9+i^0 == 0 /\ -i13^post9+i13^0 == 0 /\ i9^0-i9^post9 == 0 /\ -1-i11^0+i11^post9 == 0 /\ i7^0-i7^post9 == 0 /\ -49+i11^0 <= 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 9: l12 -> l11 : i11^0'=i11^post10, i13^0'=i13^post10, i7^0'=i7^post10, i9^0'=i9^post10, i^0'=i^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (i11^0-i11^post10 == 0 /\ i^0-i^post10 == 0 /\ -tmp^post10+tmp^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ i13^0-i13^post10 == 0 /\ -i7^post10+i7^0 == 0 /\ i9^0-i9^post10 == 0), cost: 1 20: l14 -> l0 : i11^0'=i11^post19, i13^0'=i13^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (0 == 0 /\ i11^0-i11^post20 == 0 /\ i^0-i^post20 == 0 /\ i7^post19 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i7^1 == 0 /\ i13^0-i13^post20 == 0 /\ -i11^post19+i11^post20 == 0 /\ -i9^post19+i9^post20 == 0 /\ i^post19 == 0 /\ i9^0-i9^post20 == 0 /\ -i13^post19+i13^post20 == 0 /\ -tmp^post20+tmp^0 == 0), cost: 1 Eliminating location l13 by chaining: Applied chaining First rule: l14 -> l13 : i11^0'=i11^post20, i13^0'=i13^post20, i7^0'=i7^post20, i9^0'=i9^post20, i^0'=i^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, (i11^0-i11^post20 == 0 /\ i^0-i^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i13^0-i13^post20 == 0 /\ i9^0-i9^post20 == 0 /\ -tmp^post20+tmp^0 == 0), cost: 1 Second rule: l13 -> l0 : i11^0'=i11^post19, i13^0'=i13^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (0 == 0 /\ i7^post19 == 0 /\ i9^0-i9^post19 == 0 /\ i7^1 == 0 /\ i^post19 == 0 /\ i11^0-i11^post19 == 0 /\ -i13^post19+i13^0 == 0), cost: 1 New rule: l14 -> l0 : i11^0'=i11^post19, i13^0'=i13^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (0 == 0 /\ i11^0-i11^post20 == 0 /\ i^0-i^post20 == 0 /\ i7^post19 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i7^1 == 0 /\ i13^0-i13^post20 == 0 /\ -i11^post19+i11^post20 == 0 /\ -i9^post19+i9^post20 == 0 /\ i^post19 == 0 /\ i9^0-i9^post20 == 0 /\ -i13^post19+i13^post20 == 0 /\ -tmp^post20+tmp^0 == 0), cost: 1 Applied deletion Removed the following rules: 18 19 Simplified Transitions Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 21: l0 -> l1 : T, cost: 1 37: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 38: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 22: l2 -> l3 : 50-i^0 <= 0, cost: 1 23: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l4 -> l2 : T, cost: 1 24: l5 -> l6 : T, cost: 1 34: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 35: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 25: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 26: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 33: l8 -> l7 : T, cost: 1 27: l9 -> l10 : T, cost: 1 31: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 32: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 28: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 29: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 30: l12 -> l11 : T, cost: 1 39: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : i11^0'=i11^post1, i13^0'=i13^post1, i7^0'=i7^post1, i9^0'=i9^post1, i^0'=i^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (-i7^post1+i7^0 == 0 /\ -i13^post1+i13^0 == 0 /\ i9^0-i9^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ i11^0-i11^post1 == 0 /\ -i^post1+i^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0), cost: 1 New rule: l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality i7^post1 = i7^0 propagated equality i13^post1 = i13^0 propagated equality i9^post1 = i9^0 propagated equality tmp^post1 = tmp^0 propagated equality i11^post1 = i11^0 propagated equality i^post1 = i^0 propagated equality tmp___0^post1 = tmp___0^0 Simplified Guard Original rule: l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : i11^0'=i11^post2, i13^0'=i13^post2, i7^0'=i7^post2, i9^0'=i9^post2, i^0'=i^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-tmp^post2+tmp^0 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ i11^0-i11^post2 == 0 /\ i^0-i^post2 == 0 /\ -i13^post2+i13^0 == 0 /\ 50-i^0 <= 0 /\ -i7^post2+i7^0 == 0 /\ i9^0-i9^post2 == 0), cost: 1 New rule: l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1 propagated equality tmp^post2 = tmp^0 propagated equality tmp___0^post2 = tmp___0^0 propagated equality i11^post2 = i11^0 propagated equality i^post2 = i^0 propagated equality i13^post2 = i13^0 propagated equality i7^post2 = i7^0 propagated equality i9^post2 = i9^0 Simplified Guard Original rule: l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1 New rule: l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1 New rule: l2 -> l3 : 50-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l4 : i11^0'=i11^post3, i13^0'=i13^post3, i7^0'=i7^post3, i9^0'=i9^post3, i^0'=i^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (i11^0-i11^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ i13^0-i13^post3 == 0 /\ -i7^post3+i7^0 == 0 /\ -49+i^0 <= 0 /\ -1-i^0+i^post3 == 0 /\ i9^0-i9^post3 == 0), cost: 1 New rule: l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1 propagated equality i11^post3 = i11^0 propagated equality tmp^post3 = tmp^0 propagated equality tmp___0^post3 = tmp___0^0 propagated equality i13^post3 = i13^0 propagated equality i7^post3 = i7^0 propagated equality i^post3 = 1+i^0 propagated equality i9^post3 = i9^0 Simplified Guard Original rule: l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1 New rule: l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1 New rule: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : i11^0'=i11^post4, i13^0'=i13^post4, i7^0'=i7^post4, i9^0'=i9^post4, i^0'=i^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (-i^post4+i^0 == 0 /\ -i7^post4+i7^0 == 0 /\ i9^0-i9^post4 == 0 /\ -i13^post4+i13^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ i11^0-i11^post4 == 0 /\ -tmp^post4+tmp^0 == 0), cost: 1 New rule: l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality i^post4 = i^0 propagated equality i7^post4 = i7^0 propagated equality i9^post4 = i9^0 propagated equality i13^post4 = i13^0 propagated equality tmp___0^post4 = tmp___0^0 propagated equality i11^post4 = i11^0 propagated equality tmp^post4 = tmp^0 Simplified Guard Original rule: l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l5 -> l6 : T, cost: 1 Propagated Equalities Original rule: l7 -> l4 : i11^0'=i11^post5, i13^0'=i13^post5, i7^0'=i7^post5, i9^0'=i9^post5, i^0'=i^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (50-i13^0 <= 0 /\ i9^0-i9^post5 == 0 /\ i7^0-i7^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ i^post5 == 0 /\ i11^0-i11^post5 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -i13^post5+i13^0 == 0), cost: 1 New rule: l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i13^0 <= 0), cost: 1 propagated equality i9^post5 = i9^0 propagated equality i7^post5 = i7^0 propagated equality tmp___0^post5 = tmp___0^0 propagated equality i^post5 = 0 propagated equality i11^post5 = i11^0 propagated equality tmp^post5 = tmp^0 propagated equality i13^post5 = i13^0 Simplified Guard Original rule: l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i13^0 <= 0), cost: 1 New rule: l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i13^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i13^0 <= 0, cost: 1 New rule: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l8 : i11^0'=i11^post6, i13^0'=i13^post6, i7^0'=i7^post6, i9^0'=i9^post6, i^0'=i^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (-1+i13^post6-i13^0 == 0 /\ -i11^post6+i11^0 == 0 /\ -i^post6+i^0 == 0 /\ i9^0-i9^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ i7^0-i7^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ -49+i13^0 <= 0), cost: 1 New rule: l7 -> l8 : i11^0'=i11^0, i13^0'=1+i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i13^0 <= 0), cost: 1 propagated equality i13^post6 = 1+i13^0 propagated equality i11^post6 = i11^0 propagated equality i^post6 = i^0 propagated equality i9^post6 = i9^0 propagated equality tmp___0^post6 = tmp___0^0 propagated equality i7^post6 = i7^0 propagated equality tmp^post6 = tmp^0 Simplified Guard Original rule: l7 -> l8 : i11^0'=i11^0, i13^0'=1+i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i13^0 <= 0), cost: 1 New rule: l7 -> l8 : i11^0'=i11^0, i13^0'=1+i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i13^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l8 : i11^0'=i11^0, i13^0'=1+i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i13^0 <= 0, cost: 1 New rule: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l10 : i11^0'=i11^post7, i13^0'=i13^post7, i7^0'=i7^post7, i9^0'=i9^post7, i^0'=i^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-i13^post7+i13^0 == 0 /\ -i7^post7+i7^0 == 0 /\ i^0-i^post7 == 0 /\ i9^0-i9^post7 == 0 /\ i11^0-i11^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 New rule: l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality i13^post7 = i13^0 propagated equality i7^post7 = i7^0 propagated equality i^post7 = i^0 propagated equality i9^post7 = i9^0 propagated equality i11^post7 = i11^0 propagated equality tmp^post7 = tmp^0 propagated equality tmp___0^post7 = tmp___0^0 Simplified Guard Original rule: l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l9 -> l10 : T, cost: 1 Propagated Equalities Original rule: l11 -> l8 : i11^0'=i11^post8, i13^0'=i13^post8, i7^0'=i7^post8, i9^0'=i9^post8, i^0'=i^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (50-i11^0 <= 0 /\ -tmp^post8+tmp^0 == 0 /\ -i11^post8+i11^0 == 0 /\ i13^post8 == 0 /\ -i^post8+i^0 == 0 /\ i7^0-i7^post8 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ i13^1 == 0 /\ -i9^post8+i9^0 == 0), cost: 1 New rule: l11 -> l8 : i11^0'=i11^0, i13^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i11^0 <= 0 /\ i13^1 == 0), cost: 1 propagated equality tmp^post8 = tmp^0 propagated equality i11^post8 = i11^0 propagated equality i13^post8 = 0 propagated equality i^post8 = i^0 propagated equality i7^post8 = i7^0 propagated equality tmp___0^post8 = tmp___0^0 propagated equality i9^post8 = i9^0 Propagated Equalities Original rule: l11 -> l8 : i11^0'=i11^0, i13^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i11^0 <= 0 /\ i13^1 == 0), cost: 1 New rule: l11 -> l8 : i11^0'=i11^0, i13^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i11^0 <= 0), cost: 1 propagated equality i13^1 = 0 Simplified Guard Original rule: l11 -> l8 : i11^0'=i11^0, i13^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i11^0 <= 0), cost: 1 New rule: l11 -> l8 : i11^0'=i11^0, i13^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i11^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l8 : i11^0'=i11^0, i13^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i11^0 <= 0, cost: 1 New rule: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l12 : i11^0'=i11^post9, i13^0'=i13^post9, i7^0'=i7^post9, i9^0'=i9^post9, i^0'=i^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (-i^post9+i^0 == 0 /\ -i13^post9+i13^0 == 0 /\ i9^0-i9^post9 == 0 /\ -1-i11^0+i11^post9 == 0 /\ i7^0-i7^post9 == 0 /\ -49+i11^0 <= 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 New rule: l11 -> l12 : i11^0'=1+i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i11^0 <= 0), cost: 1 propagated equality i^post9 = i^0 propagated equality i13^post9 = i13^0 propagated equality i9^post9 = i9^0 propagated equality i11^post9 = 1+i11^0 propagated equality i7^post9 = i7^0 propagated equality tmp___0^post9 = tmp___0^0 propagated equality tmp^post9 = tmp^0 Simplified Guard Original rule: l11 -> l12 : i11^0'=1+i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i11^0 <= 0), cost: 1 New rule: l11 -> l12 : i11^0'=1+i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i11^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l12 : i11^0'=1+i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i11^0 <= 0, cost: 1 New rule: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 Propagated Equalities Original rule: l12 -> l11 : i11^0'=i11^post10, i13^0'=i13^post10, i7^0'=i7^post10, i9^0'=i9^post10, i^0'=i^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (i11^0-i11^post10 == 0 /\ i^0-i^post10 == 0 /\ -tmp^post10+tmp^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ i13^0-i13^post10 == 0 /\ -i7^post10+i7^0 == 0 /\ i9^0-i9^post10 == 0), cost: 1 New rule: l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality i11^post10 = i11^0 propagated equality i^post10 = i^0 propagated equality tmp^post10 = tmp^0 propagated equality tmp___0^post10 = tmp___0^0 propagated equality i13^post10 = i13^0 propagated equality i7^post10 = i7^0 propagated equality i9^post10 = i9^0 Simplified Guard Original rule: l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l12 -> l11 : T, cost: 1 Propagated Equalities Original rule: l10 -> l12 : i11^0'=i11^post11, i13^0'=i13^post11, i7^0'=i7^post11, i9^0'=i9^post11, i^0'=i^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-tmp^post11+tmp^0 == 0 /\ i7^0-i7^post11 == 0 /\ -i^post11+i^0 == 0 /\ i11^post11 == 0 /\ -i9^post11+i9^0 == 0 /\ -i13^post11+i13^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ 50-i^0 <= 0 /\ i11^1 == 0), cost: 1 New rule: l10 -> l12 : i11^0'=0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0 /\ i11^1 == 0), cost: 1 propagated equality tmp^post11 = tmp^0 propagated equality i7^post11 = i7^0 propagated equality i^post11 = i^0 propagated equality i11^post11 = 0 propagated equality i9^post11 = i9^0 propagated equality i13^post11 = i13^0 propagated equality tmp___0^post11 = tmp___0^0 Propagated Equalities Original rule: l10 -> l12 : i11^0'=0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0 /\ i11^1 == 0), cost: 1 New rule: l10 -> l12 : i11^0'=0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1 propagated equality i11^1 = 0 Simplified Guard Original rule: l10 -> l12 : i11^0'=0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1 New rule: l10 -> l12 : i11^0'=0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l12 : i11^0'=0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1 New rule: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l9 : i11^0'=i11^post12, i13^0'=i13^post12, i7^0'=i7^post12, i9^0'=i9^post12, i^0'=i^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-i13^post12+i13^0 == 0 /\ -i11^post12+i11^0 == 0 /\ -i9^post12+i9^0 == 0 /\ -49+i^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ -1+i^post12-i^0 == 0 /\ i7^0-i7^post12 == 0 /\ -tmp___0^post12+tmp___0^0 == 0), cost: 1 New rule: l10 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1 propagated equality i13^post12 = i13^0 propagated equality i11^post12 = i11^0 propagated equality i9^post12 = i9^0 propagated equality tmp^post12 = tmp^0 propagated equality i^post12 = 1+i^0 propagated equality i7^post12 = i7^0 propagated equality tmp___0^post12 = tmp___0^0 Simplified Guard Original rule: l10 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1 New rule: l10 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1 New rule: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l7 : i11^0'=i11^post13, i13^0'=i13^post13, i7^0'=i7^post13, i9^0'=i9^post13, i^0'=i^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i^post13+i^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ i9^0-i9^post13 == 0 /\ -i13^post13+i13^0 == 0 /\ i7^0-i7^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ i11^0-i11^post13 == 0), cost: 1 New rule: l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality i^post13 = i^0 propagated equality tmp___0^post13 = tmp___0^0 propagated equality i9^post13 = i9^0 propagated equality i13^post13 = i13^0 propagated equality i7^post13 = i7^0 propagated equality tmp^post13 = tmp^0 propagated equality i11^post13 = i11^0 Simplified Guard Original rule: l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l8 -> l7 : T, cost: 1 Propagated Equalities Original rule: l6 -> l9 : i11^0'=i11^post14, i13^0'=i13^post14, i7^0'=i7^post14, i9^0'=i9^post14, i^0'=i^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (tmp___0^0-tmp___0^post14 == 0 /\ i13^0-i13^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ 50-i9^0 <= 0 /\ i11^0-i11^post14 == 0 /\ -i7^post14+i7^0 == 0 /\ i^post14 == 0 /\ i9^0-i9^post14 == 0), cost: 1 New rule: l6 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i9^0 <= 0), cost: 1 propagated equality tmp___0^post14 = tmp___0^0 propagated equality i13^post14 = i13^0 propagated equality tmp^post14 = tmp^0 propagated equality i11^post14 = i11^0 propagated equality i7^post14 = i7^0 propagated equality i^post14 = 0 propagated equality i9^post14 = i9^0 Simplified Guard Original rule: l6 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i9^0 <= 0), cost: 1 New rule: l6 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i9^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l9 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i9^0 <= 0, cost: 1 New rule: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l5 : i11^0'=i11^post15, i13^0'=i13^post15, i7^0'=i7^post15, i9^0'=i9^post15, i^0'=i^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (-1-i9^0+i9^post15 == 0 /\ -i^post15+i^0 == 0 /\ -49+i9^0 <= 0 /\ -tmp^post15+tmp^0 == 0 /\ -i7^post15+i7^0 == 0 /\ -i13^post15+i13^0 == 0 /\ i11^0-i11^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1 New rule: l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i9^0 <= 0), cost: 1 propagated equality i9^post15 = 1+i9^0 propagated equality i^post15 = i^0 propagated equality tmp^post15 = tmp^0 propagated equality i7^post15 = i7^0 propagated equality i13^post15 = i13^0 propagated equality i11^post15 = i11^0 propagated equality tmp___0^post15 = tmp___0^0 Simplified Guard Original rule: l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i9^0 <= 0), cost: 1 New rule: l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i9^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i9^0 <= 0, cost: 1 New rule: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l2 : i11^0'=i11^post16, i13^0'=i13^post16, i7^0'=i7^post16, i9^0'=i9^post16, i^0'=i^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (-i13^post16+i13^0 == 0 /\ i7^0-i7^post16 == 0 /\ -i^post16+i^0 == 0 /\ i9^0-i9^post16 == 0 /\ i11^0-i11^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 New rule: l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality i13^post16 = i13^0 propagated equality i7^post16 = i7^0 propagated equality i^post16 = i^0 propagated equality i9^post16 = i9^0 propagated equality i11^post16 = i11^0 propagated equality tmp___0^post16 = tmp___0^0 propagated equality tmp^post16 = tmp^0 Simplified Guard Original rule: l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l4 -> l2 : T, cost: 1 Propagated Equalities Original rule: l1 -> l5 : i11^0'=i11^post17, i13^0'=i13^post17, i7^0'=i7^post17, i9^0'=i9^post17, i^0'=i^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, (i11^0-i11^post17 == 0 /\ i^0-i^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ i9^1 == 0 /\ i9^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ 50-i7^0 <= 0 /\ -i13^post17+i13^0 == 0), cost: 1 New rule: l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i9^1 == 0 /\ 50-i7^0 <= 0), cost: 1 propagated equality i11^post17 = i11^0 propagated equality i^post17 = i^0 propagated equality i7^post17 = i7^0 propagated equality i9^post17 = 0 propagated equality tmp^post17 = tmp^0 propagated equality tmp___0^post17 = tmp___0^0 propagated equality i13^post17 = i13^0 Propagated Equalities Original rule: l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i9^1 == 0 /\ 50-i7^0 <= 0), cost: 1 New rule: l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i7^0 <= 0), cost: 1 propagated equality i9^1 = 0 Simplified Guard Original rule: l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i7^0 <= 0), cost: 1 New rule: l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i7^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i7^0 <= 0, cost: 1 New rule: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l0 : i11^0'=i11^post18, i13^0'=i13^post18, i7^0'=i7^post18, i9^0'=i9^post18, i^0'=i^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, (-i13^post18+i13^0 == 0 /\ -49+i7^0 <= 0 /\ i9^0-i9^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ i11^0-i11^post18 == 0 /\ -i^post18+i^0 == 0 /\ -tmp^post18+tmp^0 == 0 /\ -1+i7^post18-i7^0 == 0), cost: 1 New rule: l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i7^0 <= 0), cost: 1 propagated equality i13^post18 = i13^0 propagated equality i9^post18 = i9^0 propagated equality tmp___0^post18 = tmp___0^0 propagated equality i11^post18 = i11^0 propagated equality i^post18 = i^0 propagated equality tmp^post18 = tmp^0 propagated equality i7^post18 = 1+i7^0 Simplified Guard Original rule: l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i7^0 <= 0), cost: 1 New rule: l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i7^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i7^0 <= 0, cost: 1 New rule: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 Propagated Equalities Original rule: l14 -> l0 : i11^0'=i11^post19, i13^0'=i13^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (0 == 0 /\ i11^0-i11^post20 == 0 /\ i^0-i^post20 == 0 /\ i7^post19 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i7^1 == 0 /\ i13^0-i13^post20 == 0 /\ -i11^post19+i11^post20 == 0 /\ -i9^post19+i9^post20 == 0 /\ i^post19 == 0 /\ i9^0-i9^post20 == 0 /\ -i13^post19+i13^post20 == 0 /\ -tmp^post20+tmp^0 == 0), cost: 1 New rule: l14 -> l0 : i11^0'=i11^post20, i13^0'=i13^post20, i7^0'=0, i9^0'=i9^post20, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (0 == 0 /\ i11^0-i11^post20 == 0 /\ i^0-i^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i7^1 == 0 /\ i13^0-i13^post20 == 0 /\ i9^0-i9^post20 == 0 /\ -tmp^post20+tmp^0 == 0), cost: 1 propagated equality i7^post19 = 0 propagated equality i11^post19 = i11^post20 propagated equality i9^post19 = i9^post20 propagated equality i^post19 = 0 propagated equality i13^post19 = i13^post20 Propagated Equalities Original rule: l14 -> l0 : i11^0'=i11^post20, i13^0'=i13^post20, i7^0'=0, i9^0'=i9^post20, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (0 == 0 /\ i11^0-i11^post20 == 0 /\ i^0-i^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i7^1 == 0 /\ i13^0-i13^post20 == 0 /\ i9^0-i9^post20 == 0 /\ -tmp^post20+tmp^0 == 0), cost: 1 New rule: l14 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, 0 == 0, cost: 1 propagated equality i11^post20 = i11^0 propagated equality i^post20 = i^0 propagated equality tmp___0^post20 = tmp___0^0 propagated equality i7^post20 = i7^0 propagated equality i7^1 = 0 propagated equality i13^post20 = i13^0 propagated equality i9^post20 = i9^0 propagated equality tmp^post20 = tmp^0 Simplified Guard Original rule: l14 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, 0 == 0, cost: 1 New rule: l14 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Removed Trivial Updates Original rule: l14 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 New rule: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Step with 39 Trace 39[T] Blocked [{}, {}] Step with 21 Trace 39[T], 21[T] Blocked [{}, {}, {}] Step with 38 Trace 39[T], 21[T], 38[(-49+i7^0 <= 0)] Blocked [{}, {}, {37[T]}, {}] Accelerate Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 21: l0 -> l1 : T, cost: 1 40: l0 -> l0 : i7^0'=i7^0+n, (50-i7^0-n >= 0 /\ -1+n >= 0), cost: 1 37: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 38: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 22: l2 -> l3 : 50-i^0 <= 0, cost: 1 23: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l4 -> l2 : T, cost: 1 24: l5 -> l6 : T, cost: 1 34: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 35: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 25: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 26: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 33: l8 -> l7 : T, cost: 1 27: l9 -> l10 : T, cost: 1 31: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 32: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 28: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 29: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 30: l12 -> l11 : T, cost: 1 39: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 New rule: l0 -> l0 : i7^0'=i7^0+n, (50-i7^0-n >= 0 /\ -1+n >= 0), cost: 1 49-i7^0 >= 0 [0]: montonic decrease yields 50-i7^0-n >= 0 49-i7^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i7^0 >= 0) Replacement map: {49-i7^0 >= 0 -> 50-i7^0-n >= 0} Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {40[T]}] Step with 21 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T] Blocked [{}, {}, {40[T]}, {}] Step with 38 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 38[(-49+i7^0 <= 0)] Blocked [{}, {}, {40[T]}, {}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T] Blocked [{}, {}, {40[T]}, {38[T]}] Step with 37 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}] Step with 24 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 24[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {}] Step with 35 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 24[T], 35[(-49+i9^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {34[T]}, {}] Accelerate Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 21: l0 -> l1 : T, cost: 1 40: l0 -> l0 : i7^0'=i7^0+n, (50-i7^0-n >= 0 /\ -1+n >= 0), cost: 1 37: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 38: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 22: l2 -> l3 : 50-i^0 <= 0, cost: 1 23: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l4 -> l2 : T, cost: 1 24: l5 -> l6 : T, cost: 1 41: l5 -> l5 : i9^0'=i9^0+n2, (50-i9^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 34: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 35: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 25: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 26: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 33: l8 -> l7 : T, cost: 1 27: l9 -> l10 : T, cost: 1 31: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 32: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 28: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 29: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 30: l12 -> l11 : T, cost: 1 39: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Loop Acceleration Original rule: l5 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 New rule: l5 -> l5 : i9^0'=i9^0+n2, (50-i9^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 49-i9^0 >= 0 [0]: montonic decrease yields 50-i9^0-n2 >= 0 49-i9^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i9^0 >= 0) Replacement map: {49-i9^0 >= 0 -> 50-i9^0-n2 >= 0} Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}] Step with 24 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {}] Step with 35 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 35[(-49+i9^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}] Step with 34 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}] Step with 27 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 27[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {}] Step with 32 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 27[T], 32[(-49+i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {31[T]}, {}] Accelerate Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 21: l0 -> l1 : T, cost: 1 40: l0 -> l0 : i7^0'=i7^0+n, (50-i7^0-n >= 0 /\ -1+n >= 0), cost: 1 37: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 38: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 22: l2 -> l3 : 50-i^0 <= 0, cost: 1 23: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l4 -> l2 : T, cost: 1 24: l5 -> l6 : T, cost: 1 41: l5 -> l5 : i9^0'=i9^0+n2, (50-i9^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 34: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 35: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 25: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 26: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 33: l8 -> l7 : T, cost: 1 27: l9 -> l10 : T, cost: 1 42: l9 -> l9 : i^0'=n3+i^0, (-1+n3 >= 0 /\ 50-n3-i^0 >= 0), cost: 1 31: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 32: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 28: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 29: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 30: l12 -> l11 : T, cost: 1 39: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Loop Acceleration Original rule: l9 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 New rule: l9 -> l9 : i^0'=n3+i^0, (-1+n3 >= 0 /\ 50-n3-i^0 >= 0), cost: 1 49-i^0 >= 0 [0]: montonic decrease yields 50-n3-i^0 >= 0 49-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i^0 >= 0) Replacement map: {49-i^0 >= 0 -> 50-n3-i^0 >= 0} Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}] Step with 27 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {}] Step with 32 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 32[(-49+i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}] Step with 31 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}] Step with 30 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 30[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {}] Step with 29 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 30[T], 29[(-49+i11^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {28[T]}, {}] Accelerate Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 21: l0 -> l1 : T, cost: 1 40: l0 -> l0 : i7^0'=i7^0+n, (50-i7^0-n >= 0 /\ -1+n >= 0), cost: 1 37: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 38: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 22: l2 -> l3 : 50-i^0 <= 0, cost: 1 23: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l4 -> l2 : T, cost: 1 24: l5 -> l6 : T, cost: 1 41: l5 -> l5 : i9^0'=i9^0+n2, (50-i9^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 34: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 35: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 25: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 26: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 33: l8 -> l7 : T, cost: 1 27: l9 -> l10 : T, cost: 1 42: l9 -> l9 : i^0'=n3+i^0, (-1+n3 >= 0 /\ 50-n3-i^0 >= 0), cost: 1 31: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 32: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 28: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 29: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 30: l12 -> l11 : T, cost: 1 43: l12 -> l12 : i11^0'=n4+i11^0, (50-n4-i11^0 >= 0 /\ -1+n4 >= 0), cost: 1 39: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Loop Acceleration Original rule: l12 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 New rule: l12 -> l12 : i11^0'=n4+i11^0, (50-n4-i11^0 >= 0 /\ -1+n4 >= 0), cost: 1 49-i11^0 >= 0 [0]: montonic decrease yields 50-n4-i11^0 >= 0 49-i11^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i11^0 >= 0) Replacement map: {49-i11^0 >= 0 -> 50-n4-i11^0 >= 0} Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}] Step with 30 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {}] Step with 29 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 29[(-49+i11^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}] Step with 28 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}] Step with 33 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 33[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {}] Step with 26 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 33[T], 26[(-49+i13^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {25[T]}, {}] Accelerate Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 21: l0 -> l1 : T, cost: 1 40: l0 -> l0 : i7^0'=i7^0+n, (50-i7^0-n >= 0 /\ -1+n >= 0), cost: 1 37: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 38: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 22: l2 -> l3 : 50-i^0 <= 0, cost: 1 23: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l4 -> l2 : T, cost: 1 24: l5 -> l6 : T, cost: 1 41: l5 -> l5 : i9^0'=i9^0+n2, (50-i9^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 34: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 35: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 25: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 26: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 33: l8 -> l7 : T, cost: 1 44: l8 -> l8 : i13^0'=n5+i13^0, (50-n5-i13^0 >= 0 /\ -1+n5 >= 0), cost: 1 27: l9 -> l10 : T, cost: 1 42: l9 -> l9 : i^0'=n3+i^0, (-1+n3 >= 0 /\ 50-n3-i^0 >= 0), cost: 1 31: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 32: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 28: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 29: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 30: l12 -> l11 : T, cost: 1 43: l12 -> l12 : i11^0'=n4+i11^0, (50-n4-i11^0 >= 0 /\ -1+n4 >= 0), cost: 1 39: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Loop Acceleration Original rule: l8 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 New rule: l8 -> l8 : i13^0'=n5+i13^0, (50-n5-i13^0 >= 0 /\ -1+n5 >= 0), cost: 1 49-i13^0 >= 0 [0]: montonic decrease yields 50-n5-i13^0 >= 0 49-i13^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i13^0 >= 0) Replacement map: {49-i13^0 >= 0 -> 50-n5-i13^0 >= 0} Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}] Step with 33 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {}] Step with 26 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 26[(-49+i13^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}] Step with 25 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}] Step with 36 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 36[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {}] Step with 23 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 36[T], 23[(-49+i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {22[T]}, {}] Accelerate Start location: l14 Program variables: i11^0 i13^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0 21: l0 -> l1 : T, cost: 1 40: l0 -> l0 : i7^0'=i7^0+n, (50-i7^0-n >= 0 /\ -1+n >= 0), cost: 1 37: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1 38: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 22: l2 -> l3 : 50-i^0 <= 0, cost: 1 23: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l4 -> l2 : T, cost: 1 45: l4 -> l4 : i^0'=n6+i^0, (-1+n6 >= 0 /\ 50-n6-i^0 >= 0), cost: 1 24: l5 -> l6 : T, cost: 1 41: l5 -> l5 : i9^0'=i9^0+n2, (50-i9^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 34: l6 -> l9 : i^0'=0, 50-i9^0 <= 0, cost: 1 35: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 25: l7 -> l4 : i^0'=0, 50-i13^0 <= 0, cost: 1 26: l7 -> l8 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 33: l8 -> l7 : T, cost: 1 44: l8 -> l8 : i13^0'=n5+i13^0, (50-n5-i13^0 >= 0 /\ -1+n5 >= 0), cost: 1 27: l9 -> l10 : T, cost: 1 42: l9 -> l9 : i^0'=n3+i^0, (-1+n3 >= 0 /\ 50-n3-i^0 >= 0), cost: 1 31: l10 -> l12 : i11^0'=0, 50-i^0 <= 0, cost: 1 32: l10 -> l9 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 28: l11 -> l8 : i13^0'=0, 50-i11^0 <= 0, cost: 1 29: l11 -> l12 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 30: l12 -> l11 : T, cost: 1 43: l12 -> l12 : i11^0'=n4+i11^0, (50-n4-i11^0 >= 0 /\ -1+n4 >= 0), cost: 1 39: l14 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, T, cost: 1 Loop Acceleration Original rule: l4 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 New rule: l4 -> l4 : i^0'=n6+i^0, (-1+n6 >= 0 /\ 50-n6-i^0 >= 0), cost: 1 49-i^0 >= 0 [0]: montonic decrease yields 50-n6-i^0 >= 0 49-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i^0 >= 0) Replacement map: {49-i^0 >= 0 -> 50-n6-i^0 >= 0} Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 45[(-1+n6 >= 0 /\ 50-n6-i^0 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {45[T]}] Step with 36 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 45[(-1+n6 >= 0 /\ 50-n6-i^0 >= 0)], 36[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {45[T]}, {}] Step with 23 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 45[(-1+n6 >= 0 /\ 50-n6-i^0 >= 0)], 36[T], 23[(-49+i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {45[T]}, {}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 45[(-1+n6 >= 0 /\ 50-n6-i^0 >= 0)], 36[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {45[T]}, {23[T]}] Step with 22 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 45[(-1+n6 >= 0 /\ 50-n6-i^0 >= 0)], 36[T], 22[(50-i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {45[T]}, {23[T]}, {}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 45[(-1+n6 >= 0 /\ 50-n6-i^0 >= 0)], 36[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {45[T]}, {22[T], 23[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 45[(-1+n6 >= 0 /\ 50-n6-i^0 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {}, {36[T], 45[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {45[T]}] Step with 36 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 36[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {45[T]}, {}] Step with 23 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 36[T], 23[(-49+i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {45[T]}, {22[T]}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)], 36[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {45[T]}, {22[T], 23[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T], 25[(50-i13^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {26[T]}, {36[T], 45[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)], 33[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {44[T]}, {25[T], 26[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 44[(50-n5-i13^0 >= 0 /\ -1+n5 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {}, {33[T], 44[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {44[T]}] Step with 33 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 33[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {44[T]}, {}] Step with 26 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 33[T], 26[(-49+i13^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {44[T]}, {25[T]}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)], 33[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {44[T]}, {25[T], 26[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T], 28[(50-i11^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {29[T]}, {33[T], 44[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)], 30[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {43[T]}, {28[T], 29[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 43[(50-n4-i11^0 >= 0 /\ -1+n4 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {}, {30[T], 43[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {43[T]}] Step with 30 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 30[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {43[T]}, {}] Step with 29 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 30[T], 29[(-49+i11^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {43[T]}, {28[T]}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)], 30[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {43[T]}, {28[T], 29[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T], 31[(50-i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {32[T]}, {30[T], 43[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)], 27[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {42[T]}, {31[T], 32[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 42[(-1+n3 >= 0 /\ 50-n3-i^0 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {}, {27[T], 42[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {42[T]}] Step with 27 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 27[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {42[T]}, {}] Step with 32 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 27[T], 32[(-49+i^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {42[T]}, {31[T]}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)], 27[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {42[T]}, {31[T], 32[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 34[(50-i9^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {35[T]}, {27[T], 42[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {41[T]}, {34[T], 35[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 41[(50-i9^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {}, {24[T], 41[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {41[T]}] Step with 24 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 24[T] Blocked [{}, {}, {40[T]}, {38[T]}, {41[T]}, {}] Step with 35 Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 24[T], 35[(-49+i9^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {41[T]}, {34[T]}, {}] Covered Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)], 24[T] Blocked [{}, {}, {40[T]}, {38[T]}, {41[T]}, {34[T], 35[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T], 37[(50-i7^0 <= 0)] Blocked [{}, {}, {40[T]}, {38[T]}, {24[T], 41[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)], 21[T] Blocked [{}, {}, {40[T]}, {37[T], 38[T]}] Backtrack Trace 39[T], 40[(50-i7^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {21[T], 40[T]}] Backtrack Trace 39[T] Blocked [{}, {40[T]}] Step with 21 Trace 39[T], 21[T] Blocked [{}, {40[T]}, {}] Step with 38 Trace 39[T], 21[T], 38[(-49+i7^0 <= 0)] Blocked [{}, {40[T]}, {37[T]}, {}] Covered Trace 39[T], 21[T] Blocked [{}, {40[T]}, {37[T], 38[T]}] Backtrack Trace 39[T] Blocked [{}, {21[T], 40[T]}] Backtrack Trace Blocked [{39[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b