WORST_CASE(Omega(0),?) Initial ITS Start location: l18 0: l0 -> l1 : i17^0'=i17^post0, i11^0'=i11^post0, tmp___0^0'=tmp___0^post0, i9^0'=i9^post0, i15^0'=i15^post0, arraySize^0'=arraySize^post0, tmp^0'=tmp^post0, i7^0'=i7^post0, i13^0'=i13^post0, i^0'=i^post0, (-i9^post0+i9^0 == 0 /\ i11^0-i11^post0 == 0 /\ arraySize^0-arraySize^post0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -i7^post0+i7^0 == 0 /\ -i^post0+i^0 == 0 /\ i17^0-i17^post0 == 0 /\ -i13^post0+i13^0 == 0 /\ -i15^post0+i15^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0), cost: 1 22: l1 -> l5 : i17^0'=i17^post22, i11^0'=i11^post22, tmp___0^0'=tmp___0^post22, i9^0'=i9^post22, i15^0'=i15^post22, arraySize^0'=arraySize^post22, tmp^0'=tmp^post22, i7^0'=i7^post22, i13^0'=i13^post22, i^0'=i^post22, (i15^0-i15^post22 == 0 /\ -tmp^post22+tmp^0 == 0 /\ i17^0-i17^post22 == 0 /\ -i^post22+i^0 == 0 /\ i9^post22 == 0 /\ -arraySize^post22+arraySize^0 == 0 /\ -i13^post22+i13^0 == 0 /\ i9^10 == 0 /\ tmp___0^0-tmp___0^post22 == 0 /\ i11^0-i11^post22 == 0 /\ arraySize^0-i7^0 <= 0 /\ -i7^post22+i7^0 == 0), cost: 1 23: l1 -> l0 : i17^0'=i17^post23, i11^0'=i11^post23, tmp___0^0'=tmp___0^post23, i9^0'=i9^post23, i15^0'=i15^post23, arraySize^0'=arraySize^post23, tmp^0'=tmp^post23, i7^0'=i7^post23, i13^0'=i13^post23, i^0'=i^post23, (-tmp^post23+tmp^0 == 0 /\ -i11^post23+i11^0 == 0 /\ i13^0-i13^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -1+i7^post23-i7^0 == 0 /\ -arraySize^post23+arraySize^0 == 0 /\ 1-arraySize^0+i7^0 <= 0 /\ i15^0-i15^post23 == 0 /\ i9^0-i9^post23 == 0 /\ -i^post23+i^0 == 0 /\ i17^0-i17^post23 == 0), cost: 1 1: l2 -> l3 : i17^0'=i17^post1, i11^0'=i11^post1, tmp___0^0'=tmp___0^post1, i9^0'=i9^post1, i15^0'=i15^post1, arraySize^0'=arraySize^post1, tmp^0'=tmp^post1, i7^0'=i7^post1, i13^0'=i13^post1, i^0'=i^post1, (tmp^0-tmp^post1 == 0 /\ -i15^post1+i15^0 == 0 /\ arraySize^0-i^0 <= 0 /\ -i^post1+i^0 == 0 /\ i11^0-i11^post1 == 0 /\ -i9^post1+i9^0 == 0 /\ arraySize^0-arraySize^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -i7^post1+i7^0 == 0 /\ i17^0-i17^post1 == 0 /\ -i13^post1+i13^0 == 0), cost: 1 2: l2 -> l4 : i17^0'=i17^post2, i11^0'=i11^post2, tmp___0^0'=tmp___0^post2, i9^0'=i9^post2, i15^0'=i15^post2, arraySize^0'=arraySize^post2, tmp^0'=tmp^post2, i7^0'=i7^post2, i13^0'=i13^post2, i^0'=i^post2, (1-arraySize^0+i^0 <= 0 /\ tmp^0-tmp^post2 == 0 /\ -i15^post2+i15^0 == 0 /\ -i9^post2+i9^0 == 0 /\ arraySize^0-arraySize^post2 == 0 /\ i11^0-i11^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -i7^post2+i7^0 == 0 /\ -1+i^post2-i^0 == 0 /\ i17^0-i17^post2 == 0 /\ -i13^post2+i13^0 == 0), cost: 1 21: l4 -> l2 : i17^0'=i17^post21, i11^0'=i11^post21, tmp___0^0'=tmp___0^post21, i9^0'=i9^post21, i15^0'=i15^post21, arraySize^0'=arraySize^post21, tmp^0'=tmp^post21, i7^0'=i7^post21, i13^0'=i13^post21, i^0'=i^post21, (i13^0-i13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -i^post21+i^0 == 0 /\ -arraySize^post21+arraySize^0 == 0 /\ i9^0-i9^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ i15^0-i15^post21 == 0 /\ -i11^post21+i11^0 == 0 /\ i17^0-i17^post21 == 0 /\ -i7^post21+i7^0 == 0), cost: 1 3: l5 -> l6 : i17^0'=i17^post3, i11^0'=i11^post3, tmp___0^0'=tmp___0^post3, i9^0'=i9^post3, i15^0'=i15^post3, arraySize^0'=arraySize^post3, tmp^0'=tmp^post3, i7^0'=i7^post3, i13^0'=i13^post3, i^0'=i^post3, (i17^0-i17^post3 == 0 /\ i11^0-i11^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -arraySize^post3+arraySize^0 == 0 /\ i7^0-i7^post3 == 0 /\ -i13^post3+i13^0 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ i15^0-i15^post3 == 0 /\ i9^0-i9^post3 == 0 /\ -i^post3+i^0 == 0), cost: 1 19: l6 -> l9 : i17^0'=i17^post19, i11^0'=i11^post19, tmp___0^0'=tmp___0^post19, i9^0'=i9^post19, i15^0'=i15^post19, arraySize^0'=arraySize^post19, tmp^0'=tmp^post19, i7^0'=i7^post19, i13^0'=i13^post19, i^0'=i^post19, (-i^post19+i^0 == 0 /\ i15^0-i15^post19 == 0 /\ i9^0-i9^post19 == 0 /\ -i13^post19+i13^0 == 0 /\ -tmp^post19+tmp^0 == 0 /\ i11^10 == 0 /\ -i9^0+arraySize^0 <= 0 /\ -arraySize^post19+arraySize^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ i7^0-i7^post19 == 0 /\ i11^post19 == 0 /\ i17^0-i17^post19 == 0), cost: 1 20: l6 -> l5 : i17^0'=i17^post20, i11^0'=i11^post20, tmp___0^0'=tmp___0^post20, i9^0'=i9^post20, i15^0'=i15^post20, arraySize^0'=arraySize^post20, tmp^0'=tmp^post20, i7^0'=i7^post20, i13^0'=i13^post20, i^0'=i^post20, (-arraySize^post20+arraySize^0 == 0 /\ 1+i9^0-arraySize^0 <= 0 /\ i15^0-i15^post20 == 0 /\ -i^post20+i^0 == 0 /\ -i13^post20+i13^0 == 0 /\ i17^0-i17^post20 == 0 /\ i11^0-i11^post20 == 0 /\ -1-i9^0+i9^post20 == 0 /\ i7^0-i7^post20 == 0 /\ -tmp^post20+tmp^0 == 0 /\ tmp___0^0-tmp___0^post20 == 0), cost: 1 4: l7 -> l4 : i17^0'=i17^post4, i11^0'=i11^post4, tmp___0^0'=tmp___0^post4, i9^0'=i9^post4, i15^0'=i15^post4, arraySize^0'=arraySize^post4, tmp^0'=tmp^post4, i7^0'=i7^post4, i13^0'=i13^post4, i^0'=i^post4, (-tmp^post4+tmp^0 == 0 /\ i15^0-i15^post4 == 0 /\ i9^0-i9^post4 == 0 /\ i^post4 == 0 /\ -arraySize^post4+arraySize^0 == 0 /\ -i13^post4+i13^0 == 0 /\ i7^0-i7^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -i17^post4+i17^0 == 0 /\ i11^0-i11^post4 == 0 /\ -i17^0+arraySize^0 <= 0), cost: 1 5: l7 -> l8 : i17^0'=i17^post5, i11^0'=i11^post5, tmp___0^0'=tmp___0^post5, i9^0'=i9^post5, i15^0'=i15^post5, arraySize^0'=arraySize^post5, tmp^0'=tmp^post5, i7^0'=i7^post5, i13^0'=i13^post5, i^0'=i^post5, (-tmp^post5+tmp^0 == 0 /\ i9^0-i9^post5 == 0 /\ i15^0-i15^post5 == 0 /\ -arraySize^post5+arraySize^0 == 0 /\ -i13^post5+i13^0 == 0 /\ 1+i17^0-arraySize^0 <= 0 /\ i7^0-i7^post5 == 0 /\ -1-i17^0+i17^post5 == 0 /\ -i^post5+i^0 == 0 /\ i11^0-i11^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0), cost: 1 18: l8 -> l7 : i17^0'=i17^post18, i11^0'=i11^post18, tmp___0^0'=tmp___0^post18, i9^0'=i9^post18, i15^0'=i15^post18, arraySize^0'=arraySize^post18, tmp^0'=tmp^post18, i7^0'=i7^post18, i13^0'=i13^post18, i^0'=i^post18, (i17^0-i17^post18 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ -i13^post18+i13^0 == 0 /\ i7^0-i7^post18 == 0 /\ -arraySize^post18+arraySize^0 == 0 /\ i11^0-i11^post18 == 0 /\ -tmp^post18+tmp^0 == 0 /\ i15^0-i15^post18 == 0 /\ i9^0-i9^post18 == 0 /\ -i^post18+i^0 == 0), cost: 1 6: l9 -> l10 : i17^0'=i17^post6, i11^0'=i11^post6, tmp___0^0'=tmp___0^post6, i9^0'=i9^post6, i15^0'=i15^post6, arraySize^0'=arraySize^post6, tmp^0'=tmp^post6, i7^0'=i7^post6, i13^0'=i13^post6, i^0'=i^post6, (i15^0-i15^post6 == 0 /\ -i13^post6+i13^0 == 0 /\ i9^0-i9^post6 == 0 /\ i17^0-i17^post6 == 0 /\ -i11^post6+i11^0 == 0 /\ -i7^post6+i7^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -arraySize^post6+arraySize^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -i^post6+i^0 == 0), cost: 1 16: l10 -> l13 : i17^0'=i17^post16, i11^0'=i11^post16, tmp___0^0'=tmp___0^post16, i9^0'=i9^post16, i15^0'=i15^post16, arraySize^0'=arraySize^post16, tmp^0'=tmp^post16, i7^0'=i7^post16, i13^0'=i13^post16, i^0'=i^post16, (i17^0-i17^post16 == 0 /\ i^post16 == 0 /\ -i15^post16+i15^0 == 0 /\ i11^0-i11^post16 == 0 /\ arraySize^0-arraySize^post16 == 0 /\ -i11^0+arraySize^0 <= 0 /\ -i13^post16+i13^0 == 0 /\ i9^0-i9^post16 == 0 /\ -i7^post16+i7^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -tmp^post16+tmp^0 == 0), cost: 1 17: l10 -> l9 : i17^0'=i17^post17, i11^0'=i11^post17, tmp___0^0'=tmp___0^post17, i9^0'=i9^post17, i15^0'=i15^post17, arraySize^0'=arraySize^post17, tmp^0'=tmp^post17, i7^0'=i7^post17, i13^0'=i13^post17, i^0'=i^post17, (tmp^0-tmp^post17 == 0 /\ -i15^post17+i15^0 == 0 /\ 1+i11^0-arraySize^0 <= 0 /\ arraySize^0-arraySize^post17 == 0 /\ -i9^post17+i9^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ -i^post17+i^0 == 0 /\ i17^0-i17^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ -i13^post17+i13^0 == 0 /\ -1-i11^0+i11^post17 == 0), cost: 1 7: l11 -> l8 : i17^0'=i17^post7, i11^0'=i11^post7, tmp___0^0'=tmp___0^post7, i9^0'=i9^post7, i15^0'=i15^post7, arraySize^0'=arraySize^post7, tmp^0'=tmp^post7, i7^0'=i7^post7, i13^0'=i13^post7, i^0'=i^post7, (-i13^post7+i13^0 == 0 /\ i9^0-i9^post7 == 0 /\ i17^10 == 0 /\ -i^post7+i^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -i15^0+arraySize^0 <= 0 /\ i11^0-i11^post7 == 0 /\ -arraySize^post7+arraySize^0 == 0 /\ i15^0-i15^post7 == 0 /\ -i7^post7+i7^0 == 0 /\ i17^post7 == 0), cost: 1 8: l11 -> l12 : i17^0'=i17^post8, i11^0'=i11^post8, tmp___0^0'=tmp___0^post8, i9^0'=i9^post8, i15^0'=i15^post8, arraySize^0'=arraySize^post8, tmp^0'=tmp^post8, i7^0'=i7^post8, i13^0'=i13^post8, i^0'=i^post8, (1+i15^0-arraySize^0 <= 0 /\ -arraySize^post8+arraySize^0 == 0 /\ -i13^post8+i13^0 == 0 /\ i9^0-i9^post8 == 0 /\ -i^post8+i^0 == 0 /\ i17^0-i17^post8 == 0 /\ -1-i15^0+i15^post8 == 0 /\ -i11^post8+i11^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ -tmp^post8+tmp^0 == 0 /\ i7^0-i7^post8 == 0), cost: 1 15: l12 -> l11 : i17^0'=i17^post15, i11^0'=i11^post15, tmp___0^0'=tmp___0^post15, i9^0'=i9^post15, i15^0'=i15^post15, arraySize^0'=arraySize^post15, tmp^0'=tmp^post15, i7^0'=i7^post15, i13^0'=i13^post15, i^0'=i^post15, (i11^0-i11^post15 == 0 /\ arraySize^0-arraySize^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ -i13^post15+i13^0 == 0 /\ i17^0-i17^post15 == 0 /\ -i7^post15+i7^0 == 0 /\ -i9^post15+i9^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ -i^post15+i^0 == 0), cost: 1 9: l13 -> l14 : i17^0'=i17^post9, i11^0'=i11^post9, tmp___0^0'=tmp___0^post9, i9^0'=i9^post9, i15^0'=i15^post9, arraySize^0'=arraySize^post9, tmp^0'=tmp^post9, i7^0'=i7^post9, i13^0'=i13^post9, i^0'=i^post9, (-i7^post9+i7^0 == 0 /\ -i^post9+i^0 == 0 /\ i13^0-i13^post9 == 0 /\ -arraySize^post9+arraySize^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ i15^0-i15^post9 == 0 /\ i9^0-i9^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ i17^0-i17^post9 == 0 /\ -i11^post9+i11^0 == 0), cost: 1 13: l14 -> l16 : i17^0'=i17^post13, i11^0'=i11^post13, tmp___0^0'=tmp___0^post13, i9^0'=i9^post13, i15^0'=i15^post13, arraySize^0'=arraySize^post13, tmp^0'=tmp^post13, i7^0'=i7^post13, i13^0'=i13^post13, i^0'=i^post13, (arraySize^0-i^0 <= 0 /\ -tmp^post13+tmp^0 == 0 /\ i15^0-i15^post13 == 0 /\ -i^post13+i^0 == 0 /\ i13^10 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ i9^0-i9^post13 == 0 /\ -i7^post13+i7^0 == 0 /\ -arraySize^post13+arraySize^0 == 0 /\ i13^post13 == 0 /\ -i11^post13+i11^0 == 0 /\ i17^0-i17^post13 == 0), cost: 1 14: l14 -> l13 : i17^0'=i17^post14, i11^0'=i11^post14, tmp___0^0'=tmp___0^post14, i9^0'=i9^post14, i15^0'=i15^post14, arraySize^0'=arraySize^post14, tmp^0'=tmp^post14, i7^0'=i7^post14, i13^0'=i13^post14, i^0'=i^post14, (-i15^post14+i15^0 == 0 /\ 1-arraySize^0+i^0 <= 0 /\ i17^0-i17^post14 == 0 /\ -i9^post14+i9^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ -1+i^post14-i^0 == 0 /\ -i7^post14+i7^0 == 0 /\ -i13^post14+i13^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ i11^0-i11^post14 == 0 /\ arraySize^0-arraySize^post14 == 0), cost: 1 10: l15 -> l12 : i17^0'=i17^post10, i11^0'=i11^post10, tmp___0^0'=tmp___0^post10, i9^0'=i9^post10, i15^0'=i15^post10, arraySize^0'=arraySize^post10, tmp^0'=tmp^post10, i7^0'=i7^post10, i13^0'=i13^post10, i^0'=i^post10, (-arraySize^post10+arraySize^0 == 0 /\ -i7^post10+i7^0 == 0 /\ -tmp^post10+tmp^0 == 0 /\ arraySize^0-i13^0 <= 0 /\ i9^0-i9^post10 == 0 /\ -i^post10+i^0 == 0 /\ i17^0-i17^post10 == 0 /\ i15^post10 == 0 /\ i15^10 == 0 /\ -i13^post10+i13^0 == 0 /\ i11^0-i11^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0), cost: 1 11: l15 -> l16 : i17^0'=i17^post11, i11^0'=i11^post11, tmp___0^0'=tmp___0^post11, i9^0'=i9^post11, i15^0'=i15^post11, arraySize^0'=arraySize^post11, tmp^0'=tmp^post11, i7^0'=i7^post11, i13^0'=i13^post11, i^0'=i^post11, (-i7^post11+i7^0 == 0 /\ -arraySize^post11+arraySize^0 == 0 /\ i17^0-i17^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ i11^0-i11^post11 == 0 /\ 1-arraySize^0+i13^0 <= 0 /\ i15^0-i15^post11 == 0 /\ -i^post11+i^0 == 0 /\ i9^0-i9^post11 == 0 /\ -1-i13^0+i13^post11 == 0 /\ -tmp^post11+tmp^0 == 0), cost: 1 12: l16 -> l15 : i17^0'=i17^post12, i11^0'=i11^post12, tmp___0^0'=tmp___0^post12, i9^0'=i9^post12, i15^0'=i15^post12, arraySize^0'=arraySize^post12, tmp^0'=tmp^post12, i7^0'=i7^post12, i13^0'=i13^post12, i^0'=i^post12, (-i15^post12+i15^0 == 0 /\ i17^0-i17^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i13^post12+i13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ i11^0-i11^post12 == 0 /\ -i^post12+i^0 == 0 /\ -i7^post12+i7^0 == 0 /\ i9^0-i9^post12 == 0 /\ arraySize^0-arraySize^post12 == 0), cost: 1 24: l17 -> l0 : i17^0'=i17^post24, i11^0'=i11^post24, tmp___0^0'=tmp___0^post24, i9^0'=i9^post24, i15^0'=i15^post24, arraySize^0'=arraySize^post24, tmp^0'=tmp^post24, i7^0'=i7^post24, i13^0'=i13^post24, i^0'=i^post24, (0 == 0 /\ i15^0-i15^post24 == 0 /\ i7^post24 == 0 /\ i17^0-i17^post24 == 0 /\ i^post24 == 0 /\ i9^0-i9^post24 == 0 /\ -i13^post24+i13^0 == 0 /\ i11^0-i11^post24 == 0 /\ i7^10 == 0 /\ -arraySize^post24+arraySize^0 == 0), cost: 1 25: l18 -> l17 : i17^0'=i17^post25, i11^0'=i11^post25, tmp___0^0'=tmp___0^post25, i9^0'=i9^post25, i15^0'=i15^post25, arraySize^0'=arraySize^post25, tmp^0'=tmp^post25, i7^0'=i7^post25, i13^0'=i13^post25, i^0'=i^post25, (-i15^post25+i15^0 == 0 /\ i17^0-i17^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i7^post25+i7^0 == 0 /\ -i^post25+i^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ -arraySize^post25+arraySize^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ -i13^post25+i13^0 == 0 /\ i11^0-i11^post25 == 0), cost: 1 Removed unreachable rules and leafs Start location: l18 0: l0 -> l1 : i17^0'=i17^post0, i11^0'=i11^post0, tmp___0^0'=tmp___0^post0, i9^0'=i9^post0, i15^0'=i15^post0, arraySize^0'=arraySize^post0, tmp^0'=tmp^post0, i7^0'=i7^post0, i13^0'=i13^post0, i^0'=i^post0, (-i9^post0+i9^0 == 0 /\ i11^0-i11^post0 == 0 /\ arraySize^0-arraySize^post0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -i7^post0+i7^0 == 0 /\ -i^post0+i^0 == 0 /\ i17^0-i17^post0 == 0 /\ -i13^post0+i13^0 == 0 /\ -i15^post0+i15^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0), cost: 1 22: l1 -> l5 : i17^0'=i17^post22, i11^0'=i11^post22, tmp___0^0'=tmp___0^post22, i9^0'=i9^post22, i15^0'=i15^post22, arraySize^0'=arraySize^post22, tmp^0'=tmp^post22, i7^0'=i7^post22, i13^0'=i13^post22, i^0'=i^post22, (i15^0-i15^post22 == 0 /\ -tmp^post22+tmp^0 == 0 /\ i17^0-i17^post22 == 0 /\ -i^post22+i^0 == 0 /\ i9^post22 == 0 /\ -arraySize^post22+arraySize^0 == 0 /\ -i13^post22+i13^0 == 0 /\ i9^10 == 0 /\ tmp___0^0-tmp___0^post22 == 0 /\ i11^0-i11^post22 == 0 /\ arraySize^0-i7^0 <= 0 /\ -i7^post22+i7^0 == 0), cost: 1 23: l1 -> l0 : i17^0'=i17^post23, i11^0'=i11^post23, tmp___0^0'=tmp___0^post23, i9^0'=i9^post23, i15^0'=i15^post23, arraySize^0'=arraySize^post23, tmp^0'=tmp^post23, i7^0'=i7^post23, i13^0'=i13^post23, i^0'=i^post23, (-tmp^post23+tmp^0 == 0 /\ -i11^post23+i11^0 == 0 /\ i13^0-i13^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -1+i7^post23-i7^0 == 0 /\ -arraySize^post23+arraySize^0 == 0 /\ 1-arraySize^0+i7^0 <= 0 /\ i15^0-i15^post23 == 0 /\ i9^0-i9^post23 == 0 /\ -i^post23+i^0 == 0 /\ i17^0-i17^post23 == 0), cost: 1 2: l2 -> l4 : i17^0'=i17^post2, i11^0'=i11^post2, tmp___0^0'=tmp___0^post2, i9^0'=i9^post2, i15^0'=i15^post2, arraySize^0'=arraySize^post2, tmp^0'=tmp^post2, i7^0'=i7^post2, i13^0'=i13^post2, i^0'=i^post2, (1-arraySize^0+i^0 <= 0 /\ tmp^0-tmp^post2 == 0 /\ -i15^post2+i15^0 == 0 /\ -i9^post2+i9^0 == 0 /\ arraySize^0-arraySize^post2 == 0 /\ i11^0-i11^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -i7^post2+i7^0 == 0 /\ -1+i^post2-i^0 == 0 /\ i17^0-i17^post2 == 0 /\ -i13^post2+i13^0 == 0), cost: 1 21: l4 -> l2 : i17^0'=i17^post21, i11^0'=i11^post21, tmp___0^0'=tmp___0^post21, i9^0'=i9^post21, i15^0'=i15^post21, arraySize^0'=arraySize^post21, tmp^0'=tmp^post21, i7^0'=i7^post21, i13^0'=i13^post21, i^0'=i^post21, (i13^0-i13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -i^post21+i^0 == 0 /\ -arraySize^post21+arraySize^0 == 0 /\ i9^0-i9^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ i15^0-i15^post21 == 0 /\ -i11^post21+i11^0 == 0 /\ i17^0-i17^post21 == 0 /\ -i7^post21+i7^0 == 0), cost: 1 3: l5 -> l6 : i17^0'=i17^post3, i11^0'=i11^post3, tmp___0^0'=tmp___0^post3, i9^0'=i9^post3, i15^0'=i15^post3, arraySize^0'=arraySize^post3, tmp^0'=tmp^post3, i7^0'=i7^post3, i13^0'=i13^post3, i^0'=i^post3, (i17^0-i17^post3 == 0 /\ i11^0-i11^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -arraySize^post3+arraySize^0 == 0 /\ i7^0-i7^post3 == 0 /\ -i13^post3+i13^0 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ i15^0-i15^post3 == 0 /\ i9^0-i9^post3 == 0 /\ -i^post3+i^0 == 0), cost: 1 19: l6 -> l9 : i17^0'=i17^post19, i11^0'=i11^post19, tmp___0^0'=tmp___0^post19, i9^0'=i9^post19, i15^0'=i15^post19, arraySize^0'=arraySize^post19, tmp^0'=tmp^post19, i7^0'=i7^post19, i13^0'=i13^post19, i^0'=i^post19, (-i^post19+i^0 == 0 /\ i15^0-i15^post19 == 0 /\ i9^0-i9^post19 == 0 /\ -i13^post19+i13^0 == 0 /\ -tmp^post19+tmp^0 == 0 /\ i11^10 == 0 /\ -i9^0+arraySize^0 <= 0 /\ -arraySize^post19+arraySize^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ i7^0-i7^post19 == 0 /\ i11^post19 == 0 /\ i17^0-i17^post19 == 0), cost: 1 20: l6 -> l5 : i17^0'=i17^post20, i11^0'=i11^post20, tmp___0^0'=tmp___0^post20, i9^0'=i9^post20, i15^0'=i15^post20, arraySize^0'=arraySize^post20, tmp^0'=tmp^post20, i7^0'=i7^post20, i13^0'=i13^post20, i^0'=i^post20, (-arraySize^post20+arraySize^0 == 0 /\ 1+i9^0-arraySize^0 <= 0 /\ i15^0-i15^post20 == 0 /\ -i^post20+i^0 == 0 /\ -i13^post20+i13^0 == 0 /\ i17^0-i17^post20 == 0 /\ i11^0-i11^post20 == 0 /\ -1-i9^0+i9^post20 == 0 /\ i7^0-i7^post20 == 0 /\ -tmp^post20+tmp^0 == 0 /\ tmp___0^0-tmp___0^post20 == 0), cost: 1 4: l7 -> l4 : i17^0'=i17^post4, i11^0'=i11^post4, tmp___0^0'=tmp___0^post4, i9^0'=i9^post4, i15^0'=i15^post4, arraySize^0'=arraySize^post4, tmp^0'=tmp^post4, i7^0'=i7^post4, i13^0'=i13^post4, i^0'=i^post4, (-tmp^post4+tmp^0 == 0 /\ i15^0-i15^post4 == 0 /\ i9^0-i9^post4 == 0 /\ i^post4 == 0 /\ -arraySize^post4+arraySize^0 == 0 /\ -i13^post4+i13^0 == 0 /\ i7^0-i7^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -i17^post4+i17^0 == 0 /\ i11^0-i11^post4 == 0 /\ -i17^0+arraySize^0 <= 0), cost: 1 5: l7 -> l8 : i17^0'=i17^post5, i11^0'=i11^post5, tmp___0^0'=tmp___0^post5, i9^0'=i9^post5, i15^0'=i15^post5, arraySize^0'=arraySize^post5, tmp^0'=tmp^post5, i7^0'=i7^post5, i13^0'=i13^post5, i^0'=i^post5, (-tmp^post5+tmp^0 == 0 /\ i9^0-i9^post5 == 0 /\ i15^0-i15^post5 == 0 /\ -arraySize^post5+arraySize^0 == 0 /\ -i13^post5+i13^0 == 0 /\ 1+i17^0-arraySize^0 <= 0 /\ i7^0-i7^post5 == 0 /\ -1-i17^0+i17^post5 == 0 /\ -i^post5+i^0 == 0 /\ i11^0-i11^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0), cost: 1 18: l8 -> l7 : i17^0'=i17^post18, i11^0'=i11^post18, tmp___0^0'=tmp___0^post18, i9^0'=i9^post18, i15^0'=i15^post18, arraySize^0'=arraySize^post18, tmp^0'=tmp^post18, i7^0'=i7^post18, i13^0'=i13^post18, i^0'=i^post18, (i17^0-i17^post18 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ -i13^post18+i13^0 == 0 /\ i7^0-i7^post18 == 0 /\ -arraySize^post18+arraySize^0 == 0 /\ i11^0-i11^post18 == 0 /\ -tmp^post18+tmp^0 == 0 /\ i15^0-i15^post18 == 0 /\ i9^0-i9^post18 == 0 /\ -i^post18+i^0 == 0), cost: 1 6: l9 -> l10 : i17^0'=i17^post6, i11^0'=i11^post6, tmp___0^0'=tmp___0^post6, i9^0'=i9^post6, i15^0'=i15^post6, arraySize^0'=arraySize^post6, tmp^0'=tmp^post6, i7^0'=i7^post6, i13^0'=i13^post6, i^0'=i^post6, (i15^0-i15^post6 == 0 /\ -i13^post6+i13^0 == 0 /\ i9^0-i9^post6 == 0 /\ i17^0-i17^post6 == 0 /\ -i11^post6+i11^0 == 0 /\ -i7^post6+i7^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -arraySize^post6+arraySize^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -i^post6+i^0 == 0), cost: 1 16: l10 -> l13 : i17^0'=i17^post16, i11^0'=i11^post16, tmp___0^0'=tmp___0^post16, i9^0'=i9^post16, i15^0'=i15^post16, arraySize^0'=arraySize^post16, tmp^0'=tmp^post16, i7^0'=i7^post16, i13^0'=i13^post16, i^0'=i^post16, (i17^0-i17^post16 == 0 /\ i^post16 == 0 /\ -i15^post16+i15^0 == 0 /\ i11^0-i11^post16 == 0 /\ arraySize^0-arraySize^post16 == 0 /\ -i11^0+arraySize^0 <= 0 /\ -i13^post16+i13^0 == 0 /\ i9^0-i9^post16 == 0 /\ -i7^post16+i7^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -tmp^post16+tmp^0 == 0), cost: 1 17: l10 -> l9 : i17^0'=i17^post17, i11^0'=i11^post17, tmp___0^0'=tmp___0^post17, i9^0'=i9^post17, i15^0'=i15^post17, arraySize^0'=arraySize^post17, tmp^0'=tmp^post17, i7^0'=i7^post17, i13^0'=i13^post17, i^0'=i^post17, (tmp^0-tmp^post17 == 0 /\ -i15^post17+i15^0 == 0 /\ 1+i11^0-arraySize^0 <= 0 /\ arraySize^0-arraySize^post17 == 0 /\ -i9^post17+i9^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ -i^post17+i^0 == 0 /\ i17^0-i17^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ -i13^post17+i13^0 == 0 /\ -1-i11^0+i11^post17 == 0), cost: 1 7: l11 -> l8 : i17^0'=i17^post7, i11^0'=i11^post7, tmp___0^0'=tmp___0^post7, i9^0'=i9^post7, i15^0'=i15^post7, arraySize^0'=arraySize^post7, tmp^0'=tmp^post7, i7^0'=i7^post7, i13^0'=i13^post7, i^0'=i^post7, (-i13^post7+i13^0 == 0 /\ i9^0-i9^post7 == 0 /\ i17^10 == 0 /\ -i^post7+i^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -i15^0+arraySize^0 <= 0 /\ i11^0-i11^post7 == 0 /\ -arraySize^post7+arraySize^0 == 0 /\ i15^0-i15^post7 == 0 /\ -i7^post7+i7^0 == 0 /\ i17^post7 == 0), cost: 1 8: l11 -> l12 : i17^0'=i17^post8, i11^0'=i11^post8, tmp___0^0'=tmp___0^post8, i9^0'=i9^post8, i15^0'=i15^post8, arraySize^0'=arraySize^post8, tmp^0'=tmp^post8, i7^0'=i7^post8, i13^0'=i13^post8, i^0'=i^post8, (1+i15^0-arraySize^0 <= 0 /\ -arraySize^post8+arraySize^0 == 0 /\ -i13^post8+i13^0 == 0 /\ i9^0-i9^post8 == 0 /\ -i^post8+i^0 == 0 /\ i17^0-i17^post8 == 0 /\ -1-i15^0+i15^post8 == 0 /\ -i11^post8+i11^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ -tmp^post8+tmp^0 == 0 /\ i7^0-i7^post8 == 0), cost: 1 15: l12 -> l11 : i17^0'=i17^post15, i11^0'=i11^post15, tmp___0^0'=tmp___0^post15, i9^0'=i9^post15, i15^0'=i15^post15, arraySize^0'=arraySize^post15, tmp^0'=tmp^post15, i7^0'=i7^post15, i13^0'=i13^post15, i^0'=i^post15, (i11^0-i11^post15 == 0 /\ arraySize^0-arraySize^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ -i13^post15+i13^0 == 0 /\ i17^0-i17^post15 == 0 /\ -i7^post15+i7^0 == 0 /\ -i9^post15+i9^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ -i^post15+i^0 == 0), cost: 1 9: l13 -> l14 : i17^0'=i17^post9, i11^0'=i11^post9, tmp___0^0'=tmp___0^post9, i9^0'=i9^post9, i15^0'=i15^post9, arraySize^0'=arraySize^post9, tmp^0'=tmp^post9, i7^0'=i7^post9, i13^0'=i13^post9, i^0'=i^post9, (-i7^post9+i7^0 == 0 /\ -i^post9+i^0 == 0 /\ i13^0-i13^post9 == 0 /\ -arraySize^post9+arraySize^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ i15^0-i15^post9 == 0 /\ i9^0-i9^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ i17^0-i17^post9 == 0 /\ -i11^post9+i11^0 == 0), cost: 1 13: l14 -> l16 : i17^0'=i17^post13, i11^0'=i11^post13, tmp___0^0'=tmp___0^post13, i9^0'=i9^post13, i15^0'=i15^post13, arraySize^0'=arraySize^post13, tmp^0'=tmp^post13, i7^0'=i7^post13, i13^0'=i13^post13, i^0'=i^post13, (arraySize^0-i^0 <= 0 /\ -tmp^post13+tmp^0 == 0 /\ i15^0-i15^post13 == 0 /\ -i^post13+i^0 == 0 /\ i13^10 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ i9^0-i9^post13 == 0 /\ -i7^post13+i7^0 == 0 /\ -arraySize^post13+arraySize^0 == 0 /\ i13^post13 == 0 /\ -i11^post13+i11^0 == 0 /\ i17^0-i17^post13 == 0), cost: 1 14: l14 -> l13 : i17^0'=i17^post14, i11^0'=i11^post14, tmp___0^0'=tmp___0^post14, i9^0'=i9^post14, i15^0'=i15^post14, arraySize^0'=arraySize^post14, tmp^0'=tmp^post14, i7^0'=i7^post14, i13^0'=i13^post14, i^0'=i^post14, (-i15^post14+i15^0 == 0 /\ 1-arraySize^0+i^0 <= 0 /\ i17^0-i17^post14 == 0 /\ -i9^post14+i9^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ -1+i^post14-i^0 == 0 /\ -i7^post14+i7^0 == 0 /\ -i13^post14+i13^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ i11^0-i11^post14 == 0 /\ arraySize^0-arraySize^post14 == 0), cost: 1 10: l15 -> l12 : i17^0'=i17^post10, i11^0'=i11^post10, tmp___0^0'=tmp___0^post10, i9^0'=i9^post10, i15^0'=i15^post10, arraySize^0'=arraySize^post10, tmp^0'=tmp^post10, i7^0'=i7^post10, i13^0'=i13^post10, i^0'=i^post10, (-arraySize^post10+arraySize^0 == 0 /\ -i7^post10+i7^0 == 0 /\ -tmp^post10+tmp^0 == 0 /\ arraySize^0-i13^0 <= 0 /\ i9^0-i9^post10 == 0 /\ -i^post10+i^0 == 0 /\ i17^0-i17^post10 == 0 /\ i15^post10 == 0 /\ i15^10 == 0 /\ -i13^post10+i13^0 == 0 /\ i11^0-i11^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0), cost: 1 11: l15 -> l16 : i17^0'=i17^post11, i11^0'=i11^post11, tmp___0^0'=tmp___0^post11, i9^0'=i9^post11, i15^0'=i15^post11, arraySize^0'=arraySize^post11, tmp^0'=tmp^post11, i7^0'=i7^post11, i13^0'=i13^post11, i^0'=i^post11, (-i7^post11+i7^0 == 0 /\ -arraySize^post11+arraySize^0 == 0 /\ i17^0-i17^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ i11^0-i11^post11 == 0 /\ 1-arraySize^0+i13^0 <= 0 /\ i15^0-i15^post11 == 0 /\ -i^post11+i^0 == 0 /\ i9^0-i9^post11 == 0 /\ -1-i13^0+i13^post11 == 0 /\ -tmp^post11+tmp^0 == 0), cost: 1 12: l16 -> l15 : i17^0'=i17^post12, i11^0'=i11^post12, tmp___0^0'=tmp___0^post12, i9^0'=i9^post12, i15^0'=i15^post12, arraySize^0'=arraySize^post12, tmp^0'=tmp^post12, i7^0'=i7^post12, i13^0'=i13^post12, i^0'=i^post12, (-i15^post12+i15^0 == 0 /\ i17^0-i17^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i13^post12+i13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ i11^0-i11^post12 == 0 /\ -i^post12+i^0 == 0 /\ -i7^post12+i7^0 == 0 /\ i9^0-i9^post12 == 0 /\ arraySize^0-arraySize^post12 == 0), cost: 1 24: l17 -> l0 : i17^0'=i17^post24, i11^0'=i11^post24, tmp___0^0'=tmp___0^post24, i9^0'=i9^post24, i15^0'=i15^post24, arraySize^0'=arraySize^post24, tmp^0'=tmp^post24, i7^0'=i7^post24, i13^0'=i13^post24, i^0'=i^post24, (0 == 0 /\ i15^0-i15^post24 == 0 /\ i7^post24 == 0 /\ i17^0-i17^post24 == 0 /\ i^post24 == 0 /\ i9^0-i9^post24 == 0 /\ -i13^post24+i13^0 == 0 /\ i11^0-i11^post24 == 0 /\ i7^10 == 0 /\ -arraySize^post24+arraySize^0 == 0), cost: 1 25: l18 -> l17 : i17^0'=i17^post25, i11^0'=i11^post25, tmp___0^0'=tmp___0^post25, i9^0'=i9^post25, i15^0'=i15^post25, arraySize^0'=arraySize^post25, tmp^0'=tmp^post25, i7^0'=i7^post25, i13^0'=i13^post25, i^0'=i^post25, (-i15^post25+i15^0 == 0 /\ i17^0-i17^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i7^post25+i7^0 == 0 /\ -i^post25+i^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ -arraySize^post25+arraySize^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ -i13^post25+i13^0 == 0 /\ i11^0-i11^post25 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : i17^0'=i17^post0, i11^0'=i11^post0, tmp___0^0'=tmp___0^post0, i9^0'=i9^post0, i15^0'=i15^post0, arraySize^0'=arraySize^post0, tmp^0'=tmp^post0, i7^0'=i7^post0, i13^0'=i13^post0, i^0'=i^post0, (-i9^post0+i9^0 == 0 /\ i11^0-i11^post0 == 0 /\ arraySize^0-arraySize^post0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -i7^post0+i7^0 == 0 /\ -i^post0+i^0 == 0 /\ i17^0-i17^post0 == 0 /\ -i13^post0+i13^0 == 0 /\ -i15^post0+i15^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0), cost: 1 New rule: l0 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l4 : i17^0'=i17^post2, i11^0'=i11^post2, tmp___0^0'=tmp___0^post2, i9^0'=i9^post2, i15^0'=i15^post2, arraySize^0'=arraySize^post2, tmp^0'=tmp^post2, i7^0'=i7^post2, i13^0'=i13^post2, i^0'=i^post2, (1-arraySize^0+i^0 <= 0 /\ tmp^0-tmp^post2 == 0 /\ -i15^post2+i15^0 == 0 /\ -i9^post2+i9^0 == 0 /\ arraySize^0-arraySize^post2 == 0 /\ i11^0-i11^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -i7^post2+i7^0 == 0 /\ -1+i^post2-i^0 == 0 /\ i17^0-i17^post2 == 0 /\ -i13^post2+i13^0 == 0), cost: 1 New rule: l2 -> l4 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l6 : i17^0'=i17^post3, i11^0'=i11^post3, tmp___0^0'=tmp___0^post3, i9^0'=i9^post3, i15^0'=i15^post3, arraySize^0'=arraySize^post3, tmp^0'=tmp^post3, i7^0'=i7^post3, i13^0'=i13^post3, i^0'=i^post3, (i17^0-i17^post3 == 0 /\ i11^0-i11^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -arraySize^post3+arraySize^0 == 0 /\ i7^0-i7^post3 == 0 /\ -i13^post3+i13^0 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ i15^0-i15^post3 == 0 /\ i9^0-i9^post3 == 0 /\ -i^post3+i^0 == 0), cost: 1 New rule: l5 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l4 : i17^0'=i17^post4, i11^0'=i11^post4, tmp___0^0'=tmp___0^post4, i9^0'=i9^post4, i15^0'=i15^post4, arraySize^0'=arraySize^post4, tmp^0'=tmp^post4, i7^0'=i7^post4, i13^0'=i13^post4, i^0'=i^post4, (-tmp^post4+tmp^0 == 0 /\ i15^0-i15^post4 == 0 /\ i9^0-i9^post4 == 0 /\ i^post4 == 0 /\ -arraySize^post4+arraySize^0 == 0 /\ -i13^post4+i13^0 == 0 /\ i7^0-i7^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -i17^post4+i17^0 == 0 /\ i11^0-i11^post4 == 0 /\ -i17^0+arraySize^0 <= 0), cost: 1 New rule: l7 -> l4 : i^0'=0, -i17^0+arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l7 -> l8 : i17^0'=i17^post5, i11^0'=i11^post5, tmp___0^0'=tmp___0^post5, i9^0'=i9^post5, i15^0'=i15^post5, arraySize^0'=arraySize^post5, tmp^0'=tmp^post5, i7^0'=i7^post5, i13^0'=i13^post5, i^0'=i^post5, (-tmp^post5+tmp^0 == 0 /\ i9^0-i9^post5 == 0 /\ i15^0-i15^post5 == 0 /\ -arraySize^post5+arraySize^0 == 0 /\ -i13^post5+i13^0 == 0 /\ 1+i17^0-arraySize^0 <= 0 /\ i7^0-i7^post5 == 0 /\ -1-i17^0+i17^post5 == 0 /\ -i^post5+i^0 == 0 /\ i11^0-i11^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0), cost: 1 New rule: l7 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l10 : i17^0'=i17^post6, i11^0'=i11^post6, tmp___0^0'=tmp___0^post6, i9^0'=i9^post6, i15^0'=i15^post6, arraySize^0'=arraySize^post6, tmp^0'=tmp^post6, i7^0'=i7^post6, i13^0'=i13^post6, i^0'=i^post6, (i15^0-i15^post6 == 0 /\ -i13^post6+i13^0 == 0 /\ i9^0-i9^post6 == 0 /\ i17^0-i17^post6 == 0 /\ -i11^post6+i11^0 == 0 /\ -i7^post6+i7^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -arraySize^post6+arraySize^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -i^post6+i^0 == 0), cost: 1 New rule: l9 -> l10 : TRUE, cost: 1 Applied preprocessing Original rule: l11 -> l8 : i17^0'=i17^post7, i11^0'=i11^post7, tmp___0^0'=tmp___0^post7, i9^0'=i9^post7, i15^0'=i15^post7, arraySize^0'=arraySize^post7, tmp^0'=tmp^post7, i7^0'=i7^post7, i13^0'=i13^post7, i^0'=i^post7, (-i13^post7+i13^0 == 0 /\ i9^0-i9^post7 == 0 /\ i17^10 == 0 /\ -i^post7+i^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -i15^0+arraySize^0 <= 0 /\ i11^0-i11^post7 == 0 /\ -arraySize^post7+arraySize^0 == 0 /\ i15^0-i15^post7 == 0 /\ -i7^post7+i7^0 == 0 /\ i17^post7 == 0), cost: 1 New rule: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l11 -> l12 : i17^0'=i17^post8, i11^0'=i11^post8, tmp___0^0'=tmp___0^post8, i9^0'=i9^post8, i15^0'=i15^post8, arraySize^0'=arraySize^post8, tmp^0'=tmp^post8, i7^0'=i7^post8, i13^0'=i13^post8, i^0'=i^post8, (1+i15^0-arraySize^0 <= 0 /\ -arraySize^post8+arraySize^0 == 0 /\ -i13^post8+i13^0 == 0 /\ i9^0-i9^post8 == 0 /\ -i^post8+i^0 == 0 /\ i17^0-i17^post8 == 0 /\ -1-i15^0+i15^post8 == 0 /\ -i11^post8+i11^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ -tmp^post8+tmp^0 == 0 /\ i7^0-i7^post8 == 0), cost: 1 New rule: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l13 -> l14 : i17^0'=i17^post9, i11^0'=i11^post9, tmp___0^0'=tmp___0^post9, i9^0'=i9^post9, i15^0'=i15^post9, arraySize^0'=arraySize^post9, tmp^0'=tmp^post9, i7^0'=i7^post9, i13^0'=i13^post9, i^0'=i^post9, (-i7^post9+i7^0 == 0 /\ -i^post9+i^0 == 0 /\ i13^0-i13^post9 == 0 /\ -arraySize^post9+arraySize^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ i15^0-i15^post9 == 0 /\ i9^0-i9^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ i17^0-i17^post9 == 0 /\ -i11^post9+i11^0 == 0), cost: 1 New rule: l13 -> l14 : TRUE, cost: 1 Applied preprocessing Original rule: l15 -> l12 : i17^0'=i17^post10, i11^0'=i11^post10, tmp___0^0'=tmp___0^post10, i9^0'=i9^post10, i15^0'=i15^post10, arraySize^0'=arraySize^post10, tmp^0'=tmp^post10, i7^0'=i7^post10, i13^0'=i13^post10, i^0'=i^post10, (-arraySize^post10+arraySize^0 == 0 /\ -i7^post10+i7^0 == 0 /\ -tmp^post10+tmp^0 == 0 /\ arraySize^0-i13^0 <= 0 /\ i9^0-i9^post10 == 0 /\ -i^post10+i^0 == 0 /\ i17^0-i17^post10 == 0 /\ i15^post10 == 0 /\ i15^10 == 0 /\ -i13^post10+i13^0 == 0 /\ i11^0-i11^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0), cost: 1 New rule: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 Applied preprocessing Original rule: l15 -> l16 : i17^0'=i17^post11, i11^0'=i11^post11, tmp___0^0'=tmp___0^post11, i9^0'=i9^post11, i15^0'=i15^post11, arraySize^0'=arraySize^post11, tmp^0'=tmp^post11, i7^0'=i7^post11, i13^0'=i13^post11, i^0'=i^post11, (-i7^post11+i7^0 == 0 /\ -arraySize^post11+arraySize^0 == 0 /\ i17^0-i17^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ i11^0-i11^post11 == 0 /\ 1-arraySize^0+i13^0 <= 0 /\ i15^0-i15^post11 == 0 /\ -i^post11+i^0 == 0 /\ i9^0-i9^post11 == 0 /\ -1-i13^0+i13^post11 == 0 /\ -tmp^post11+tmp^0 == 0), cost: 1 New rule: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 Applied preprocessing Original rule: l16 -> l15 : i17^0'=i17^post12, i11^0'=i11^post12, tmp___0^0'=tmp___0^post12, i9^0'=i9^post12, i15^0'=i15^post12, arraySize^0'=arraySize^post12, tmp^0'=tmp^post12, i7^0'=i7^post12, i13^0'=i13^post12, i^0'=i^post12, (-i15^post12+i15^0 == 0 /\ i17^0-i17^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i13^post12+i13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ i11^0-i11^post12 == 0 /\ -i^post12+i^0 == 0 /\ -i7^post12+i7^0 == 0 /\ i9^0-i9^post12 == 0 /\ arraySize^0-arraySize^post12 == 0), cost: 1 New rule: l16 -> l15 : TRUE, cost: 1 Applied preprocessing Original rule: l14 -> l16 : i17^0'=i17^post13, i11^0'=i11^post13, tmp___0^0'=tmp___0^post13, i9^0'=i9^post13, i15^0'=i15^post13, arraySize^0'=arraySize^post13, tmp^0'=tmp^post13, i7^0'=i7^post13, i13^0'=i13^post13, i^0'=i^post13, (arraySize^0-i^0 <= 0 /\ -tmp^post13+tmp^0 == 0 /\ i15^0-i15^post13 == 0 /\ -i^post13+i^0 == 0 /\ i13^10 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ i9^0-i9^post13 == 0 /\ -i7^post13+i7^0 == 0 /\ -arraySize^post13+arraySize^0 == 0 /\ i13^post13 == 0 /\ -i11^post13+i11^0 == 0 /\ i17^0-i17^post13 == 0), cost: 1 New rule: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 Applied preprocessing Original rule: l14 -> l13 : i17^0'=i17^post14, i11^0'=i11^post14, tmp___0^0'=tmp___0^post14, i9^0'=i9^post14, i15^0'=i15^post14, arraySize^0'=arraySize^post14, tmp^0'=tmp^post14, i7^0'=i7^post14, i13^0'=i13^post14, i^0'=i^post14, (-i15^post14+i15^0 == 0 /\ 1-arraySize^0+i^0 <= 0 /\ i17^0-i17^post14 == 0 /\ -i9^post14+i9^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ -1+i^post14-i^0 == 0 /\ -i7^post14+i7^0 == 0 /\ -i13^post14+i13^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ i11^0-i11^post14 == 0 /\ arraySize^0-arraySize^post14 == 0), cost: 1 New rule: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 Applied preprocessing Original rule: l12 -> l11 : i17^0'=i17^post15, i11^0'=i11^post15, tmp___0^0'=tmp___0^post15, i9^0'=i9^post15, i15^0'=i15^post15, arraySize^0'=arraySize^post15, tmp^0'=tmp^post15, i7^0'=i7^post15, i13^0'=i13^post15, i^0'=i^post15, (i11^0-i11^post15 == 0 /\ arraySize^0-arraySize^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ -i13^post15+i13^0 == 0 /\ i17^0-i17^post15 == 0 /\ -i7^post15+i7^0 == 0 /\ -i9^post15+i9^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ -i^post15+i^0 == 0), cost: 1 New rule: l12 -> l11 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l13 : i17^0'=i17^post16, i11^0'=i11^post16, tmp___0^0'=tmp___0^post16, i9^0'=i9^post16, i15^0'=i15^post16, arraySize^0'=arraySize^post16, tmp^0'=tmp^post16, i7^0'=i7^post16, i13^0'=i13^post16, i^0'=i^post16, (i17^0-i17^post16 == 0 /\ i^post16 == 0 /\ -i15^post16+i15^0 == 0 /\ i11^0-i11^post16 == 0 /\ arraySize^0-arraySize^post16 == 0 /\ -i11^0+arraySize^0 <= 0 /\ -i13^post16+i13^0 == 0 /\ i9^0-i9^post16 == 0 /\ -i7^post16+i7^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -tmp^post16+tmp^0 == 0), cost: 1 New rule: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l10 -> l9 : i17^0'=i17^post17, i11^0'=i11^post17, tmp___0^0'=tmp___0^post17, i9^0'=i9^post17, i15^0'=i15^post17, arraySize^0'=arraySize^post17, tmp^0'=tmp^post17, i7^0'=i7^post17, i13^0'=i13^post17, i^0'=i^post17, (tmp^0-tmp^post17 == 0 /\ -i15^post17+i15^0 == 0 /\ 1+i11^0-arraySize^0 <= 0 /\ arraySize^0-arraySize^post17 == 0 /\ -i9^post17+i9^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ -i^post17+i^0 == 0 /\ i17^0-i17^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ -i13^post17+i13^0 == 0 /\ -1-i11^0+i11^post17 == 0), cost: 1 New rule: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l8 -> l7 : i17^0'=i17^post18, i11^0'=i11^post18, tmp___0^0'=tmp___0^post18, i9^0'=i9^post18, i15^0'=i15^post18, arraySize^0'=arraySize^post18, tmp^0'=tmp^post18, i7^0'=i7^post18, i13^0'=i13^post18, i^0'=i^post18, (i17^0-i17^post18 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ -i13^post18+i13^0 == 0 /\ i7^0-i7^post18 == 0 /\ -arraySize^post18+arraySize^0 == 0 /\ i11^0-i11^post18 == 0 /\ -tmp^post18+tmp^0 == 0 /\ i15^0-i15^post18 == 0 /\ i9^0-i9^post18 == 0 /\ -i^post18+i^0 == 0), cost: 1 New rule: l8 -> l7 : TRUE, cost: 1 Applied preprocessing Original rule: l6 -> l9 : i17^0'=i17^post19, i11^0'=i11^post19, tmp___0^0'=tmp___0^post19, i9^0'=i9^post19, i15^0'=i15^post19, arraySize^0'=arraySize^post19, tmp^0'=tmp^post19, i7^0'=i7^post19, i13^0'=i13^post19, i^0'=i^post19, (-i^post19+i^0 == 0 /\ i15^0-i15^post19 == 0 /\ i9^0-i9^post19 == 0 /\ -i13^post19+i13^0 == 0 /\ -tmp^post19+tmp^0 == 0 /\ i11^10 == 0 /\ -i9^0+arraySize^0 <= 0 /\ -arraySize^post19+arraySize^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ i7^0-i7^post19 == 0 /\ i11^post19 == 0 /\ i17^0-i17^post19 == 0), cost: 1 New rule: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l5 : i17^0'=i17^post20, i11^0'=i11^post20, tmp___0^0'=tmp___0^post20, i9^0'=i9^post20, i15^0'=i15^post20, arraySize^0'=arraySize^post20, tmp^0'=tmp^post20, i7^0'=i7^post20, i13^0'=i13^post20, i^0'=i^post20, (-arraySize^post20+arraySize^0 == 0 /\ 1+i9^0-arraySize^0 <= 0 /\ i15^0-i15^post20 == 0 /\ -i^post20+i^0 == 0 /\ -i13^post20+i13^0 == 0 /\ i17^0-i17^post20 == 0 /\ i11^0-i11^post20 == 0 /\ -1-i9^0+i9^post20 == 0 /\ i7^0-i7^post20 == 0 /\ -tmp^post20+tmp^0 == 0 /\ tmp___0^0-tmp___0^post20 == 0), cost: 1 New rule: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 Applied preprocessing Original rule: l4 -> l2 : i17^0'=i17^post21, i11^0'=i11^post21, tmp___0^0'=tmp___0^post21, i9^0'=i9^post21, i15^0'=i15^post21, arraySize^0'=arraySize^post21, tmp^0'=tmp^post21, i7^0'=i7^post21, i13^0'=i13^post21, i^0'=i^post21, (i13^0-i13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -i^post21+i^0 == 0 /\ -arraySize^post21+arraySize^0 == 0 /\ i9^0-i9^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ i15^0-i15^post21 == 0 /\ -i11^post21+i11^0 == 0 /\ i17^0-i17^post21 == 0 /\ -i7^post21+i7^0 == 0), cost: 1 New rule: l4 -> l2 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l5 : i17^0'=i17^post22, i11^0'=i11^post22, tmp___0^0'=tmp___0^post22, i9^0'=i9^post22, i15^0'=i15^post22, arraySize^0'=arraySize^post22, tmp^0'=tmp^post22, i7^0'=i7^post22, i13^0'=i13^post22, i^0'=i^post22, (i15^0-i15^post22 == 0 /\ -tmp^post22+tmp^0 == 0 /\ i17^0-i17^post22 == 0 /\ -i^post22+i^0 == 0 /\ i9^post22 == 0 /\ -arraySize^post22+arraySize^0 == 0 /\ -i13^post22+i13^0 == 0 /\ i9^10 == 0 /\ tmp___0^0-tmp___0^post22 == 0 /\ i11^0-i11^post22 == 0 /\ arraySize^0-i7^0 <= 0 /\ -i7^post22+i7^0 == 0), cost: 1 New rule: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 Applied preprocessing Original rule: l1 -> l0 : i17^0'=i17^post23, i11^0'=i11^post23, tmp___0^0'=tmp___0^post23, i9^0'=i9^post23, i15^0'=i15^post23, arraySize^0'=arraySize^post23, tmp^0'=tmp^post23, i7^0'=i7^post23, i13^0'=i13^post23, i^0'=i^post23, (-tmp^post23+tmp^0 == 0 /\ -i11^post23+i11^0 == 0 /\ i13^0-i13^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -1+i7^post23-i7^0 == 0 /\ -arraySize^post23+arraySize^0 == 0 /\ 1-arraySize^0+i7^0 <= 0 /\ i15^0-i15^post23 == 0 /\ i9^0-i9^post23 == 0 /\ -i^post23+i^0 == 0 /\ i17^0-i17^post23 == 0), cost: 1 New rule: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 Applied preprocessing Original rule: l17 -> l0 : i17^0'=i17^post24, i11^0'=i11^post24, tmp___0^0'=tmp___0^post24, i9^0'=i9^post24, i15^0'=i15^post24, arraySize^0'=arraySize^post24, tmp^0'=tmp^post24, i7^0'=i7^post24, i13^0'=i13^post24, i^0'=i^post24, (0 == 0 /\ i15^0-i15^post24 == 0 /\ i7^post24 == 0 /\ i17^0-i17^post24 == 0 /\ i^post24 == 0 /\ i9^0-i9^post24 == 0 /\ -i13^post24+i13^0 == 0 /\ i11^0-i11^post24 == 0 /\ i7^10 == 0 /\ -arraySize^post24+arraySize^0 == 0), cost: 1 New rule: l17 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 1 Applied preprocessing Original rule: l18 -> l17 : i17^0'=i17^post25, i11^0'=i11^post25, tmp___0^0'=tmp___0^post25, i9^0'=i9^post25, i15^0'=i15^post25, arraySize^0'=arraySize^post25, tmp^0'=tmp^post25, i7^0'=i7^post25, i13^0'=i13^post25, i^0'=i^post25, (-i15^post25+i15^0 == 0 /\ i17^0-i17^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i7^post25+i7^0 == 0 /\ -i^post25+i^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ -arraySize^post25+arraySize^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ -i13^post25+i13^0 == 0 /\ i11^0-i11^post25 == 0), cost: 1 New rule: l18 -> l17 : TRUE, cost: 1 Simplified rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 27: l2 -> l4 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 46: l4 -> l2 : TRUE, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -i17^0+arraySize^0 <= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 49: l17 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 1 50: l18 -> l17 : TRUE, cost: 1 Eliminating location l17 by chaining: Applied chaining First rule: l18 -> l17 : TRUE, cost: 1 Second rule: l17 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 1 New rule: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied deletion Removed the following rules: 49 50 Eliminating location l2 by chaining: Applied chaining First rule: l4 -> l2 : TRUE, cost: 1 Second rule: l2 -> l4 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 New rule: l4 -> l4 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 2 Applied deletion Removed the following rules: 27 46 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 52: l4 -> l4 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 2 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -i17^0+arraySize^0 <= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l4 -> l4 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 2 New rule: l4 -> l4 : i^0'=n+i^0, (arraySize^0-n-i^0 >= 0 /\ n >= 0), cost: 2*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_PHBIHM.txt Applied instantiation Original rule: l4 -> l4 : i^0'=n+i^0, (arraySize^0-n-i^0 >= 0 /\ n >= 0), cost: 2*n New rule: l4 -> l4 : i^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i^0 >= 0), cost: 2*arraySize^0-2*i^0 Applied simplification Original rule: l4 -> l4 : i^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i^0 >= 0), cost: 2*arraySize^0-2*i^0 New rule: l4 -> l4 : i^0'=arraySize^0, arraySize^0-i^0 >= 0, cost: 2*arraySize^0-2*i^0 Applied deletion Removed the following rules: 52 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 54: l4 -> l4 : i^0'=arraySize^0, arraySize^0-i^0 >= 0, cost: 2*arraySize^0-2*i^0 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -i17^0+arraySize^0 <= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l7 -> l4 : i^0'=0, -i17^0+arraySize^0 <= 0, cost: 1 Second rule: l4 -> l4 : i^0'=arraySize^0, arraySize^0-i^0 >= 0, cost: 2*arraySize^0-2*i^0 New rule: l7 -> l4 : i^0'=arraySize^0, (arraySize^0 >= 0 /\ -i17^0+arraySize^0 <= 0), cost: 1+2*arraySize^0 Applied deletion Removed the following rules: 54 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -i17^0+arraySize^0 <= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 1 55: l7 -> l4 : i^0'=arraySize^0, (arraySize^0 >= 0 /\ -i17^0+arraySize^0 <= 0), cost: 1+2*arraySize^0 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Eliminating location l7 by chaining: Applied chaining First rule: l8 -> l7 : TRUE, cost: 1 Second rule: l7 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 1 New rule: l8 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 2 Applied deletion Removed the following rules: 30 43 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 56: l8 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 2 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l8 -> l8 : i17^0'=1+i17^0, 1+i17^0-arraySize^0 <= 0, cost: 2 New rule: l8 -> l8 : i17^0'=i17^0+n0, (n0 >= 0 /\ -i17^0-n0+arraySize^0 >= 0), cost: 2*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_gdMmec.txt Applied instantiation Original rule: l8 -> l8 : i17^0'=i17^0+n0, (n0 >= 0 /\ -i17^0-n0+arraySize^0 >= 0), cost: 2*n0 New rule: l8 -> l8 : i17^0'=arraySize^0, (0 >= 0 /\ -i17^0+arraySize^0 >= 0), cost: -2*i17^0+2*arraySize^0 Applied simplification Original rule: l8 -> l8 : i17^0'=arraySize^0, (0 >= 0 /\ -i17^0+arraySize^0 >= 0), cost: -2*i17^0+2*arraySize^0 New rule: l8 -> l8 : i17^0'=arraySize^0, -i17^0+arraySize^0 >= 0, cost: -2*i17^0+2*arraySize^0 Applied deletion Removed the following rules: 56 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 58: l8 -> l8 : i17^0'=arraySize^0, -i17^0+arraySize^0 >= 0, cost: -2*i17^0+2*arraySize^0 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 Second rule: l8 -> l8 : i17^0'=arraySize^0, -i17^0+arraySize^0 >= 0, cost: -2*i17^0+2*arraySize^0 New rule: l11 -> l8 : i17^0'=arraySize^0, (-i15^0+arraySize^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 Applied deletion Removed the following rules: 58 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -i15^0+arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 59: l11 -> l8 : i17^0'=arraySize^0, (-i15^0+arraySize^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Eliminating location l11 by chaining: Applied chaining First rule: l12 -> l11 : TRUE, cost: 1 Second rule: l11 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 1 New rule: l12 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 2 Applied deletion Removed the following rules: 33 40 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 60: l12 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 2 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l12 -> l12 : i15^0'=1+i15^0, 1+i15^0-arraySize^0 <= 0, cost: 2 New rule: l12 -> l12 : i15^0'=i15^0+n1, (-i15^0+arraySize^0-n1 >= 0 /\ n1 >= 0), cost: 2*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_bFMIpd.txt Applied instantiation Original rule: l12 -> l12 : i15^0'=i15^0+n1, (-i15^0+arraySize^0-n1 >= 0 /\ n1 >= 0), cost: 2*n1 New rule: l12 -> l12 : i15^0'=arraySize^0, (0 >= 0 /\ -i15^0+arraySize^0 >= 0), cost: -2*i15^0+2*arraySize^0 Applied simplification Original rule: l12 -> l12 : i15^0'=arraySize^0, (0 >= 0 /\ -i15^0+arraySize^0 >= 0), cost: -2*i15^0+2*arraySize^0 New rule: l12 -> l12 : i15^0'=arraySize^0, -i15^0+arraySize^0 >= 0, cost: -2*i15^0+2*arraySize^0 Applied deletion Removed the following rules: 60 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 62: l12 -> l12 : i15^0'=arraySize^0, -i15^0+arraySize^0 >= 0, cost: -2*i15^0+2*arraySize^0 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 Second rule: l12 -> l12 : i15^0'=arraySize^0, -i15^0+arraySize^0 >= 0, cost: -2*i15^0+2*arraySize^0 New rule: l15 -> l12 : i15^0'=arraySize^0, (arraySize^0-i13^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 Applied deletion Removed the following rules: 62 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, arraySize^0-i13^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 63: l15 -> l12 : i15^0'=arraySize^0, (arraySize^0-i13^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Eliminating location l15 by chaining: Applied chaining First rule: l16 -> l15 : TRUE, cost: 1 Second rule: l15 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 1 New rule: l16 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 2 Applied deletion Removed the following rules: 36 37 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 64: l16 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 2 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l16 -> l16 : i13^0'=1+i13^0, 1-arraySize^0+i13^0 <= 0, cost: 2 New rule: l16 -> l16 : i13^0'=n2+i13^0, (n2 >= 0 /\ -n2+arraySize^0-i13^0 >= 0), cost: 2*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_aoGaDo.txt Applied instantiation Original rule: l16 -> l16 : i13^0'=n2+i13^0, (n2 >= 0 /\ -n2+arraySize^0-i13^0 >= 0), cost: 2*n2 New rule: l16 -> l16 : i13^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i13^0 >= 0), cost: 2*arraySize^0-2*i13^0 Applied simplification Original rule: l16 -> l16 : i13^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i13^0 >= 0), cost: 2*arraySize^0-2*i13^0 New rule: l16 -> l16 : i13^0'=arraySize^0, arraySize^0-i13^0 >= 0, cost: 2*arraySize^0-2*i13^0 Applied deletion Removed the following rules: 64 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 66: l16 -> l16 : i13^0'=arraySize^0, arraySize^0-i13^0 >= 0, cost: 2*arraySize^0-2*i13^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 Second rule: l16 -> l16 : i13^0'=arraySize^0, arraySize^0-i13^0 >= 0, cost: 2*arraySize^0-2*i13^0 New rule: l14 -> l16 : i13^0'=arraySize^0, (arraySize^0-i^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 Applied deletion Removed the following rules: 66 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, arraySize^0-i^0 <= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 67: l14 -> l16 : i13^0'=arraySize^0, (arraySize^0-i^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 39: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Eliminating location l14 by chaining: Applied chaining First rule: l13 -> l14 : TRUE, cost: 1 Second rule: l14 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 1 New rule: l13 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 2 Applied deletion Removed the following rules: 34 39 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 68: l13 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 2 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l13 -> l13 : i^0'=1+i^0, 1-arraySize^0+i^0 <= 0, cost: 2 New rule: l13 -> l13 : i^0'=n3+i^0, (n3 >= 0 /\ -n3+arraySize^0-i^0 >= 0), cost: 2*n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_CHGAJp.txt Applied instantiation Original rule: l13 -> l13 : i^0'=n3+i^0, (n3 >= 0 /\ -n3+arraySize^0-i^0 >= 0), cost: 2*n3 New rule: l13 -> l13 : i^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i^0 >= 0), cost: 2*arraySize^0-2*i^0 Applied simplification Original rule: l13 -> l13 : i^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i^0 >= 0), cost: 2*arraySize^0-2*i^0 New rule: l13 -> l13 : i^0'=arraySize^0, arraySize^0-i^0 >= 0, cost: 2*arraySize^0-2*i^0 Applied deletion Removed the following rules: 68 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 70: l13 -> l13 : i^0'=arraySize^0, arraySize^0-i^0 >= 0, cost: 2*arraySize^0-2*i^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 Second rule: l13 -> l13 : i^0'=arraySize^0, arraySize^0-i^0 >= 0, cost: 2*arraySize^0-2*i^0 New rule: l10 -> l13 : i^0'=arraySize^0, (-i11^0+arraySize^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 Applied deletion Removed the following rules: 70 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -i11^0+arraySize^0 <= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 71: l10 -> l13 : i^0'=arraySize^0, (-i11^0+arraySize^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Eliminating location l10 by chaining: Applied chaining First rule: l9 -> l10 : TRUE, cost: 1 Second rule: l10 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 1 New rule: l9 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 2 Applied deletion Removed the following rules: 31 42 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 72: l9 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 2 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l9 -> l9 : i11^0'=1+i11^0, 1+i11^0-arraySize^0 <= 0, cost: 2 New rule: l9 -> l9 : i11^0'=i11^0+n4, (-i11^0+arraySize^0-n4 >= 0 /\ n4 >= 0), cost: 2*n4 Sub-proof via acceration calculus written to file:///tmp/tmpnam_GAPenc.txt Applied instantiation Original rule: l9 -> l9 : i11^0'=i11^0+n4, (-i11^0+arraySize^0-n4 >= 0 /\ n4 >= 0), cost: 2*n4 New rule: l9 -> l9 : i11^0'=arraySize^0, (0 >= 0 /\ -i11^0+arraySize^0 >= 0), cost: -2*i11^0+2*arraySize^0 Applied simplification Original rule: l9 -> l9 : i11^0'=arraySize^0, (0 >= 0 /\ -i11^0+arraySize^0 >= 0), cost: -2*i11^0+2*arraySize^0 New rule: l9 -> l9 : i11^0'=arraySize^0, -i11^0+arraySize^0 >= 0, cost: -2*i11^0+2*arraySize^0 Applied deletion Removed the following rules: 72 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 74: l9 -> l9 : i11^0'=arraySize^0, -i11^0+arraySize^0 >= 0, cost: -2*i11^0+2*arraySize^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 Second rule: l9 -> l9 : i11^0'=arraySize^0, -i11^0+arraySize^0 >= 0, cost: -2*i11^0+2*arraySize^0 New rule: l6 -> l9 : i11^0'=arraySize^0, (-i9^0+arraySize^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 Applied deletion Removed the following rules: 74 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -i9^0+arraySize^0 <= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 75: l6 -> l9 : i11^0'=arraySize^0, (-i9^0+arraySize^0 <= 0 /\ arraySize^0 >= 0), cost: 1+2*arraySize^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Eliminating location l6 by chaining: Applied chaining First rule: l5 -> l6 : TRUE, cost: 1 Second rule: l6 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 1 New rule: l5 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 2 Applied deletion Removed the following rules: 28 45 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 76: l5 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 2 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l5 -> l5 : i9^0'=1+i9^0, 1+i9^0-arraySize^0 <= 0, cost: 2 New rule: l5 -> l5 : i9^0'=n5+i9^0, (n5 >= 0 /\ -n5-i9^0+arraySize^0 >= 0), cost: 2*n5 Sub-proof via acceration calculus written to file:///tmp/tmpnam_egFboF.txt Applied instantiation Original rule: l5 -> l5 : i9^0'=n5+i9^0, (n5 >= 0 /\ -n5-i9^0+arraySize^0 >= 0), cost: 2*n5 New rule: l5 -> l5 : i9^0'=arraySize^0, (0 >= 0 /\ -i9^0+arraySize^0 >= 0), cost: -2*i9^0+2*arraySize^0 Applied simplification Original rule: l5 -> l5 : i9^0'=arraySize^0, (0 >= 0 /\ -i9^0+arraySize^0 >= 0), cost: -2*i9^0+2*arraySize^0 New rule: l5 -> l5 : i9^0'=arraySize^0, -i9^0+arraySize^0 >= 0, cost: -2*i9^0+2*arraySize^0 Applied deletion Removed the following rules: 76 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 78: l5 -> l5 : i9^0'=arraySize^0, -i9^0+arraySize^0 >= 0, cost: -2*i9^0+2*arraySize^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 Second rule: l5 -> l5 : i9^0'=arraySize^0, -i9^0+arraySize^0 >= 0, cost: -2*i9^0+2*arraySize^0 New rule: l1 -> l5 : i9^0'=arraySize^0, (arraySize^0 >= 0 /\ arraySize^0-i7^0 <= 0), cost: 1+2*arraySize^0 Applied deletion Removed the following rules: 78 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, arraySize^0-i7^0 <= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 79: l1 -> l5 : i9^0'=arraySize^0, (arraySize^0 >= 0 /\ arraySize^0-i7^0 <= 0), cost: 1+2*arraySize^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Eliminating location l1 by chaining: Applied chaining First rule: l0 -> l1 : TRUE, cost: 1 Second rule: l1 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 1 New rule: l0 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 2 Applied deletion Removed the following rules: 26 48 Eliminated locations on linear paths Start location: l18 80: l0 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 2 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied acceleration Original rule: l0 -> l0 : i7^0'=1+i7^0, 1-arraySize^0+i7^0 <= 0, cost: 2 New rule: l0 -> l0 : i7^0'=n6+i7^0, (-n6+arraySize^0-i7^0 >= 0 /\ n6 >= 0), cost: 2*n6 Sub-proof via acceration calculus written to file:///tmp/tmpnam_CPngEg.txt Applied instantiation Original rule: l0 -> l0 : i7^0'=n6+i7^0, (-n6+arraySize^0-i7^0 >= 0 /\ n6 >= 0), cost: 2*n6 New rule: l0 -> l0 : i7^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i7^0 >= 0), cost: 2*arraySize^0-2*i7^0 Applied simplification Original rule: l0 -> l0 : i7^0'=arraySize^0, (0 >= 0 /\ arraySize^0-i7^0 >= 0), cost: 2*arraySize^0-2*i7^0 New rule: l0 -> l0 : i7^0'=arraySize^0, arraySize^0-i7^0 >= 0, cost: 2*arraySize^0-2*i7^0 Applied deletion Removed the following rules: 80 Accelerated simple loops Start location: l18 82: l0 -> l0 : i7^0'=arraySize^0, arraySize^0-i7^0 >= 0, cost: 2*arraySize^0-2*i7^0 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Applied chaining First rule: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 Second rule: l0 -> l0 : i7^0'=arraySize^0, arraySize^0-i7^0 >= 0, cost: 2*arraySize^0-2*i7^0 New rule: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=arraySize^0, i^0'=0, arraySize^0 >= 0, cost: 2+2*arraySize^0 Applied deletion Removed the following rules: 82 Chained accelerated rules with incoming rules Start location: l18 51: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=0, i^0'=0, 0 == 0, cost: 2 83: l18 -> l0 : tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, i7^0'=arraySize^0, i^0'=0, arraySize^0 >= 0, cost: 2+2*arraySize^0 Removed unreachable locations and irrelevant leafs Start location: l18 Computing asymptotic complexity Proved the following lower bound Complexity: Unknown Cpx degree: ? Solved cost: 0 Rule cost: 0