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