NO Initial ITS Start location: l12 Program variables: data16^0 data18^0 i6^0 ret17^0 ret28^0 ret_f19^0 ret_f212^0 ret_f215^0 tmp^0 val10^0 val13^0 0: l0 -> l1 : data16^0'=data16^post1, data18^0'=data18^post1, i6^0'=i6^post1, ret17^0'=ret17^post1, ret28^0'=ret28^post1, ret_f19^0'=ret_f19^post1, ret_f212^0'=ret_f212^post1, ret_f215^0'=ret_f215^post1, tmp^0'=tmp^post1, val10^0'=val10^post1, val13^0'=val13^post1, (0 == 0 /\ -ret28^post1+ret28^0 == 0 /\ ret17^0-ret17^post1 == 0 /\ val13^0-val13^post1 == 0 /\ val10^0-val10^post1 == 0 /\ -data16^post1+data16^0 == 0 /\ ret_f212^0-ret_f212^post1 == 0 /\ -ret_f19^post1+ret_f19^0 == 0 /\ ret_f215^0-ret_f215^post1 == 0 /\ -data18^post1+data18^0 == 0 /\ -tmp^post1+tmp^0 == 0), cost: 1 1: l0 -> l2 : data16^0'=data16^post2, data18^0'=data18^post2, i6^0'=i6^post2, ret17^0'=ret17^post2, ret28^0'=ret28^post2, ret_f19^0'=ret_f19^post2, ret_f212^0'=ret_f212^post2, ret_f215^0'=ret_f215^post2, tmp^0'=tmp^post2, val10^0'=val10^post2, val13^0'=val13^post2, (-ret_f212^post2+ret_f212^0 == 0 /\ -ret17^post2+ret17^0 == 0 /\ -ret28^post2+ret28^0 == 0 /\ -data16^post2+data16^0 == 0 /\ -val13^post2+val13^0 == 0 /\ -1+ret_f19^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ val10^0-val10^post2 == 0 /\ -ret_f215^post2+ret_f215^0 == 0 /\ -data18^post2+data18^0 == 0 /\ i6^0-i6^post2 == 0), cost: 1 13: l1 -> l9 : data16^0'=data16^post14, data18^0'=data18^post14, i6^0'=i6^post14, ret17^0'=ret17^post14, ret28^0'=ret28^post14, ret_f19^0'=ret_f19^post14, ret_f212^0'=ret_f212^post14, ret_f215^0'=ret_f215^post14, tmp^0'=tmp^post14, val10^0'=val10^post14, val13^0'=val13^post14, (tmp^0-tmp^post14 == 0 /\ ret17^0-ret17^post14 == 0 /\ -ret_f215^post14+ret_f215^0 == 0 /\ ret_f212^0-ret_f212^post14 == 0 /\ -val13^post14+val13^0 == 0 /\ -ret_f19^post14+ret_f19^0 == 0 /\ i6^0-i6^post14 == 0 /\ -data16^post14+data16^0 == 0 /\ -data18^post14+data18^0 == 0 /\ val10^0-val10^post14 == 0 /\ -ret28^post14+ret28^0 == 0), cost: 1 2: l2 -> l3 : data16^0'=data16^post3, data18^0'=data18^post3, i6^0'=i6^post3, ret17^0'=ret17^post3, ret28^0'=ret28^post3, ret_f19^0'=ret_f19^post3, ret_f212^0'=ret_f212^post3, ret_f215^0'=ret_f215^post3, tmp^0'=tmp^post3, val10^0'=val10^post3, val13^0'=val13^post3, (-data16^post3+data16^0 == 0 /\ tmp^post3-ret_f19^0 == 0 /\ -ret_f19^post3+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post3 == 0 /\ val13^0-val13^post3 == 0 /\ ret17^0-ret17^post3 == 0 /\ val10^0-val10^post3 == 0 /\ ret_f215^0-ret_f215^post3 == 0 /\ ret28^0-ret28^post3 == 0 /\ i6^0-i6^post3 == 0 /\ data18^0-data18^post3 == 0), cost: 1 3: l4 -> l2 : data16^0'=data16^post4, data18^0'=data18^post4, i6^0'=i6^post4, ret17^0'=ret17^post4, ret28^0'=ret28^post4, ret_f19^0'=ret_f19^post4, ret_f212^0'=ret_f212^post4, ret_f215^0'=ret_f215^post4, tmp^0'=tmp^post4, val10^0'=val10^post4, val13^0'=val13^post4, (tmp^0-tmp^post4 == 0 /\ i6^0-i6^post4 == 0 /\ val10^0-val10^post4 == 0 /\ -ret17^post4+ret17^0 == 0 /\ -val13^post4+val13^0 == 0 /\ -data18^post4+data18^0 == 0 /\ -data16^post4+data16^0 == 0 /\ -ret28^0+ret_f19^post4 == 0 /\ ret_f212^0-ret_f212^post4 == 0 /\ -ret28^post4+ret28^0 == 0 /\ -ret_f215^post4+ret_f215^0 == 0), cost: 1 4: l5 -> l2 : data16^0'=data16^post5, data18^0'=data18^post5, i6^0'=i6^post5, ret17^0'=ret17^post5, ret28^0'=ret28^post5, ret_f19^0'=ret_f19^post5, ret_f212^0'=ret_f212^post5, ret_f215^0'=ret_f215^post5, tmp^0'=tmp^post5, val10^0'=val10^post5, val13^0'=val13^post5, (ret_f19^post5 == 0 /\ ret_f212^0-ret_f212^post5 == 0 /\ val10^0-val10^post5 == 0 /\ -val13^post5+val13^0 == 0 /\ i6^0-i6^post5 == 0 /\ -data18^post5+data18^0 == 0 /\ -data16^post5+data16^0 == 0 /\ -ret28^0 <= 0 /\ ret_f215^0-ret_f215^post5 == 0 /\ -ret28^post5+ret28^0 == 0 /\ ret17^0-ret17^post5 == 0 /\ ret28^0 <= 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 5: l5 -> l4 : data16^0'=data16^post6, data18^0'=data18^post6, i6^0'=i6^post6, ret17^0'=ret17^post6, ret28^0'=ret28^post6, ret_f19^0'=ret_f19^post6, ret_f212^0'=ret_f212^post6, ret_f215^0'=ret_f215^post6, tmp^0'=tmp^post6, val10^0'=val10^post6, val13^0'=val13^post6, (ret17^0-ret17^post6 == 0 /\ -ret_f215^post6+ret_f215^0 == 0 /\ data18^0-data18^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ ret_f19^0-ret_f19^post6 == 0 /\ ret_f212^0-ret_f212^post6 == 0 /\ val10^0-val10^post6 == 0 /\ -data16^post6+data16^0 == 0 /\ i6^0-i6^post6 == 0 /\ 1-ret28^0 <= 0 /\ -ret28^post6+ret28^0 == 0 /\ -val13^post6+val13^0 == 0), cost: 1 6: l5 -> l4 : data16^0'=data16^post7, data18^0'=data18^post7, i6^0'=i6^post7, ret17^0'=ret17^post7, ret28^0'=ret28^post7, ret_f19^0'=ret_f19^post7, ret_f212^0'=ret_f212^post7, ret_f215^0'=ret_f215^post7, tmp^0'=tmp^post7, val10^0'=val10^post7, val13^0'=val13^post7, (-data16^post7+data16^0 == 0 /\ -data18^post7+data18^0 == 0 /\ 1+ret28^0 <= 0 /\ -ret_f19^post7+ret_f19^0 == 0 /\ ret28^0-ret28^post7 == 0 /\ val10^0-val10^post7 == 0 /\ val13^0-val13^post7 == 0 /\ -ret_f215^post7+ret_f215^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i6^0-i6^post7 == 0 /\ ret_f212^0-ret_f212^post7 == 0 /\ ret17^0-ret17^post7 == 0), cost: 1 7: l6 -> l0 : data16^0'=data16^post8, data18^0'=data18^post8, i6^0'=i6^post8, ret17^0'=ret17^post8, ret28^0'=ret28^post8, ret_f19^0'=ret_f19^post8, ret_f212^0'=ret_f212^post8, ret_f215^0'=ret_f215^post8, tmp^0'=tmp^post8, val10^0'=val10^post8, val13^0'=val13^post8, (-ret_f215^post8+ret_f215^0 == 0 /\ tmp^0-tmp^post8 == 0 /\ i6^0-i6^post8 == 0 /\ -data18^post8+data18^0 == 0 /\ ret17^0-ret17^post8 == 0 /\ -ret28^post8+ret28^0 == 0 /\ ret_f19^0-ret_f19^post8 == 0 /\ -val13^post8+val13^0 == 0 /\ ret_f212^0-ret_f212^post8 == 0 /\ val10^0-val10^post8 == 0 /\ -data16^post8+data16^0 == 0), cost: 1 8: l6 -> l3 : data16^0'=data16^post9, data18^0'=data18^post9, i6^0'=i6^post9, ret17^0'=ret17^post9, ret28^0'=ret28^post9, ret_f19^0'=ret_f19^post9, ret_f212^0'=ret_f212^post9, ret_f215^0'=ret_f215^post9, tmp^0'=tmp^post9, val10^0'=val10^post9, val13^0'=val13^post9, (-val13^post9+val13^0 == 0 /\ -i6^post9+i6^0 == 0 /\ ret17^0-ret17^post9 == 0 /\ -ret_f215^post9+ret_f215^0 == 0 /\ -ret_f19^post9+ret_f19^0 == 0 /\ -ret28^post9+ret28^0 == 0 /\ data18^0-data18^post9 == 0 /\ -data16^post9+data16^0 == 0 /\ val10^0-val10^post9 == 0 /\ ret_f212^0-ret_f212^post9 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 9: l7 -> l2 : data16^0'=data16^post10, data18^0'=data18^post10, i6^0'=i6^post10, ret17^0'=ret17^post10, ret28^0'=ret28^post10, ret_f19^0'=ret_f19^post10, ret_f212^0'=ret_f212^post10, ret_f215^0'=ret_f215^post10, tmp^0'=tmp^post10, val10^0'=val10^post10, val13^0'=val13^post10, (-val13^post10+val13^0 == 0 /\ -ret_f215^post10+ret_f215^0 == 0 /\ ret_f212^0-ret_f212^post10 == 0 /\ val10^0-val10^post10 == 0 /\ -ret17^0+ret_f19^post10 == 0 /\ -data16^post10+data16^0 == 0 /\ i6^0-i6^post10 == 0 /\ -ret28^post10+ret28^0 == 0 /\ -ret17^post10+ret17^0 == 0 /\ tmp^0-tmp^post10 == 0 /\ -data18^post10+data18^0 == 0), cost: 1 10: l8 -> l1 : data16^0'=data16^post11, data18^0'=data18^post11, i6^0'=i6^post11, ret17^0'=ret17^post11, ret28^0'=ret28^post11, ret_f19^0'=ret_f19^post11, ret_f212^0'=ret_f212^post11, ret_f215^0'=ret_f215^post11, tmp^0'=tmp^post11, val10^0'=val10^post11, val13^0'=val13^post11, (-tmp^post11+tmp^0 == 0 /\ -ret_f19^post11+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post11 == 0 /\ ret17^0 <= 0 /\ val13^0-val13^post11 == 0 /\ val10^0-val10^post11 == 0 /\ -ret17^0 <= 0 /\ -data16^post11+data16^0 == 0 /\ ret17^0-ret17^post11 == 0 /\ 1-i6^0+i6^post11 == 0 /\ ret_f215^0-ret_f215^post11 == 0 /\ data18^0-data18^post11 == 0 /\ ret28^0-ret28^post11 == 0), cost: 1 11: l8 -> l7 : data16^0'=data16^post12, data18^0'=data18^post12, i6^0'=i6^post12, ret17^0'=ret17^post12, ret28^0'=ret28^post12, ret_f19^0'=ret_f19^post12, ret_f212^0'=ret_f212^post12, ret_f215^0'=ret_f215^post12, tmp^0'=tmp^post12, val10^0'=val10^post12, val13^0'=val13^post12, (-ret_f212^post12+ret_f212^0 == 0 /\ -ret17^post12+ret17^0 == 0 /\ -ret28^post12+ret28^0 == 0 /\ 1-ret17^0 <= 0 /\ -data16^post12+data16^0 == 0 /\ -val13^post12+val13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ val10^0-val10^post12 == 0 /\ ret_f19^0-ret_f19^post12 == 0 /\ i6^0-i6^post12 == 0 /\ -ret_f215^post12+ret_f215^0 == 0 /\ -data18^post12+data18^0 == 0), cost: 1 12: l8 -> l7 : data16^0'=data16^post13, data18^0'=data18^post13, i6^0'=i6^post13, ret17^0'=ret17^post13, ret28^0'=ret28^post13, ret_f19^0'=ret_f19^post13, ret_f212^0'=ret_f212^post13, ret_f215^0'=ret_f215^post13, tmp^0'=tmp^post13, val10^0'=val10^post13, val13^0'=val13^post13, (tmp^0-tmp^post13 == 0 /\ val10^0-val10^post13 == 0 /\ -ret28^post13+ret28^0 == 0 /\ -val13^post13+val13^0 == 0 /\ ret17^0-ret17^post13 == 0 /\ ret_f212^0-ret_f212^post13 == 0 /\ -data16^post13+data16^0 == 0 /\ 1+ret17^0 <= 0 /\ -ret_f215^post13+ret_f215^0 == 0 /\ data18^0-data18^post13 == 0 /\ -ret_f19^post13+ret_f19^0 == 0 /\ -i6^post13+i6^0 == 0), cost: 1 15: l9 -> l5 : data16^0'=data16^post16, data18^0'=data18^post16, i6^0'=i6^post16, ret17^0'=ret17^post16, ret28^0'=ret28^post16, ret_f19^0'=ret_f19^post16, ret_f212^0'=ret_f212^post16, ret_f215^0'=ret_f215^post16, tmp^0'=tmp^post16, val10^0'=val10^post16, val13^0'=val13^post16, (0 == 0 /\ i6^0-i6^post16 == 0 /\ -val13^post16+data18^post16 == 0 /\ ret_f215^post16 == 0 /\ i6^0 <= 0 /\ -ret17^post16+ret17^0 == 0 /\ -i6^0 <= 0 /\ val10^0-val10^post16 == 0 /\ -ret_f215^post16+ret28^post16 == 0 /\ -data16^post16+data16^0 == 0 /\ ret_f212^0-ret_f212^post16 == 0 /\ ret_f19^0-ret_f19^post16 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 16: l9 -> l10 : data16^0'=data16^post17, data18^0'=data18^post17, i6^0'=i6^post17, ret17^0'=ret17^post17, ret28^0'=ret28^post17, ret_f19^0'=ret_f19^post17, ret_f212^0'=ret_f212^post17, ret_f215^0'=ret_f215^post17, tmp^0'=tmp^post17, val10^0'=val10^post17, val13^0'=val13^post17, (ret17^0-ret17^post17 == 0 /\ -ret28^post17+ret28^0 == 0 /\ 1-i6^0 <= 0 /\ val10^0-val10^post17 == 0 /\ val13^0-val13^post17 == 0 /\ data18^0-data18^post17 == 0 /\ -ret_f215^post17+ret_f215^0 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -i6^post17+i6^0 == 0 /\ -data16^post17+data16^0 == 0 /\ ret_f212^0-ret_f212^post17 == 0 /\ -ret_f19^post17+ret_f19^0 == 0), cost: 1 17: l9 -> l10 : data16^0'=data16^post18, data18^0'=data18^post18, i6^0'=i6^post18, ret17^0'=ret17^post18, ret28^0'=ret28^post18, ret_f19^0'=ret_f19^post18, ret_f212^0'=ret_f212^post18, ret_f215^0'=ret_f215^post18, tmp^0'=tmp^post18, val10^0'=val10^post18, val13^0'=val13^post18, (-val13^post18+val13^0 == 0 /\ -ret_f215^post18+ret_f215^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ i6^0-i6^post18 == 0 /\ 1+i6^0 <= 0 /\ ret17^0-ret17^post18 == 0 /\ -data18^post18+data18^0 == 0 /\ -ret28^post18+ret28^0 == 0 /\ ret_f212^0-ret_f212^post18 == 0 /\ ret_f19^0-ret_f19^post18 == 0 /\ val10^0-val10^post18 == 0 /\ -data16^post18+data16^0 == 0), cost: 1 14: l10 -> l8 : data16^0'=data16^post15, data18^0'=data18^post15, i6^0'=i6^post15, ret17^0'=ret17^post15, ret28^0'=ret28^post15, ret_f19^0'=ret_f19^post15, ret_f212^0'=ret_f212^post15, ret_f215^0'=ret_f215^post15, tmp^0'=tmp^post15, val10^0'=val10^post15, val13^0'=val13^post15, (0 == 0 /\ -val10^post15+data16^post15 == 0 /\ ret_f212^post15 == 0 /\ -ret_f212^post15+ret17^post15 == 0 /\ data18^0-data18^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ ret_f19^0-ret_f19^post15 == 0 /\ i6^0-i6^post15 == 0 /\ -ret_f215^post15+ret_f215^0 == 0 /\ -val13^post15+val13^0 == 0 /\ -ret28^post15+ret28^0 == 0), cost: 1 18: l11 -> l6 : data16^0'=data16^post19, data18^0'=data18^post19, i6^0'=i6^post19, ret17^0'=ret17^post19, ret28^0'=ret28^post19, ret_f19^0'=ret_f19^post19, ret_f212^0'=ret_f212^post19, ret_f215^0'=ret_f215^post19, tmp^0'=tmp^post19, val10^0'=val10^post19, val13^0'=val13^post19, (ret_f19^0-ret_f19^post19 == 0 /\ data18^0-data18^post19 == 0 /\ tmp^0-tmp^post19 == 0 /\ ret_f212^0-ret_f212^post19 == 0 /\ -ret_f215^post19+ret_f215^0 == 0 /\ val10^0-val10^post19 == 0 /\ i6^0-i6^post19 == 0 /\ -ret28^post19+ret28^0 == 0 /\ ret17^0-ret17^post19 == 0 /\ -data16^post19+data16^0 == 0 /\ -val13^post19+val13^0 == 0), cost: 1 19: l12 -> l11 : data16^0'=data16^post20, data18^0'=data18^post20, i6^0'=i6^post20, ret17^0'=ret17^post20, ret28^0'=ret28^post20, ret_f19^0'=ret_f19^post20, ret_f212^0'=ret_f212^post20, ret_f215^0'=ret_f215^post20, tmp^0'=tmp^post20, val10^0'=val10^post20, val13^0'=val13^post20, (-data16^post20+data16^0 == 0 /\ -data18^post20+data18^0 == 0 /\ val13^0-val13^post20 == 0 /\ val10^0-val10^post20 == 0 /\ ret_f212^0-ret_f212^post20 == 0 /\ ret_f215^0-ret_f215^post20 == 0 /\ -ret_f19^post20+ret_f19^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i6^0-i6^post20 == 0 /\ ret28^0-ret28^post20 == 0 /\ ret17^0-ret17^post20 == 0), cost: 1 Chained Linear Paths Start location: l12 Program variables: data16^0 data18^0 i6^0 ret17^0 ret28^0 ret_f19^0 ret_f212^0 ret_f215^0 tmp^0 val10^0 val13^0 0: l0 -> l1 : data16^0'=data16^post1, data18^0'=data18^post1, i6^0'=i6^post1, ret17^0'=ret17^post1, ret28^0'=ret28^post1, ret_f19^0'=ret_f19^post1, ret_f212^0'=ret_f212^post1, ret_f215^0'=ret_f215^post1, tmp^0'=tmp^post1, val10^0'=val10^post1, val13^0'=val13^post1, (0 == 0 /\ -ret28^post1+ret28^0 == 0 /\ ret17^0-ret17^post1 == 0 /\ val13^0-val13^post1 == 0 /\ val10^0-val10^post1 == 0 /\ -data16^post1+data16^0 == 0 /\ ret_f212^0-ret_f212^post1 == 0 /\ -ret_f19^post1+ret_f19^0 == 0 /\ ret_f215^0-ret_f215^post1 == 0 /\ -data18^post1+data18^0 == 0 /\ -tmp^post1+tmp^0 == 0), cost: 1 1: l0 -> l2 : data16^0'=data16^post2, data18^0'=data18^post2, i6^0'=i6^post2, ret17^0'=ret17^post2, ret28^0'=ret28^post2, ret_f19^0'=ret_f19^post2, ret_f212^0'=ret_f212^post2, ret_f215^0'=ret_f215^post2, tmp^0'=tmp^post2, val10^0'=val10^post2, val13^0'=val13^post2, (-ret_f212^post2+ret_f212^0 == 0 /\ -ret17^post2+ret17^0 == 0 /\ -ret28^post2+ret28^0 == 0 /\ -data16^post2+data16^0 == 0 /\ -val13^post2+val13^0 == 0 /\ -1+ret_f19^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ val10^0-val10^post2 == 0 /\ -ret_f215^post2+ret_f215^0 == 0 /\ -data18^post2+data18^0 == 0 /\ i6^0-i6^post2 == 0), cost: 1 13: l1 -> l9 : data16^0'=data16^post14, data18^0'=data18^post14, i6^0'=i6^post14, ret17^0'=ret17^post14, ret28^0'=ret28^post14, ret_f19^0'=ret_f19^post14, ret_f212^0'=ret_f212^post14, ret_f215^0'=ret_f215^post14, tmp^0'=tmp^post14, val10^0'=val10^post14, val13^0'=val13^post14, (tmp^0-tmp^post14 == 0 /\ ret17^0-ret17^post14 == 0 /\ -ret_f215^post14+ret_f215^0 == 0 /\ ret_f212^0-ret_f212^post14 == 0 /\ -val13^post14+val13^0 == 0 /\ -ret_f19^post14+ret_f19^0 == 0 /\ i6^0-i6^post14 == 0 /\ -data16^post14+data16^0 == 0 /\ -data18^post14+data18^0 == 0 /\ val10^0-val10^post14 == 0 /\ -ret28^post14+ret28^0 == 0), cost: 1 2: l2 -> l3 : data16^0'=data16^post3, data18^0'=data18^post3, i6^0'=i6^post3, ret17^0'=ret17^post3, ret28^0'=ret28^post3, ret_f19^0'=ret_f19^post3, ret_f212^0'=ret_f212^post3, ret_f215^0'=ret_f215^post3, tmp^0'=tmp^post3, val10^0'=val10^post3, val13^0'=val13^post3, (-data16^post3+data16^0 == 0 /\ tmp^post3-ret_f19^0 == 0 /\ -ret_f19^post3+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post3 == 0 /\ val13^0-val13^post3 == 0 /\ ret17^0-ret17^post3 == 0 /\ val10^0-val10^post3 == 0 /\ ret_f215^0-ret_f215^post3 == 0 /\ ret28^0-ret28^post3 == 0 /\ i6^0-i6^post3 == 0 /\ data18^0-data18^post3 == 0), cost: 1 3: l4 -> l2 : data16^0'=data16^post4, data18^0'=data18^post4, i6^0'=i6^post4, ret17^0'=ret17^post4, ret28^0'=ret28^post4, ret_f19^0'=ret_f19^post4, ret_f212^0'=ret_f212^post4, ret_f215^0'=ret_f215^post4, tmp^0'=tmp^post4, val10^0'=val10^post4, val13^0'=val13^post4, (tmp^0-tmp^post4 == 0 /\ i6^0-i6^post4 == 0 /\ val10^0-val10^post4 == 0 /\ -ret17^post4+ret17^0 == 0 /\ -val13^post4+val13^0 == 0 /\ -data18^post4+data18^0 == 0 /\ -data16^post4+data16^0 == 0 /\ -ret28^0+ret_f19^post4 == 0 /\ ret_f212^0-ret_f212^post4 == 0 /\ -ret28^post4+ret28^0 == 0 /\ -ret_f215^post4+ret_f215^0 == 0), cost: 1 4: l5 -> l2 : data16^0'=data16^post5, data18^0'=data18^post5, i6^0'=i6^post5, ret17^0'=ret17^post5, ret28^0'=ret28^post5, ret_f19^0'=ret_f19^post5, ret_f212^0'=ret_f212^post5, ret_f215^0'=ret_f215^post5, tmp^0'=tmp^post5, val10^0'=val10^post5, val13^0'=val13^post5, (ret_f19^post5 == 0 /\ ret_f212^0-ret_f212^post5 == 0 /\ val10^0-val10^post5 == 0 /\ -val13^post5+val13^0 == 0 /\ i6^0-i6^post5 == 0 /\ -data18^post5+data18^0 == 0 /\ -data16^post5+data16^0 == 0 /\ -ret28^0 <= 0 /\ ret_f215^0-ret_f215^post5 == 0 /\ -ret28^post5+ret28^0 == 0 /\ ret17^0-ret17^post5 == 0 /\ ret28^0 <= 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 5: l5 -> l4 : data16^0'=data16^post6, data18^0'=data18^post6, i6^0'=i6^post6, ret17^0'=ret17^post6, ret28^0'=ret28^post6, ret_f19^0'=ret_f19^post6, ret_f212^0'=ret_f212^post6, ret_f215^0'=ret_f215^post6, tmp^0'=tmp^post6, val10^0'=val10^post6, val13^0'=val13^post6, (ret17^0-ret17^post6 == 0 /\ -ret_f215^post6+ret_f215^0 == 0 /\ data18^0-data18^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ ret_f19^0-ret_f19^post6 == 0 /\ ret_f212^0-ret_f212^post6 == 0 /\ val10^0-val10^post6 == 0 /\ -data16^post6+data16^0 == 0 /\ i6^0-i6^post6 == 0 /\ 1-ret28^0 <= 0 /\ -ret28^post6+ret28^0 == 0 /\ -val13^post6+val13^0 == 0), cost: 1 6: l5 -> l4 : data16^0'=data16^post7, data18^0'=data18^post7, i6^0'=i6^post7, ret17^0'=ret17^post7, ret28^0'=ret28^post7, ret_f19^0'=ret_f19^post7, ret_f212^0'=ret_f212^post7, ret_f215^0'=ret_f215^post7, tmp^0'=tmp^post7, val10^0'=val10^post7, val13^0'=val13^post7, (-data16^post7+data16^0 == 0 /\ -data18^post7+data18^0 == 0 /\ 1+ret28^0 <= 0 /\ -ret_f19^post7+ret_f19^0 == 0 /\ ret28^0-ret28^post7 == 0 /\ val10^0-val10^post7 == 0 /\ val13^0-val13^post7 == 0 /\ -ret_f215^post7+ret_f215^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i6^0-i6^post7 == 0 /\ ret_f212^0-ret_f212^post7 == 0 /\ ret17^0-ret17^post7 == 0), cost: 1 7: l6 -> l0 : data16^0'=data16^post8, data18^0'=data18^post8, i6^0'=i6^post8, ret17^0'=ret17^post8, ret28^0'=ret28^post8, ret_f19^0'=ret_f19^post8, ret_f212^0'=ret_f212^post8, ret_f215^0'=ret_f215^post8, tmp^0'=tmp^post8, val10^0'=val10^post8, val13^0'=val13^post8, (-ret_f215^post8+ret_f215^0 == 0 /\ tmp^0-tmp^post8 == 0 /\ i6^0-i6^post8 == 0 /\ -data18^post8+data18^0 == 0 /\ ret17^0-ret17^post8 == 0 /\ -ret28^post8+ret28^0 == 0 /\ ret_f19^0-ret_f19^post8 == 0 /\ -val13^post8+val13^0 == 0 /\ ret_f212^0-ret_f212^post8 == 0 /\ val10^0-val10^post8 == 0 /\ -data16^post8+data16^0 == 0), cost: 1 8: l6 -> l3 : data16^0'=data16^post9, data18^0'=data18^post9, i6^0'=i6^post9, ret17^0'=ret17^post9, ret28^0'=ret28^post9, ret_f19^0'=ret_f19^post9, ret_f212^0'=ret_f212^post9, ret_f215^0'=ret_f215^post9, tmp^0'=tmp^post9, val10^0'=val10^post9, val13^0'=val13^post9, (-val13^post9+val13^0 == 0 /\ -i6^post9+i6^0 == 0 /\ ret17^0-ret17^post9 == 0 /\ -ret_f215^post9+ret_f215^0 == 0 /\ -ret_f19^post9+ret_f19^0 == 0 /\ -ret28^post9+ret28^0 == 0 /\ data18^0-data18^post9 == 0 /\ -data16^post9+data16^0 == 0 /\ val10^0-val10^post9 == 0 /\ ret_f212^0-ret_f212^post9 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 9: l7 -> l2 : data16^0'=data16^post10, data18^0'=data18^post10, i6^0'=i6^post10, ret17^0'=ret17^post10, ret28^0'=ret28^post10, ret_f19^0'=ret_f19^post10, ret_f212^0'=ret_f212^post10, ret_f215^0'=ret_f215^post10, tmp^0'=tmp^post10, val10^0'=val10^post10, val13^0'=val13^post10, (-val13^post10+val13^0 == 0 /\ -ret_f215^post10+ret_f215^0 == 0 /\ ret_f212^0-ret_f212^post10 == 0 /\ val10^0-val10^post10 == 0 /\ -ret17^0+ret_f19^post10 == 0 /\ -data16^post10+data16^0 == 0 /\ i6^0-i6^post10 == 0 /\ -ret28^post10+ret28^0 == 0 /\ -ret17^post10+ret17^0 == 0 /\ tmp^0-tmp^post10 == 0 /\ -data18^post10+data18^0 == 0), cost: 1 10: l8 -> l1 : data16^0'=data16^post11, data18^0'=data18^post11, i6^0'=i6^post11, ret17^0'=ret17^post11, ret28^0'=ret28^post11, ret_f19^0'=ret_f19^post11, ret_f212^0'=ret_f212^post11, ret_f215^0'=ret_f215^post11, tmp^0'=tmp^post11, val10^0'=val10^post11, val13^0'=val13^post11, (-tmp^post11+tmp^0 == 0 /\ -ret_f19^post11+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post11 == 0 /\ ret17^0 <= 0 /\ val13^0-val13^post11 == 0 /\ val10^0-val10^post11 == 0 /\ -ret17^0 <= 0 /\ -data16^post11+data16^0 == 0 /\ ret17^0-ret17^post11 == 0 /\ 1-i6^0+i6^post11 == 0 /\ ret_f215^0-ret_f215^post11 == 0 /\ data18^0-data18^post11 == 0 /\ ret28^0-ret28^post11 == 0), cost: 1 11: l8 -> l7 : data16^0'=data16^post12, data18^0'=data18^post12, i6^0'=i6^post12, ret17^0'=ret17^post12, ret28^0'=ret28^post12, ret_f19^0'=ret_f19^post12, ret_f212^0'=ret_f212^post12, ret_f215^0'=ret_f215^post12, tmp^0'=tmp^post12, val10^0'=val10^post12, val13^0'=val13^post12, (-ret_f212^post12+ret_f212^0 == 0 /\ -ret17^post12+ret17^0 == 0 /\ -ret28^post12+ret28^0 == 0 /\ 1-ret17^0 <= 0 /\ -data16^post12+data16^0 == 0 /\ -val13^post12+val13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ val10^0-val10^post12 == 0 /\ ret_f19^0-ret_f19^post12 == 0 /\ i6^0-i6^post12 == 0 /\ -ret_f215^post12+ret_f215^0 == 0 /\ -data18^post12+data18^0 == 0), cost: 1 12: l8 -> l7 : data16^0'=data16^post13, data18^0'=data18^post13, i6^0'=i6^post13, ret17^0'=ret17^post13, ret28^0'=ret28^post13, ret_f19^0'=ret_f19^post13, ret_f212^0'=ret_f212^post13, ret_f215^0'=ret_f215^post13, tmp^0'=tmp^post13, val10^0'=val10^post13, val13^0'=val13^post13, (tmp^0-tmp^post13 == 0 /\ val10^0-val10^post13 == 0 /\ -ret28^post13+ret28^0 == 0 /\ -val13^post13+val13^0 == 0 /\ ret17^0-ret17^post13 == 0 /\ ret_f212^0-ret_f212^post13 == 0 /\ -data16^post13+data16^0 == 0 /\ 1+ret17^0 <= 0 /\ -ret_f215^post13+ret_f215^0 == 0 /\ data18^0-data18^post13 == 0 /\ -ret_f19^post13+ret_f19^0 == 0 /\ -i6^post13+i6^0 == 0), cost: 1 15: l9 -> l5 : data16^0'=data16^post16, data18^0'=data18^post16, i6^0'=i6^post16, ret17^0'=ret17^post16, ret28^0'=ret28^post16, ret_f19^0'=ret_f19^post16, ret_f212^0'=ret_f212^post16, ret_f215^0'=ret_f215^post16, tmp^0'=tmp^post16, val10^0'=val10^post16, val13^0'=val13^post16, (0 == 0 /\ i6^0-i6^post16 == 0 /\ -val13^post16+data18^post16 == 0 /\ ret_f215^post16 == 0 /\ i6^0 <= 0 /\ -ret17^post16+ret17^0 == 0 /\ -i6^0 <= 0 /\ val10^0-val10^post16 == 0 /\ -ret_f215^post16+ret28^post16 == 0 /\ -data16^post16+data16^0 == 0 /\ ret_f212^0-ret_f212^post16 == 0 /\ ret_f19^0-ret_f19^post16 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 16: l9 -> l10 : data16^0'=data16^post17, data18^0'=data18^post17, i6^0'=i6^post17, ret17^0'=ret17^post17, ret28^0'=ret28^post17, ret_f19^0'=ret_f19^post17, ret_f212^0'=ret_f212^post17, ret_f215^0'=ret_f215^post17, tmp^0'=tmp^post17, val10^0'=val10^post17, val13^0'=val13^post17, (ret17^0-ret17^post17 == 0 /\ -ret28^post17+ret28^0 == 0 /\ 1-i6^0 <= 0 /\ val10^0-val10^post17 == 0 /\ val13^0-val13^post17 == 0 /\ data18^0-data18^post17 == 0 /\ -ret_f215^post17+ret_f215^0 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -i6^post17+i6^0 == 0 /\ -data16^post17+data16^0 == 0 /\ ret_f212^0-ret_f212^post17 == 0 /\ -ret_f19^post17+ret_f19^0 == 0), cost: 1 17: l9 -> l10 : data16^0'=data16^post18, data18^0'=data18^post18, i6^0'=i6^post18, ret17^0'=ret17^post18, ret28^0'=ret28^post18, ret_f19^0'=ret_f19^post18, ret_f212^0'=ret_f212^post18, ret_f215^0'=ret_f215^post18, tmp^0'=tmp^post18, val10^0'=val10^post18, val13^0'=val13^post18, (-val13^post18+val13^0 == 0 /\ -ret_f215^post18+ret_f215^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ i6^0-i6^post18 == 0 /\ 1+i6^0 <= 0 /\ ret17^0-ret17^post18 == 0 /\ -data18^post18+data18^0 == 0 /\ -ret28^post18+ret28^0 == 0 /\ ret_f212^0-ret_f212^post18 == 0 /\ ret_f19^0-ret_f19^post18 == 0 /\ val10^0-val10^post18 == 0 /\ -data16^post18+data16^0 == 0), cost: 1 14: l10 -> l8 : data16^0'=data16^post15, data18^0'=data18^post15, i6^0'=i6^post15, ret17^0'=ret17^post15, ret28^0'=ret28^post15, ret_f19^0'=ret_f19^post15, ret_f212^0'=ret_f212^post15, ret_f215^0'=ret_f215^post15, tmp^0'=tmp^post15, val10^0'=val10^post15, val13^0'=val13^post15, (0 == 0 /\ -val10^post15+data16^post15 == 0 /\ ret_f212^post15 == 0 /\ -ret_f212^post15+ret17^post15 == 0 /\ data18^0-data18^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ ret_f19^0-ret_f19^post15 == 0 /\ i6^0-i6^post15 == 0 /\ -ret_f215^post15+ret_f215^0 == 0 /\ -val13^post15+val13^0 == 0 /\ -ret28^post15+ret28^0 == 0), cost: 1 20: l12 -> l6 : data16^0'=data16^post19, data18^0'=data18^post19, i6^0'=i6^post19, ret17^0'=ret17^post19, ret28^0'=ret28^post19, ret_f19^0'=ret_f19^post19, ret_f212^0'=ret_f212^post19, ret_f215^0'=ret_f215^post19, tmp^0'=tmp^post19, val10^0'=val10^post19, val13^0'=val13^post19, (-ret_f215^post19+ret_f215^post20 == 0 /\ -data16^post20+data16^0 == 0 /\ -data18^post20+data18^0 == 0 /\ val13^0-val13^post20 == 0 /\ data18^post20-data18^post19 == 0 /\ -val10^post19+val10^post20 == 0 /\ val10^0-val10^post20 == 0 /\ -data16^post19+data16^post20 == 0 /\ -val13^post19+val13^post20 == 0 /\ ret_f212^0-ret_f212^post20 == 0 /\ -ret17^post19+ret17^post20 == 0 /\ ret_f215^0-ret_f215^post20 == 0 /\ -ret_f19^post20+ret_f19^0 == 0 /\ ret_f19^post20-ret_f19^post19 == 0 /\ tmp^post20-tmp^post19 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i6^0-i6^post20 == 0 /\ -ret28^post19+ret28^post20 == 0 /\ -ret_f212^post19+ret_f212^post20 == 0 /\ ret28^0-ret28^post20 == 0 /\ i6^post20-i6^post19 == 0 /\ ret17^0-ret17^post20 == 0), cost: 1 Eliminating location l11 by chaining: Applied chaining First rule: l12 -> l11 : data16^0'=data16^post20, data18^0'=data18^post20, i6^0'=i6^post20, ret17^0'=ret17^post20, ret28^0'=ret28^post20, ret_f19^0'=ret_f19^post20, ret_f212^0'=ret_f212^post20, ret_f215^0'=ret_f215^post20, tmp^0'=tmp^post20, val10^0'=val10^post20, val13^0'=val13^post20, (-data16^post20+data16^0 == 0 /\ -data18^post20+data18^0 == 0 /\ val13^0-val13^post20 == 0 /\ val10^0-val10^post20 == 0 /\ ret_f212^0-ret_f212^post20 == 0 /\ ret_f215^0-ret_f215^post20 == 0 /\ -ret_f19^post20+ret_f19^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i6^0-i6^post20 == 0 /\ ret28^0-ret28^post20 == 0 /\ ret17^0-ret17^post20 == 0), cost: 1 Second rule: l11 -> l6 : data16^0'=data16^post19, data18^0'=data18^post19, i6^0'=i6^post19, ret17^0'=ret17^post19, ret28^0'=ret28^post19, ret_f19^0'=ret_f19^post19, ret_f212^0'=ret_f212^post19, ret_f215^0'=ret_f215^post19, tmp^0'=tmp^post19, val10^0'=val10^post19, val13^0'=val13^post19, (ret_f19^0-ret_f19^post19 == 0 /\ data18^0-data18^post19 == 0 /\ tmp^0-tmp^post19 == 0 /\ ret_f212^0-ret_f212^post19 == 0 /\ -ret_f215^post19+ret_f215^0 == 0 /\ val10^0-val10^post19 == 0 /\ i6^0-i6^post19 == 0 /\ -ret28^post19+ret28^0 == 0 /\ ret17^0-ret17^post19 == 0 /\ -data16^post19+data16^0 == 0 /\ -val13^post19+val13^0 == 0), cost: 1 New rule: l12 -> l6 : data16^0'=data16^post19, data18^0'=data18^post19, i6^0'=i6^post19, ret17^0'=ret17^post19, ret28^0'=ret28^post19, ret_f19^0'=ret_f19^post19, ret_f212^0'=ret_f212^post19, ret_f215^0'=ret_f215^post19, tmp^0'=tmp^post19, val10^0'=val10^post19, val13^0'=val13^post19, (-ret_f215^post19+ret_f215^post20 == 0 /\ -data16^post20+data16^0 == 0 /\ -data18^post20+data18^0 == 0 /\ val13^0-val13^post20 == 0 /\ data18^post20-data18^post19 == 0 /\ -val10^post19+val10^post20 == 0 /\ val10^0-val10^post20 == 0 /\ -data16^post19+data16^post20 == 0 /\ -val13^post19+val13^post20 == 0 /\ ret_f212^0-ret_f212^post20 == 0 /\ -ret17^post19+ret17^post20 == 0 /\ ret_f215^0-ret_f215^post20 == 0 /\ -ret_f19^post20+ret_f19^0 == 0 /\ ret_f19^post20-ret_f19^post19 == 0 /\ tmp^post20-tmp^post19 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i6^0-i6^post20 == 0 /\ -ret28^post19+ret28^post20 == 0 /\ -ret_f212^post19+ret_f212^post20 == 0 /\ ret28^0-ret28^post20 == 0 /\ i6^post20-i6^post19 == 0 /\ ret17^0-ret17^post20 == 0), cost: 1 Applied deletion Removed the following rules: 18 19 Simplified Transitions Start location: l12 Program variables: data16^0 data18^0 i6^0 ret17^0 ret28^0 ret_f19^0 ret_f212^0 ret_f215^0 tmp^0 val10^0 val13^0 21: l0 -> l1 : i6^0'=i6^post1, T, cost: 1 22: l0 -> l2 : ret_f19^0'=1, T, cost: 1 34: l1 -> l9 : T, cost: 1 23: l2 -> l3 : tmp^0'=ret_f19^0, T, cost: 1 24: l4 -> l2 : ret_f19^0'=ret28^0, T, cost: 1 25: l5 -> l2 : ret_f19^0'=0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 26: l5 -> l4 : 1-ret28^0 <= 0, cost: 1 27: l5 -> l4 : 1+ret28^0 <= 0, cost: 1 28: l6 -> l0 : T, cost: 1 29: l6 -> l3 : T, cost: 1 30: l7 -> l2 : ret_f19^0'=ret17^0, T, cost: 1 31: l8 -> l1 : i6^0'=-1+i6^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 32: l8 -> l7 : 1-ret17^0 <= 0, cost: 1 33: l8 -> l7 : 1+ret17^0 <= 0, cost: 1 36: l9 -> l5 : data18^0'=val13^post16, ret28^0'=0, ret_f215^0'=0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 37: l9 -> l10 : 1-i6^0 <= 0, cost: 1 38: l9 -> l10 : 1+i6^0 <= 0, cost: 1 35: l10 -> l8 : data16^0'=val10^post15, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post15, T, cost: 1 39: l12 -> l6 : T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : data16^0'=data16^post1, data18^0'=data18^post1, i6^0'=i6^post1, ret17^0'=ret17^post1, ret28^0'=ret28^post1, ret_f19^0'=ret_f19^post1, ret_f212^0'=ret_f212^post1, ret_f215^0'=ret_f215^post1, tmp^0'=tmp^post1, val10^0'=val10^post1, val13^0'=val13^post1, (0 == 0 /\ -ret28^post1+ret28^0 == 0 /\ ret17^0-ret17^post1 == 0 /\ val13^0-val13^post1 == 0 /\ val10^0-val10^post1 == 0 /\ -data16^post1+data16^0 == 0 /\ ret_f212^0-ret_f212^post1 == 0 /\ -ret_f19^post1+ret_f19^0 == 0 /\ ret_f215^0-ret_f215^post1 == 0 /\ -data18^post1+data18^0 == 0 /\ -tmp^post1+tmp^0 == 0), cost: 1 New rule: l0 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^post1, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality ret28^post1 = ret28^0 propagated equality ret17^post1 = ret17^0 propagated equality val13^post1 = val13^0 propagated equality val10^post1 = val10^0 propagated equality data16^post1 = data16^0 propagated equality ret_f212^post1 = ret_f212^0 propagated equality ret_f19^post1 = ret_f19^0 propagated equality ret_f215^post1 = ret_f215^0 propagated equality data18^post1 = data18^0 propagated equality tmp^post1 = tmp^0 Simplified Guard Original rule: l0 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^post1, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l0 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^post1, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^post1, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l0 -> l1 : i6^0'=i6^post1, T, cost: 1 Propagated Equalities Original rule: l0 -> l2 : data16^0'=data16^post2, data18^0'=data18^post2, i6^0'=i6^post2, ret17^0'=ret17^post2, ret28^0'=ret28^post2, ret_f19^0'=ret_f19^post2, ret_f212^0'=ret_f212^post2, ret_f215^0'=ret_f215^post2, tmp^0'=tmp^post2, val10^0'=val10^post2, val13^0'=val13^post2, (-ret_f212^post2+ret_f212^0 == 0 /\ -ret17^post2+ret17^0 == 0 /\ -ret28^post2+ret28^0 == 0 /\ -data16^post2+data16^0 == 0 /\ -val13^post2+val13^0 == 0 /\ -1+ret_f19^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ val10^0-val10^post2 == 0 /\ -ret_f215^post2+ret_f215^0 == 0 /\ -data18^post2+data18^0 == 0 /\ i6^0-i6^post2 == 0), cost: 1 New rule: l0 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=1, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality ret_f212^post2 = ret_f212^0 propagated equality ret17^post2 = ret17^0 propagated equality ret28^post2 = ret28^0 propagated equality data16^post2 = data16^0 propagated equality val13^post2 = val13^0 propagated equality ret_f19^post2 = 1 propagated equality tmp^post2 = tmp^0 propagated equality val10^post2 = val10^0 propagated equality ret_f215^post2 = ret_f215^0 propagated equality data18^post2 = data18^0 propagated equality i6^post2 = i6^0 Simplified Guard Original rule: l0 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=1, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l0 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=1, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=1, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l0 -> l2 : ret_f19^0'=1, T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : data16^0'=data16^post3, data18^0'=data18^post3, i6^0'=i6^post3, ret17^0'=ret17^post3, ret28^0'=ret28^post3, ret_f19^0'=ret_f19^post3, ret_f212^0'=ret_f212^post3, ret_f215^0'=ret_f215^post3, tmp^0'=tmp^post3, val10^0'=val10^post3, val13^0'=val13^post3, (-data16^post3+data16^0 == 0 /\ tmp^post3-ret_f19^0 == 0 /\ -ret_f19^post3+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post3 == 0 /\ val13^0-val13^post3 == 0 /\ ret17^0-ret17^post3 == 0 /\ val10^0-val10^post3 == 0 /\ ret_f215^0-ret_f215^post3 == 0 /\ ret28^0-ret28^post3 == 0 /\ i6^0-i6^post3 == 0 /\ data18^0-data18^post3 == 0), cost: 1 New rule: l2 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=ret_f19^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality data16^post3 = data16^0 propagated equality tmp^post3 = ret_f19^0 propagated equality ret_f19^post3 = ret_f19^0 propagated equality ret_f212^post3 = ret_f212^0 propagated equality val13^post3 = val13^0 propagated equality ret17^post3 = ret17^0 propagated equality val10^post3 = val10^0 propagated equality ret_f215^post3 = ret_f215^0 propagated equality ret28^post3 = ret28^0 propagated equality i6^post3 = i6^0 propagated equality data18^post3 = data18^0 Simplified Guard Original rule: l2 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=ret_f19^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l2 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=ret_f19^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=ret_f19^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l2 -> l3 : tmp^0'=ret_f19^0, T, cost: 1 Propagated Equalities Original rule: l4 -> l2 : data16^0'=data16^post4, data18^0'=data18^post4, i6^0'=i6^post4, ret17^0'=ret17^post4, ret28^0'=ret28^post4, ret_f19^0'=ret_f19^post4, ret_f212^0'=ret_f212^post4, ret_f215^0'=ret_f215^post4, tmp^0'=tmp^post4, val10^0'=val10^post4, val13^0'=val13^post4, (tmp^0-tmp^post4 == 0 /\ i6^0-i6^post4 == 0 /\ val10^0-val10^post4 == 0 /\ -ret17^post4+ret17^0 == 0 /\ -val13^post4+val13^0 == 0 /\ -data18^post4+data18^0 == 0 /\ -data16^post4+data16^0 == 0 /\ -ret28^0+ret_f19^post4 == 0 /\ ret_f212^0-ret_f212^post4 == 0 /\ -ret28^post4+ret28^0 == 0 /\ -ret_f215^post4+ret_f215^0 == 0), cost: 1 New rule: l4 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret28^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality tmp^post4 = tmp^0 propagated equality i6^post4 = i6^0 propagated equality val10^post4 = val10^0 propagated equality ret17^post4 = ret17^0 propagated equality val13^post4 = val13^0 propagated equality data18^post4 = data18^0 propagated equality data16^post4 = data16^0 propagated equality ret_f19^post4 = ret28^0 propagated equality ret_f212^post4 = ret_f212^0 propagated equality ret28^post4 = ret28^0 propagated equality ret_f215^post4 = ret_f215^0 Simplified Guard Original rule: l4 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret28^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l4 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret28^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret28^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l4 -> l2 : ret_f19^0'=ret28^0, T, cost: 1 made implied equalities explicit Original rule: l5 -> l2 : data16^0'=data16^post5, data18^0'=data18^post5, i6^0'=i6^post5, ret17^0'=ret17^post5, ret28^0'=ret28^post5, ret_f19^0'=ret_f19^post5, ret_f212^0'=ret_f212^post5, ret_f215^0'=ret_f215^post5, tmp^0'=tmp^post5, val10^0'=val10^post5, val13^0'=val13^post5, (ret_f19^post5 == 0 /\ ret_f212^0-ret_f212^post5 == 0 /\ val10^0-val10^post5 == 0 /\ -val13^post5+val13^0 == 0 /\ i6^0-i6^post5 == 0 /\ -data18^post5+data18^0 == 0 /\ -data16^post5+data16^0 == 0 /\ -ret28^0 <= 0 /\ ret_f215^0-ret_f215^post5 == 0 /\ -ret28^post5+ret28^0 == 0 /\ ret17^0-ret17^post5 == 0 /\ ret28^0 <= 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 New rule: l5 -> l2 : data16^0'=data16^post5, data18^0'=data18^post5, i6^0'=i6^post5, ret17^0'=ret17^post5, ret28^0'=ret28^post5, ret_f19^0'=ret_f19^post5, ret_f212^0'=ret_f212^post5, ret_f215^0'=ret_f215^post5, tmp^0'=tmp^post5, val10^0'=val10^post5, val13^0'=val13^post5, (ret_f19^post5 == 0 /\ ret_f212^0-ret_f212^post5 == 0 /\ val10^0-val10^post5 == 0 /\ -val13^post5+val13^0 == 0 /\ i6^0-i6^post5 == 0 /\ -data18^post5+data18^0 == 0 /\ -data16^post5+data16^0 == 0 /\ -ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret_f215^0-ret_f215^post5 == 0 /\ -ret28^post5+ret28^0 == 0 /\ ret17^0-ret17^post5 == 0 /\ ret28^0 <= 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 Propagated Equalities Original rule: l5 -> l2 : data16^0'=data16^post5, data18^0'=data18^post5, i6^0'=i6^post5, ret17^0'=ret17^post5, ret28^0'=ret28^post5, ret_f19^0'=ret_f19^post5, ret_f212^0'=ret_f212^post5, ret_f215^0'=ret_f215^post5, tmp^0'=tmp^post5, val10^0'=val10^post5, val13^0'=val13^post5, (ret_f19^post5 == 0 /\ ret_f212^0-ret_f212^post5 == 0 /\ val10^0-val10^post5 == 0 /\ -val13^post5+val13^0 == 0 /\ i6^0-i6^post5 == 0 /\ -data18^post5+data18^0 == 0 /\ -data16^post5+data16^0 == 0 /\ -ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret_f215^0-ret_f215^post5 == 0 /\ -ret28^post5+ret28^0 == 0 /\ ret17^0-ret17^post5 == 0 /\ ret28^0 <= 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 New rule: l5 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ -ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 propagated equality ret_f19^post5 = 0 propagated equality ret_f212^post5 = ret_f212^0 propagated equality val10^post5 = val10^0 propagated equality val13^post5 = val13^0 propagated equality i6^post5 = i6^0 propagated equality data18^post5 = data18^0 propagated equality data16^post5 = data16^0 propagated equality ret_f215^post5 = ret_f215^0 propagated equality ret28^post5 = ret28^0 propagated equality ret17^post5 = ret17^0 propagated equality tmp^post5 = tmp^0 Simplified Guard Original rule: l5 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ -ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 New rule: l5 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 made implied equalities explicit Original rule: l5 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 New rule: l5 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l5 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 New rule: l5 -> l2 : ret_f19^0'=0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 Propagated Equalities Original rule: l5 -> l4 : data16^0'=data16^post6, data18^0'=data18^post6, i6^0'=i6^post6, ret17^0'=ret17^post6, ret28^0'=ret28^post6, ret_f19^0'=ret_f19^post6, ret_f212^0'=ret_f212^post6, ret_f215^0'=ret_f215^post6, tmp^0'=tmp^post6, val10^0'=val10^post6, val13^0'=val13^post6, (ret17^0-ret17^post6 == 0 /\ -ret_f215^post6+ret_f215^0 == 0 /\ data18^0-data18^post6 == 0 /\ tmp^0-tmp^post6 == 0 /\ ret_f19^0-ret_f19^post6 == 0 /\ ret_f212^0-ret_f212^post6 == 0 /\ val10^0-val10^post6 == 0 /\ -data16^post6+data16^0 == 0 /\ i6^0-i6^post6 == 0 /\ 1-ret28^0 <= 0 /\ -ret28^post6+ret28^0 == 0 /\ -val13^post6+val13^0 == 0), cost: 1 New rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1-ret28^0 <= 0), cost: 1 propagated equality ret17^post6 = ret17^0 propagated equality ret_f215^post6 = ret_f215^0 propagated equality data18^post6 = data18^0 propagated equality tmp^post6 = tmp^0 propagated equality ret_f19^post6 = ret_f19^0 propagated equality ret_f212^post6 = ret_f212^0 propagated equality val10^post6 = val10^0 propagated equality data16^post6 = data16^0 propagated equality i6^post6 = i6^0 propagated equality ret28^post6 = ret28^0 propagated equality val13^post6 = val13^0 Simplified Guard Original rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1-ret28^0 <= 0), cost: 1 New rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1-ret28^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1-ret28^0 <= 0, cost: 1 New rule: l5 -> l4 : 1-ret28^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l4 : data16^0'=data16^post7, data18^0'=data18^post7, i6^0'=i6^post7, ret17^0'=ret17^post7, ret28^0'=ret28^post7, ret_f19^0'=ret_f19^post7, ret_f212^0'=ret_f212^post7, ret_f215^0'=ret_f215^post7, tmp^0'=tmp^post7, val10^0'=val10^post7, val13^0'=val13^post7, (-data16^post7+data16^0 == 0 /\ -data18^post7+data18^0 == 0 /\ 1+ret28^0 <= 0 /\ -ret_f19^post7+ret_f19^0 == 0 /\ ret28^0-ret28^post7 == 0 /\ val10^0-val10^post7 == 0 /\ val13^0-val13^post7 == 0 /\ -ret_f215^post7+ret_f215^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i6^0-i6^post7 == 0 /\ ret_f212^0-ret_f212^post7 == 0 /\ ret17^0-ret17^post7 == 0), cost: 1 New rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1+ret28^0 <= 0), cost: 1 propagated equality data16^post7 = data16^0 propagated equality data18^post7 = data18^0 propagated equality ret_f19^post7 = ret_f19^0 propagated equality ret28^post7 = ret28^0 propagated equality val10^post7 = val10^0 propagated equality val13^post7 = val13^0 propagated equality ret_f215^post7 = ret_f215^0 propagated equality tmp^post7 = tmp^0 propagated equality i6^post7 = i6^0 propagated equality ret_f212^post7 = ret_f212^0 propagated equality ret17^post7 = ret17^0 Simplified Guard Original rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1+ret28^0 <= 0), cost: 1 New rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1+ret28^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l4 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1+ret28^0 <= 0, cost: 1 New rule: l5 -> l4 : 1+ret28^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l0 : data16^0'=data16^post8, data18^0'=data18^post8, i6^0'=i6^post8, ret17^0'=ret17^post8, ret28^0'=ret28^post8, ret_f19^0'=ret_f19^post8, ret_f212^0'=ret_f212^post8, ret_f215^0'=ret_f215^post8, tmp^0'=tmp^post8, val10^0'=val10^post8, val13^0'=val13^post8, (-ret_f215^post8+ret_f215^0 == 0 /\ tmp^0-tmp^post8 == 0 /\ i6^0-i6^post8 == 0 /\ -data18^post8+data18^0 == 0 /\ ret17^0-ret17^post8 == 0 /\ -ret28^post8+ret28^0 == 0 /\ ret_f19^0-ret_f19^post8 == 0 /\ -val13^post8+val13^0 == 0 /\ ret_f212^0-ret_f212^post8 == 0 /\ val10^0-val10^post8 == 0 /\ -data16^post8+data16^0 == 0), cost: 1 New rule: l6 -> l0 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality ret_f215^post8 = ret_f215^0 propagated equality tmp^post8 = tmp^0 propagated equality i6^post8 = i6^0 propagated equality data18^post8 = data18^0 propagated equality ret17^post8 = ret17^0 propagated equality ret28^post8 = ret28^0 propagated equality ret_f19^post8 = ret_f19^0 propagated equality val13^post8 = val13^0 propagated equality ret_f212^post8 = ret_f212^0 propagated equality val10^post8 = val10^0 propagated equality data16^post8 = data16^0 Simplified Guard Original rule: l6 -> l0 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l6 -> l0 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l0 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l6 -> l0 : T, cost: 1 Propagated Equalities Original rule: l6 -> l3 : data16^0'=data16^post9, data18^0'=data18^post9, i6^0'=i6^post9, ret17^0'=ret17^post9, ret28^0'=ret28^post9, ret_f19^0'=ret_f19^post9, ret_f212^0'=ret_f212^post9, ret_f215^0'=ret_f215^post9, tmp^0'=tmp^post9, val10^0'=val10^post9, val13^0'=val13^post9, (-val13^post9+val13^0 == 0 /\ -i6^post9+i6^0 == 0 /\ ret17^0-ret17^post9 == 0 /\ -ret_f215^post9+ret_f215^0 == 0 /\ -ret_f19^post9+ret_f19^0 == 0 /\ -ret28^post9+ret28^0 == 0 /\ data18^0-data18^post9 == 0 /\ -data16^post9+data16^0 == 0 /\ val10^0-val10^post9 == 0 /\ ret_f212^0-ret_f212^post9 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 New rule: l6 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality val13^post9 = val13^0 propagated equality i6^post9 = i6^0 propagated equality ret17^post9 = ret17^0 propagated equality ret_f215^post9 = ret_f215^0 propagated equality ret_f19^post9 = ret_f19^0 propagated equality ret28^post9 = ret28^0 propagated equality data18^post9 = data18^0 propagated equality data16^post9 = data16^0 propagated equality val10^post9 = val10^0 propagated equality ret_f212^post9 = ret_f212^0 propagated equality tmp^post9 = tmp^0 Simplified Guard Original rule: l6 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l6 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l3 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l6 -> l3 : T, cost: 1 Propagated Equalities Original rule: l7 -> l2 : data16^0'=data16^post10, data18^0'=data18^post10, i6^0'=i6^post10, ret17^0'=ret17^post10, ret28^0'=ret28^post10, ret_f19^0'=ret_f19^post10, ret_f212^0'=ret_f212^post10, ret_f215^0'=ret_f215^post10, tmp^0'=tmp^post10, val10^0'=val10^post10, val13^0'=val13^post10, (-val13^post10+val13^0 == 0 /\ -ret_f215^post10+ret_f215^0 == 0 /\ ret_f212^0-ret_f212^post10 == 0 /\ val10^0-val10^post10 == 0 /\ -ret17^0+ret_f19^post10 == 0 /\ -data16^post10+data16^0 == 0 /\ i6^0-i6^post10 == 0 /\ -ret28^post10+ret28^0 == 0 /\ -ret17^post10+ret17^0 == 0 /\ tmp^0-tmp^post10 == 0 /\ -data18^post10+data18^0 == 0), cost: 1 New rule: l7 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret17^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality val13^post10 = val13^0 propagated equality ret_f215^post10 = ret_f215^0 propagated equality ret_f212^post10 = ret_f212^0 propagated equality val10^post10 = val10^0 propagated equality ret_f19^post10 = ret17^0 propagated equality data16^post10 = data16^0 propagated equality i6^post10 = i6^0 propagated equality ret28^post10 = ret28^0 propagated equality ret17^post10 = ret17^0 propagated equality tmp^post10 = tmp^0 propagated equality data18^post10 = data18^0 Simplified Guard Original rule: l7 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret17^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l7 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret17^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l2 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret17^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l7 -> l2 : ret_f19^0'=ret17^0, T, cost: 1 made implied equalities explicit Original rule: l8 -> l1 : data16^0'=data16^post11, data18^0'=data18^post11, i6^0'=i6^post11, ret17^0'=ret17^post11, ret28^0'=ret28^post11, ret_f19^0'=ret_f19^post11, ret_f212^0'=ret_f212^post11, ret_f215^0'=ret_f215^post11, tmp^0'=tmp^post11, val10^0'=val10^post11, val13^0'=val13^post11, (-tmp^post11+tmp^0 == 0 /\ -ret_f19^post11+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post11 == 0 /\ ret17^0 <= 0 /\ val13^0-val13^post11 == 0 /\ val10^0-val10^post11 == 0 /\ -ret17^0 <= 0 /\ -data16^post11+data16^0 == 0 /\ ret17^0-ret17^post11 == 0 /\ 1-i6^0+i6^post11 == 0 /\ ret_f215^0-ret_f215^post11 == 0 /\ data18^0-data18^post11 == 0 /\ ret28^0-ret28^post11 == 0), cost: 1 New rule: l8 -> l1 : data16^0'=data16^post11, data18^0'=data18^post11, i6^0'=i6^post11, ret17^0'=ret17^post11, ret28^0'=ret28^post11, ret_f19^0'=ret_f19^post11, ret_f212^0'=ret_f212^post11, ret_f215^0'=ret_f215^post11, tmp^0'=tmp^post11, val10^0'=val10^post11, val13^0'=val13^post11, (-tmp^post11+tmp^0 == 0 /\ -ret_f19^post11+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post11 == 0 /\ ret17^0 <= 0 /\ ret17^0 == 0 /\ val13^0-val13^post11 == 0 /\ val10^0-val10^post11 == 0 /\ -ret17^0 <= 0 /\ -data16^post11+data16^0 == 0 /\ ret17^0-ret17^post11 == 0 /\ 1-i6^0+i6^post11 == 0 /\ ret_f215^0-ret_f215^post11 == 0 /\ data18^0-data18^post11 == 0 /\ ret28^0-ret28^post11 == 0), cost: 1 Propagated Equalities Original rule: l8 -> l1 : data16^0'=data16^post11, data18^0'=data18^post11, i6^0'=i6^post11, ret17^0'=ret17^post11, ret28^0'=ret28^post11, ret_f19^0'=ret_f19^post11, ret_f212^0'=ret_f212^post11, ret_f215^0'=ret_f215^post11, tmp^0'=tmp^post11, val10^0'=val10^post11, val13^0'=val13^post11, (-tmp^post11+tmp^0 == 0 /\ -ret_f19^post11+ret_f19^0 == 0 /\ ret_f212^0-ret_f212^post11 == 0 /\ ret17^0 <= 0 /\ ret17^0 == 0 /\ val13^0-val13^post11 == 0 /\ val10^0-val10^post11 == 0 /\ -ret17^0 <= 0 /\ -data16^post11+data16^0 == 0 /\ ret17^0-ret17^post11 == 0 /\ 1-i6^0+i6^post11 == 0 /\ ret_f215^0-ret_f215^post11 == 0 /\ data18^0-data18^post11 == 0 /\ ret28^0-ret28^post11 == 0), cost: 1 New rule: l8 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=-1+i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 propagated equality tmp^post11 = tmp^0 propagated equality ret_f19^post11 = ret_f19^0 propagated equality ret_f212^post11 = ret_f212^0 propagated equality val13^post11 = val13^0 propagated equality val10^post11 = val10^0 propagated equality data16^post11 = data16^0 propagated equality ret17^post11 = ret17^0 propagated equality i6^post11 = -1+i6^0 propagated equality ret_f215^post11 = ret_f215^0 propagated equality data18^post11 = data18^0 propagated equality ret28^post11 = ret28^0 Simplified Guard Original rule: l8 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=-1+i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 New rule: l8 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=-1+i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 made implied equalities explicit Original rule: l8 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=-1+i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 New rule: l8 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=-1+i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l8 -> l1 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=-1+i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 New rule: l8 -> l1 : i6^0'=-1+i6^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 Propagated Equalities Original rule: l8 -> l7 : data16^0'=data16^post12, data18^0'=data18^post12, i6^0'=i6^post12, ret17^0'=ret17^post12, ret28^0'=ret28^post12, ret_f19^0'=ret_f19^post12, ret_f212^0'=ret_f212^post12, ret_f215^0'=ret_f215^post12, tmp^0'=tmp^post12, val10^0'=val10^post12, val13^0'=val13^post12, (-ret_f212^post12+ret_f212^0 == 0 /\ -ret17^post12+ret17^0 == 0 /\ -ret28^post12+ret28^0 == 0 /\ 1-ret17^0 <= 0 /\ -data16^post12+data16^0 == 0 /\ -val13^post12+val13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ val10^0-val10^post12 == 0 /\ ret_f19^0-ret_f19^post12 == 0 /\ i6^0-i6^post12 == 0 /\ -ret_f215^post12+ret_f215^0 == 0 /\ -data18^post12+data18^0 == 0), cost: 1 New rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1-ret17^0 <= 0), cost: 1 propagated equality ret_f212^post12 = ret_f212^0 propagated equality ret17^post12 = ret17^0 propagated equality ret28^post12 = ret28^0 propagated equality data16^post12 = data16^0 propagated equality val13^post12 = val13^0 propagated equality tmp^post12 = tmp^0 propagated equality val10^post12 = val10^0 propagated equality ret_f19^post12 = ret_f19^0 propagated equality i6^post12 = i6^0 propagated equality ret_f215^post12 = ret_f215^0 propagated equality data18^post12 = data18^0 Simplified Guard Original rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1-ret17^0 <= 0), cost: 1 New rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1-ret17^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1-ret17^0 <= 0, cost: 1 New rule: l8 -> l7 : 1-ret17^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l7 : data16^0'=data16^post13, data18^0'=data18^post13, i6^0'=i6^post13, ret17^0'=ret17^post13, ret28^0'=ret28^post13, ret_f19^0'=ret_f19^post13, ret_f212^0'=ret_f212^post13, ret_f215^0'=ret_f215^post13, tmp^0'=tmp^post13, val10^0'=val10^post13, val13^0'=val13^post13, (tmp^0-tmp^post13 == 0 /\ val10^0-val10^post13 == 0 /\ -ret28^post13+ret28^0 == 0 /\ -val13^post13+val13^0 == 0 /\ ret17^0-ret17^post13 == 0 /\ ret_f212^0-ret_f212^post13 == 0 /\ -data16^post13+data16^0 == 0 /\ 1+ret17^0 <= 0 /\ -ret_f215^post13+ret_f215^0 == 0 /\ data18^0-data18^post13 == 0 /\ -ret_f19^post13+ret_f19^0 == 0 /\ -i6^post13+i6^0 == 0), cost: 1 New rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1+ret17^0 <= 0), cost: 1 propagated equality tmp^post13 = tmp^0 propagated equality val10^post13 = val10^0 propagated equality ret28^post13 = ret28^0 propagated equality val13^post13 = val13^0 propagated equality ret17^post13 = ret17^0 propagated equality ret_f212^post13 = ret_f212^0 propagated equality data16^post13 = data16^0 propagated equality ret_f215^post13 = ret_f215^0 propagated equality data18^post13 = data18^0 propagated equality ret_f19^post13 = ret_f19^0 propagated equality i6^post13 = i6^0 Simplified Guard Original rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1+ret17^0 <= 0), cost: 1 New rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1+ret17^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1+ret17^0 <= 0, cost: 1 New rule: l8 -> l7 : 1+ret17^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l9 : data16^0'=data16^post14, data18^0'=data18^post14, i6^0'=i6^post14, ret17^0'=ret17^post14, ret28^0'=ret28^post14, ret_f19^0'=ret_f19^post14, ret_f212^0'=ret_f212^post14, ret_f215^0'=ret_f215^post14, tmp^0'=tmp^post14, val10^0'=val10^post14, val13^0'=val13^post14, (tmp^0-tmp^post14 == 0 /\ ret17^0-ret17^post14 == 0 /\ -ret_f215^post14+ret_f215^0 == 0 /\ ret_f212^0-ret_f212^post14 == 0 /\ -val13^post14+val13^0 == 0 /\ -ret_f19^post14+ret_f19^0 == 0 /\ i6^0-i6^post14 == 0 /\ -data16^post14+data16^0 == 0 /\ -data18^post14+data18^0 == 0 /\ val10^0-val10^post14 == 0 /\ -ret28^post14+ret28^0 == 0), cost: 1 New rule: l1 -> l9 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality tmp^post14 = tmp^0 propagated equality ret17^post14 = ret17^0 propagated equality ret_f215^post14 = ret_f215^0 propagated equality ret_f212^post14 = ret_f212^0 propagated equality val13^post14 = val13^0 propagated equality ret_f19^post14 = ret_f19^0 propagated equality i6^post14 = i6^0 propagated equality data16^post14 = data16^0 propagated equality data18^post14 = data18^0 propagated equality val10^post14 = val10^0 propagated equality ret28^post14 = ret28^0 Simplified Guard Original rule: l1 -> l9 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l1 -> l9 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l9 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l1 -> l9 : T, cost: 1 Propagated Equalities Original rule: l10 -> l8 : data16^0'=data16^post15, data18^0'=data18^post15, i6^0'=i6^post15, ret17^0'=ret17^post15, ret28^0'=ret28^post15, ret_f19^0'=ret_f19^post15, ret_f212^0'=ret_f212^post15, ret_f215^0'=ret_f215^post15, tmp^0'=tmp^post15, val10^0'=val10^post15, val13^0'=val13^post15, (0 == 0 /\ -val10^post15+data16^post15 == 0 /\ ret_f212^post15 == 0 /\ -ret_f212^post15+ret17^post15 == 0 /\ data18^0-data18^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ ret_f19^0-ret_f19^post15 == 0 /\ i6^0-i6^post15 == 0 /\ -ret_f215^post15+ret_f215^0 == 0 /\ -val13^post15+val13^0 == 0 /\ -ret28^post15+ret28^0 == 0), cost: 1 New rule: l10 -> l8 : data16^0'=val10^post15, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^post15, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality data16^post15 = val10^post15 propagated equality ret_f212^post15 = 0 propagated equality ret17^post15 = 0 propagated equality data18^post15 = data18^0 propagated equality tmp^post15 = tmp^0 propagated equality ret_f19^post15 = ret_f19^0 propagated equality i6^post15 = i6^0 propagated equality ret_f215^post15 = ret_f215^0 propagated equality val13^post15 = val13^0 propagated equality ret28^post15 = ret28^0 Simplified Guard Original rule: l10 -> l8 : data16^0'=val10^post15, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^post15, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l10 -> l8 : data16^0'=val10^post15, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^post15, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l10 -> l8 : data16^0'=val10^post15, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^post15, val13^0'=val13^0, T, cost: 1 New rule: l10 -> l8 : data16^0'=val10^post15, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post15, T, cost: 1 made implied equalities explicit Original rule: l9 -> l5 : data16^0'=data16^post16, data18^0'=data18^post16, i6^0'=i6^post16, ret17^0'=ret17^post16, ret28^0'=ret28^post16, ret_f19^0'=ret_f19^post16, ret_f212^0'=ret_f212^post16, ret_f215^0'=ret_f215^post16, tmp^0'=tmp^post16, val10^0'=val10^post16, val13^0'=val13^post16, (0 == 0 /\ i6^0-i6^post16 == 0 /\ -val13^post16+data18^post16 == 0 /\ ret_f215^post16 == 0 /\ i6^0 <= 0 /\ -ret17^post16+ret17^0 == 0 /\ -i6^0 <= 0 /\ val10^0-val10^post16 == 0 /\ -ret_f215^post16+ret28^post16 == 0 /\ -data16^post16+data16^0 == 0 /\ ret_f212^0-ret_f212^post16 == 0 /\ ret_f19^0-ret_f19^post16 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 New rule: l9 -> l5 : data16^0'=data16^post16, data18^0'=data18^post16, i6^0'=i6^post16, ret17^0'=ret17^post16, ret28^0'=ret28^post16, ret_f19^0'=ret_f19^post16, ret_f212^0'=ret_f212^post16, ret_f215^0'=ret_f215^post16, tmp^0'=tmp^post16, val10^0'=val10^post16, val13^0'=val13^post16, (0 == 0 /\ i6^0-i6^post16 == 0 /\ -val13^post16+data18^post16 == 0 /\ ret_f215^post16 == 0 /\ i6^0 <= 0 /\ i6^0 == 0 /\ -ret17^post16+ret17^0 == 0 /\ -i6^0 <= 0 /\ val10^0-val10^post16 == 0 /\ -ret_f215^post16+ret28^post16 == 0 /\ -data16^post16+data16^0 == 0 /\ ret_f212^0-ret_f212^post16 == 0 /\ ret_f19^0-ret_f19^post16 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 Propagated Equalities Original rule: l9 -> l5 : data16^0'=data16^post16, data18^0'=data18^post16, i6^0'=i6^post16, ret17^0'=ret17^post16, ret28^0'=ret28^post16, ret_f19^0'=ret_f19^post16, ret_f212^0'=ret_f212^post16, ret_f215^0'=ret_f215^post16, tmp^0'=tmp^post16, val10^0'=val10^post16, val13^0'=val13^post16, (0 == 0 /\ i6^0-i6^post16 == 0 /\ -val13^post16+data18^post16 == 0 /\ ret_f215^post16 == 0 /\ i6^0 <= 0 /\ i6^0 == 0 /\ -ret17^post16+ret17^0 == 0 /\ -i6^0 <= 0 /\ val10^0-val10^post16 == 0 /\ -ret_f215^post16+ret28^post16 == 0 /\ -data16^post16+data16^0 == 0 /\ ret_f212^0-ret_f212^post16 == 0 /\ ret_f19^0-ret_f19^post16 == 0 /\ tmp^0-tmp^post16 == 0), cost: 1 New rule: l9 -> l5 : data16^0'=data16^0, data18^0'=val13^post16, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^post16, (0 == 0 /\ i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 propagated equality i6^post16 = i6^0 propagated equality data18^post16 = val13^post16 propagated equality ret_f215^post16 = 0 propagated equality ret17^post16 = ret17^0 propagated equality val10^post16 = val10^0 propagated equality ret28^post16 = 0 propagated equality data16^post16 = data16^0 propagated equality ret_f212^post16 = ret_f212^0 propagated equality ret_f19^post16 = ret_f19^0 propagated equality tmp^post16 = tmp^0 Simplified Guard Original rule: l9 -> l5 : data16^0'=data16^0, data18^0'=val13^post16, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^post16, (0 == 0 /\ i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 New rule: l9 -> l5 : data16^0'=data16^0, data18^0'=val13^post16, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 made implied equalities explicit Original rule: l9 -> l5 : data16^0'=data16^0, data18^0'=val13^post16, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 New rule: l9 -> l5 : data16^0'=data16^0, data18^0'=val13^post16, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l9 -> l5 : data16^0'=data16^0, data18^0'=val13^post16, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 New rule: l9 -> l5 : data18^0'=val13^post16, ret28^0'=0, ret_f215^0'=0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 Propagated Equalities Original rule: l9 -> l10 : data16^0'=data16^post17, data18^0'=data18^post17, i6^0'=i6^post17, ret17^0'=ret17^post17, ret28^0'=ret28^post17, ret_f19^0'=ret_f19^post17, ret_f212^0'=ret_f212^post17, ret_f215^0'=ret_f215^post17, tmp^0'=tmp^post17, val10^0'=val10^post17, val13^0'=val13^post17, (ret17^0-ret17^post17 == 0 /\ -ret28^post17+ret28^0 == 0 /\ 1-i6^0 <= 0 /\ val10^0-val10^post17 == 0 /\ val13^0-val13^post17 == 0 /\ data18^0-data18^post17 == 0 /\ -ret_f215^post17+ret_f215^0 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -i6^post17+i6^0 == 0 /\ -data16^post17+data16^0 == 0 /\ ret_f212^0-ret_f212^post17 == 0 /\ -ret_f19^post17+ret_f19^0 == 0), cost: 1 New rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1-i6^0 <= 0), cost: 1 propagated equality ret17^post17 = ret17^0 propagated equality ret28^post17 = ret28^0 propagated equality val10^post17 = val10^0 propagated equality val13^post17 = val13^0 propagated equality data18^post17 = data18^0 propagated equality ret_f215^post17 = ret_f215^0 propagated equality tmp^post17 = tmp^0 propagated equality i6^post17 = i6^0 propagated equality data16^post17 = data16^0 propagated equality ret_f212^post17 = ret_f212^0 propagated equality ret_f19^post17 = ret_f19^0 Simplified Guard Original rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1-i6^0 <= 0), cost: 1 New rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1-i6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1-i6^0 <= 0, cost: 1 New rule: l9 -> l10 : 1-i6^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l10 : data16^0'=data16^post18, data18^0'=data18^post18, i6^0'=i6^post18, ret17^0'=ret17^post18, ret28^0'=ret28^post18, ret_f19^0'=ret_f19^post18, ret_f212^0'=ret_f212^post18, ret_f215^0'=ret_f215^post18, tmp^0'=tmp^post18, val10^0'=val10^post18, val13^0'=val13^post18, (-val13^post18+val13^0 == 0 /\ -ret_f215^post18+ret_f215^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ i6^0-i6^post18 == 0 /\ 1+i6^0 <= 0 /\ ret17^0-ret17^post18 == 0 /\ -data18^post18+data18^0 == 0 /\ -ret28^post18+ret28^0 == 0 /\ ret_f212^0-ret_f212^post18 == 0 /\ ret_f19^0-ret_f19^post18 == 0 /\ val10^0-val10^post18 == 0 /\ -data16^post18+data16^0 == 0), cost: 1 New rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1+i6^0 <= 0), cost: 1 propagated equality val13^post18 = val13^0 propagated equality ret_f215^post18 = ret_f215^0 propagated equality tmp^post18 = tmp^0 propagated equality i6^post18 = i6^0 propagated equality ret17^post18 = ret17^0 propagated equality data18^post18 = data18^0 propagated equality ret28^post18 = ret28^0 propagated equality ret_f212^post18 = ret_f212^0 propagated equality ret_f19^post18 = ret_f19^0 propagated equality val10^post18 = val10^0 propagated equality data16^post18 = data16^0 Simplified Guard Original rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, (0 == 0 /\ 1+i6^0 <= 0), cost: 1 New rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1+i6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l10 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 1+i6^0 <= 0, cost: 1 New rule: l9 -> l10 : 1+i6^0 <= 0, cost: 1 Propagated Equalities Original rule: l12 -> l6 : data16^0'=data16^post19, data18^0'=data18^post19, i6^0'=i6^post19, ret17^0'=ret17^post19, ret28^0'=ret28^post19, ret_f19^0'=ret_f19^post19, ret_f212^0'=ret_f212^post19, ret_f215^0'=ret_f215^post19, tmp^0'=tmp^post19, val10^0'=val10^post19, val13^0'=val13^post19, (-ret_f215^post19+ret_f215^post20 == 0 /\ -data16^post20+data16^0 == 0 /\ -data18^post20+data18^0 == 0 /\ val13^0-val13^post20 == 0 /\ data18^post20-data18^post19 == 0 /\ -val10^post19+val10^post20 == 0 /\ val10^0-val10^post20 == 0 /\ -data16^post19+data16^post20 == 0 /\ -val13^post19+val13^post20 == 0 /\ ret_f212^0-ret_f212^post20 == 0 /\ -ret17^post19+ret17^post20 == 0 /\ ret_f215^0-ret_f215^post20 == 0 /\ -ret_f19^post20+ret_f19^0 == 0 /\ ret_f19^post20-ret_f19^post19 == 0 /\ tmp^post20-tmp^post19 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i6^0-i6^post20 == 0 /\ -ret28^post19+ret28^post20 == 0 /\ -ret_f212^post19+ret_f212^post20 == 0 /\ ret28^0-ret28^post20 == 0 /\ i6^post20-i6^post19 == 0 /\ ret17^0-ret17^post20 == 0), cost: 1 New rule: l12 -> l6 : data16^0'=data16^post20, data18^0'=data18^post20, i6^0'=i6^post20, ret17^0'=ret17^post20, ret28^0'=ret28^post20, ret_f19^0'=ret_f19^post20, ret_f212^0'=ret_f212^post20, ret_f215^0'=ret_f215^post20, tmp^0'=tmp^post20, val10^0'=val10^post20, val13^0'=val13^post20, (0 == 0 /\ -data16^post20+data16^0 == 0 /\ -data18^post20+data18^0 == 0 /\ val13^0-val13^post20 == 0 /\ val10^0-val10^post20 == 0 /\ ret_f212^0-ret_f212^post20 == 0 /\ ret_f215^0-ret_f215^post20 == 0 /\ -ret_f19^post20+ret_f19^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i6^0-i6^post20 == 0 /\ ret28^0-ret28^post20 == 0 /\ ret17^0-ret17^post20 == 0), cost: 1 propagated equality ret_f215^post19 = ret_f215^post20 propagated equality data18^post19 = data18^post20 propagated equality val10^post19 = val10^post20 propagated equality data16^post19 = data16^post20 propagated equality val13^post19 = val13^post20 propagated equality ret17^post19 = ret17^post20 propagated equality ret_f19^post19 = ret_f19^post20 propagated equality tmp^post19 = tmp^post20 propagated equality ret28^post19 = ret28^post20 propagated equality ret_f212^post19 = ret_f212^post20 propagated equality i6^post19 = i6^post20 Propagated Equalities Original rule: l12 -> l6 : data16^0'=data16^post20, data18^0'=data18^post20, i6^0'=i6^post20, ret17^0'=ret17^post20, ret28^0'=ret28^post20, ret_f19^0'=ret_f19^post20, ret_f212^0'=ret_f212^post20, ret_f215^0'=ret_f215^post20, tmp^0'=tmp^post20, val10^0'=val10^post20, val13^0'=val13^post20, (0 == 0 /\ -data16^post20+data16^0 == 0 /\ -data18^post20+data18^0 == 0 /\ val13^0-val13^post20 == 0 /\ val10^0-val10^post20 == 0 /\ ret_f212^0-ret_f212^post20 == 0 /\ ret_f215^0-ret_f215^post20 == 0 /\ -ret_f19^post20+ret_f19^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i6^0-i6^post20 == 0 /\ ret28^0-ret28^post20 == 0 /\ ret17^0-ret17^post20 == 0), cost: 1 New rule: l12 -> l6 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 propagated equality data16^post20 = data16^0 propagated equality data18^post20 = data18^0 propagated equality val13^post20 = val13^0 propagated equality val10^post20 = val10^0 propagated equality ret_f212^post20 = ret_f212^0 propagated equality ret_f215^post20 = ret_f215^0 propagated equality ret_f19^post20 = ret_f19^0 propagated equality tmp^post20 = tmp^0 propagated equality i6^post20 = i6^0 propagated equality ret28^post20 = ret28^0 propagated equality ret17^post20 = ret17^0 Simplified Guard Original rule: l12 -> l6 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, 0 == 0, cost: 1 New rule: l12 -> l6 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 Removed Trivial Updates Original rule: l12 -> l6 : data16^0'=data16^0, data18^0'=data18^0, i6^0'=i6^0, ret17^0'=ret17^0, ret28^0'=ret28^0, ret_f19^0'=ret_f19^0, ret_f212^0'=ret_f212^0, ret_f215^0'=ret_f215^0, tmp^0'=tmp^0, val10^0'=val10^0, val13^0'=val13^0, T, cost: 1 New rule: l12 -> l6 : T, cost: 1 Step with 39 Trace 39[T] Blocked [{}, {}] Step with 28 Trace 39[T], 28[T] Blocked [{}, {}, {}] Step with 21 Trace 39[T], 28[T], 21[T] Blocked [{}, {}, {}, {}] Step with 34 Trace 39[T], 28[T], 21[T], 34[T] Blocked [{}, {}, {}, {}, {}] Step with 36 Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}] Step with 25 Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {}] Step with 23 Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)], 23[T] Blocked [{}, {}, {}, {}, {}, {}, {}, {}] Backtrack Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {23[T]}] Backtrack Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {25[T]}] Backtrack Trace 39[T], 28[T], 21[T], 34[T] Blocked [{}, {}, {}, {}, {36[T]}] Step with 37 Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)] Blocked [{}, {}, {}, {}, {36[T]}, {}] Step with 35 Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)], 35[T] Blocked [{}, {}, {}, {}, {36[T]}, {}, {}] Step with 31 Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)], 35[T], 31[(ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0)] Blocked [{}, {}, {}, {}, {36[T]}, {}, {32[T], 33[T]}, {}] Accelerate Start location: l12 Program variables: data16^0 data18^0 i6^0 ret17^0 ret28^0 ret_f19^0 ret_f212^0 ret_f215^0 tmp^0 val10^0 val13^0 21: l0 -> l1 : i6^0'=i6^post1, T, cost: 1 22: l0 -> l2 : ret_f19^0'=1, T, cost: 1 34: l1 -> l9 : T, cost: 1 40: l1 -> l1 : data16^0'=val10^post151, i6^0'=i6^0-n, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post151, (-1+n >= 0 /\ i6^0-n >= 0), cost: 1 23: l2 -> l3 : tmp^0'=ret_f19^0, T, cost: 1 24: l4 -> l2 : ret_f19^0'=ret28^0, T, cost: 1 25: l5 -> l2 : ret_f19^0'=0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 26: l5 -> l4 : 1-ret28^0 <= 0, cost: 1 27: l5 -> l4 : 1+ret28^0 <= 0, cost: 1 28: l6 -> l0 : T, cost: 1 29: l6 -> l3 : T, cost: 1 30: l7 -> l2 : ret_f19^0'=ret17^0, T, cost: 1 31: l8 -> l1 : i6^0'=-1+i6^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 32: l8 -> l7 : 1-ret17^0 <= 0, cost: 1 33: l8 -> l7 : 1+ret17^0 <= 0, cost: 1 36: l9 -> l5 : data18^0'=val13^post16, ret28^0'=0, ret_f215^0'=0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 37: l9 -> l10 : 1-i6^0 <= 0, cost: 1 38: l9 -> l10 : 1+i6^0 <= 0, cost: 1 35: l10 -> l8 : data16^0'=val10^post15, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post15, T, cost: 1 39: l12 -> l6 : T, cost: 1 Loop Acceleration Original rule: l1 -> l1 : data16^0'=val10^post151, i6^0'=-1+i6^0, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post151, 1-i6^0 <= 0, cost: 1 New rule: l1 -> l1 : data16^0'=val10^post151, i6^0'=i6^0-n, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post151, (-1+n >= 0 /\ i6^0-n >= 0), cost: 1 -1+i6^0 >= 0 [0]: montonic decrease yields i6^0-n >= 0 -1+i6^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+i6^0 >= 0) Replacement map: {-1+i6^0 >= 0 -> i6^0-n >= 0} Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)] Blocked [{}, {}, {}, {}, {40[T]}] Step with 34 Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T] Blocked [{}, {}, {}, {}, {40[T]}, {}] Step with 37 Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 37[(1-i6^0 <= 0)] Blocked [{}, {}, {}, {}, {40[T]}, {}, {}] Step with 35 Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 37[(1-i6^0 <= 0)], 35[T] Blocked [{}, {}, {}, {}, {40[T]}, {}, {}, {}] Step with 31 Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 37[(1-i6^0 <= 0)], 35[T], 31[(ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0)] Blocked [{}, {}, {}, {}, {40[T]}, {}, {}, {}, {}] Covered Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 37[(1-i6^0 <= 0)], 35[T] Blocked [{}, {}, {}, {}, {40[T]}, {}, {}, {31[T]}] Backtrack Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 37[(1-i6^0 <= 0)] Blocked [{}, {}, {}, {}, {40[T]}, {}, {35[T]}] Backtrack Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T] Blocked [{}, {}, {}, {}, {40[T]}, {37[T]}] Step with 36 Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)] Blocked [{}, {}, {}, {}, {40[T]}, {37[T], 38[T]}, {}] Step with 25 Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)] Blocked [{}, {}, {}, {}, {40[T]}, {37[T], 38[T]}, {}, {}] Step with 23 Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)], 23[T] Blocked [{}, {}, {}, {}, {40[T]}, {37[T], 38[T]}, {}, {}, {}] Backtrack Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)] Blocked [{}, {}, {}, {}, {40[T]}, {37[T], 38[T]}, {}, {23[T]}] Backtrack Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)] Blocked [{}, {}, {}, {}, {40[T]}, {37[T], 38[T]}, {25[T]}] Backtrack Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)], 34[T] Blocked [{}, {}, {}, {}, {40[T]}, {36[T], 37[T], 38[T]}] Backtrack Trace 39[T], 28[T], 21[T], 40[(-1+n >= 0 /\ i6^0-n >= 0)] Blocked [{}, {}, {}, {}, {34[T], 40[T]}] Backtrack Trace 39[T], 28[T], 21[T] Blocked [{}, {}, {}, {40[T]}] Step with 34 Trace 39[T], 28[T], 21[T], 34[T] Blocked [{}, {}, {}, {40[T]}, {}] Step with 36 Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {}, {}] Step with 25 Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {}, {}, {}] Step with 23 Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)], 23[T] Blocked [{}, {}, {}, {40[T]}, {}, {}, {}, {}] Backtrack Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)], 25[(-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {}, {}, {23[T]}] Backtrack Trace 39[T], 28[T], 21[T], 34[T], 36[(i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {}, {25[T]}] Backtrack Trace 39[T], 28[T], 21[T], 34[T] Blocked [{}, {}, {}, {40[T]}, {36[T]}] Step with 37 Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {36[T]}, {}] Step with 35 Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)], 35[T] Blocked [{}, {}, {}, {40[T]}, {36[T]}, {}, {}] Step with 31 Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)], 35[T], 31[(ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {36[T]}, {}, {}, {}] Covered Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)], 35[T] Blocked [{}, {}, {}, {40[T]}, {36[T]}, {}, {31[T]}] Backtrack Trace 39[T], 28[T], 21[T], 34[T], 37[(1-i6^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {36[T]}, {35[T]}] Backtrack Trace 39[T], 28[T], 21[T], 34[T] Blocked [{}, {}, {}, {40[T]}, {36[T], 37[T]}] Step with 38 Trace 39[T], 28[T], 21[T], 34[T], 38[(1+i6^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {36[T], 37[T]}, {}] Step with 35 Trace 39[T], 28[T], 21[T], 34[T], 38[(1+i6^0 <= 0)], 35[T] Blocked [{}, {}, {}, {40[T]}, {36[T], 37[T]}, {}, {}] Step with 31 Trace 39[T], 28[T], 21[T], 34[T], 38[(1+i6^0 <= 0)], 35[T], 31[(ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0)] Blocked [{}, {}, {}, {40[T]}, {36[T], 37[T]}, {}, {}, {}] Nonterm Start location: l12 Program variables: data16^0 data18^0 i6^0 ret17^0 ret28^0 ret_f19^0 ret_f212^0 ret_f215^0 tmp^0 val10^0 val13^0 21: l0 -> l1 : i6^0'=i6^post1, T, cost: 1 22: l0 -> l2 : ret_f19^0'=1, T, cost: 1 34: l1 -> l9 : T, cost: 1 40: l1 -> l1 : data16^0'=val10^post151, i6^0'=i6^0-n, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post151, (-1+n >= 0 /\ i6^0-n >= 0), cost: 1 41: l1 -> LoAT_sink : (-1+n2 >= 0 /\ -1-i6^0 >= 0), cost: NONTERM 42: l1 -> l1 : data16^0'=val10^post154, i6^0'=i6^0-n2, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post154, (-1+n2 >= 0 /\ -1-i6^0 >= 0), cost: 1 23: l2 -> l3 : tmp^0'=ret_f19^0, T, cost: 1 24: l4 -> l2 : ret_f19^0'=ret28^0, T, cost: 1 25: l5 -> l2 : ret_f19^0'=0, (-ret28^0 <= 0 /\ -ret28^0 == 0 /\ ret28^0 <= 0), cost: 1 26: l5 -> l4 : 1-ret28^0 <= 0, cost: 1 27: l5 -> l4 : 1+ret28^0 <= 0, cost: 1 28: l6 -> l0 : T, cost: 1 29: l6 -> l3 : T, cost: 1 30: l7 -> l2 : ret_f19^0'=ret17^0, T, cost: 1 31: l8 -> l1 : i6^0'=-1+i6^0, (ret17^0 <= 0 /\ ret17^0 == 0 /\ -ret17^0 <= 0), cost: 1 32: l8 -> l7 : 1-ret17^0 <= 0, cost: 1 33: l8 -> l7 : 1+ret17^0 <= 0, cost: 1 36: l9 -> l5 : data18^0'=val13^post16, ret28^0'=0, ret_f215^0'=0, val13^0'=val13^post16, (i6^0 <= 0 /\ i6^0 == 0 /\ -i6^0 <= 0), cost: 1 37: l9 -> l10 : 1-i6^0 <= 0, cost: 1 38: l9 -> l10 : 1+i6^0 <= 0, cost: 1 35: l10 -> l8 : data16^0'=val10^post15, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post15, T, cost: 1 39: l12 -> l6 : T, cost: 1 Certificate of Non-Termination Original rule: l1 -> l1 : data16^0'=val10^post154, i6^0'=-1+i6^0, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post154, 1+i6^0 <= 0, cost: 1 New rule: l1 -> LoAT_sink : (-1+n2 >= 0 /\ -1-i6^0 >= 0), cost: NONTERM -1-i6^0 >= 0 [0]: monotonic increase yields -1-i6^0 >= 0 Replacement map: {-1-i6^0 >= 0 -> -1-i6^0 >= 0} Loop Acceleration Original rule: l1 -> l1 : data16^0'=val10^post154, i6^0'=-1+i6^0, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post154, 1+i6^0 <= 0, cost: 1 New rule: l1 -> l1 : data16^0'=val10^post154, i6^0'=i6^0-n2, ret17^0'=0, ret_f212^0'=0, val10^0'=val10^post154, (-1+n2 >= 0 /\ -1-i6^0 >= 0), cost: 1 -1-i6^0 >= 0 [0]: monotonic increase yields -1-i6^0 >= 0 Replacement map: {-1-i6^0 >= 0 -> -1-i6^0 >= 0} Step with 41 Trace 39[T], 28[T], 21[T], 41[(-1+n2 >= 0 /\ -1-i6^0 >= 0)] Blocked [{}, {}, {}, {40[T]}, {41[T]}] Refute Counterexample [ data16^0=0 data18^0=0 i6^0=0 ret17^0=0 ret28^0=0 ret_f19^0=0 ret_f212^0=0 ret_f215^0=0 tmp^0=0 val10^0=0 val13^0=0 ] 39 [ data16^0=0 data18^0=0 i6^0=0 ret17^0=0 ret28^0=0 ret_f19^0=0 ret_f212^0=0 ret_f215^0=0 tmp^0=0 val10^0=0 val13^0=0 ] 28 [ data16^0=0 data18^0=0 i6^0=-1 ret17^0=0 ret28^0=0 ret_f19^0=0 ret_f212^0=0 ret_f215^0=0 tmp^0=0 val10^0=0 val13^0=0 ] 21 [ data16^0=0 data18^0=0 i6^0=0 ret17^0=0 ret28^0=0 ret_f19^0=0 ret_f212^0=0 ret_f215^0=0 tmp^0=0 val10^0=0 val13^0=0 ] 41 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b