WORST_CASE(Omega(0),?)

Initial ITS
Start location: l11
   0: l0 -> l1 : tmp^0'=tmp^post0, il^0'=il^post0, x4^0'=x4^post0, ret_foo7^0'=ret_foo7^post0, __const_10^0'=__const_10^post0, tmp___0^0'=tmp___0^post0, ret_foo5^0'=ret_foo5^post0, x6^0'=x6^post0, (tmp^0 <= 0 /\ -x6^post0+x6^0 == 0 /\ -ret_foo5^post0+ret_foo5^0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -ret_foo7^post0+ret_foo7^0 == 0 /\ x4^0-x4^post0 == 0 /\ -tmp^0 <= 0 /\ -il^post0+il^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ __const_10^0-__const_10^post0 == 0), cost: 1
   1: l0 -> l2 : tmp^0'=tmp^post1, il^0'=il^post1, x4^0'=x4^post1, ret_foo7^0'=ret_foo7^post1, __const_10^0'=__const_10^post1, tmp___0^0'=tmp___0^post1, ret_foo5^0'=ret_foo5^post1, x6^0'=x6^post1, (il^0-il^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ ret_foo7^0-ret_foo7^post1 == 0 /\ -ret_foo5^post1+ret_foo5^0 == 0 /\ -x6^post1+x6^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -x4^post1+x4^0 == 0 /\ 1-tmp^0 <= 0), cost: 1
   2: l0 -> l2 : tmp^0'=tmp^post2, il^0'=il^post2, x4^0'=x4^post2, ret_foo7^0'=ret_foo7^post2, __const_10^0'=__const_10^post2, tmp___0^0'=tmp___0^post2, ret_foo5^0'=ret_foo5^post2, x6^0'=x6^post2, (1+tmp^0 <= 0 /\ -x6^post2+x6^0 == 0 /\ x4^0-x4^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -il^post2+il^0 == 0 /\ -ret_foo5^post2+ret_foo5^0 == 0 /\ ret_foo7^0-ret_foo7^post2 == 0), cost: 1
  12: l1 -> l7 : tmp^0'=tmp^post12, il^0'=il^post12, x4^0'=x4^post12, ret_foo7^0'=ret_foo7^post12, __const_10^0'=__const_10^post12, tmp___0^0'=tmp___0^post12, ret_foo5^0'=ret_foo5^post12, x6^0'=x6^post12, (-__const_10^post12+__const_10^0 == 0 /\ -x4^post12+x4^0 == 0 /\ -x6^post12+x6^0 == 0 /\ il^post12 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ ret_foo7^0-ret_foo7^post12 == 0 /\ -ret_foo5^post12+ret_foo5^0 == 0), cost: 1
  13: l2 -> l1 : tmp^0'=tmp^post13, il^0'=il^post13, x4^0'=x4^post13, ret_foo7^0'=ret_foo7^post13, __const_10^0'=__const_10^post13, tmp___0^0'=tmp___0^post13, ret_foo5^0'=ret_foo5^post13, x6^0'=x6^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ __const_10^0-__const_10^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ -ret_foo5^post13+ret_foo5^0 == 0 /\ -il^0+__const_10^0 <= 0 /\ -ret_foo7^post13+ret_foo7^0 == 0 /\ x4^0-x4^post13 == 0 /\ -il^post13+il^0 == 0 /\ -x6^post13+x6^0 == 0), cost: 1
  14: l2 -> l3 : tmp^0'=tmp^post14, il^0'=il^post14, x4^0'=x4^post14, ret_foo7^0'=ret_foo7^post14, __const_10^0'=__const_10^post14, tmp___0^0'=tmp___0^post14, ret_foo5^0'=ret_foo5^post14, x6^0'=x6^post14, (1+il^0-__const_10^0 <= 0 /\ -x4^post14+x4^0 == 0 /\ -x6^post14+x6^0 == 0 /\ -ret_foo5^post14+ret_foo5^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ ret_foo7^0-ret_foo7^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -1-il^0+il^post14 == 0), cost: 1
   3: l3 -> l0 : tmp^0'=tmp^post3, il^0'=il^post3, x4^0'=x4^post3, ret_foo7^0'=ret_foo7^post3, __const_10^0'=__const_10^post3, tmp___0^0'=tmp___0^post3, ret_foo5^0'=ret_foo5^post3, x6^0'=x6^post3, (0 == 0 /\ il^0-il^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -ret_foo5^post3+tmp^post3 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -il^0+x4^post3 == 0 /\ -x6^post3+x6^0 == 0 /\ ret_foo7^0-ret_foo7^post3 == 0), cost: 1
   4: l4 -> l5 : tmp^0'=tmp^post4, il^0'=il^post4, x4^0'=x4^post4, ret_foo7^0'=ret_foo7^post4, __const_10^0'=__const_10^post4, tmp___0^0'=tmp___0^post4, ret_foo5^0'=ret_foo5^post4, x6^0'=x6^post4, (tmp^0-tmp^post4 == 0 /\ -ret_foo7^post4+ret_foo7^0 == 0 /\ x4^0-x4^post4 == 0 /\ __const_10^0-__const_10^post4 == 0 /\ -ret_foo5^post4+ret_foo5^0 == 0 /\ il^0-il^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -x6^post4+x6^0 == 0), cost: 1
   5: l6 -> l7 : tmp^0'=tmp^post5, il^0'=il^post5, x4^0'=x4^post5, ret_foo7^0'=ret_foo7^post5, __const_10^0'=__const_10^post5, tmp___0^0'=tmp___0^post5, ret_foo5^0'=ret_foo5^post5, x6^0'=x6^post5, (-ret_foo5^post5+ret_foo5^0 == 0 /\ -x6^post5+x6^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_10^post5+__const_10^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ ret_foo7^0-ret_foo7^post5 == 0 /\ -x4^post5+x4^0 == 0 /\ -1-il^0+il^post5 == 0), cost: 1
   9: l7 -> l9 : tmp^0'=tmp^post9, il^0'=il^post9, x4^0'=x4^post9, ret_foo7^0'=ret_foo7^post9, __const_10^0'=__const_10^post9, tmp___0^0'=tmp___0^post9, ret_foo5^0'=ret_foo5^post9, x6^0'=x6^post9, (-x4^post9+x4^0 == 0 /\ ret_foo7^0-ret_foo7^post9 == 0 /\ ret_foo5^0-ret_foo5^post9 == 0 /\ il^0-il^post9 == 0 /\ -x6^post9+x6^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -__const_10^post9+__const_10^0 == 0), cost: 1
   6: l8 -> l4 : tmp^0'=tmp^post6, il^0'=il^post6, x4^0'=x4^post6, ret_foo7^0'=ret_foo7^post6, __const_10^0'=__const_10^post6, tmp___0^0'=tmp___0^post6, ret_foo5^0'=ret_foo5^post6, x6^0'=x6^post6, (-ret_foo7^post6+ret_foo7^0 == 0 /\ x4^0-x4^post6 == 0 /\ -ret_foo5^post6+ret_foo5^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ -tmp___0^0 <= 0 /\ -il^post6+il^0 == 0 /\ tmp___0^0 <= 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -x6^post6+x6^0 == 0 /\ __const_10^0-__const_10^post6 == 0), cost: 1
   7: l8 -> l6 : tmp^0'=tmp^post7, il^0'=il^post7, x4^0'=x4^post7, ret_foo7^0'=ret_foo7^post7, __const_10^0'=__const_10^post7, tmp___0^0'=tmp___0^post7, ret_foo5^0'=ret_foo5^post7, x6^0'=x6^post7, (tmp^0-tmp^post7 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -x6^post7+x6^0 == 0 /\ ret_foo5^0-ret_foo5^post7 == 0 /\ 1-tmp___0^0 <= 0 /\ -x4^post7+x4^0 == 0 /\ ret_foo7^0-ret_foo7^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ il^0-il^post7 == 0), cost: 1
   8: l8 -> l6 : tmp^0'=tmp^post8, il^0'=il^post8, x4^0'=x4^post8, ret_foo7^0'=ret_foo7^post8, __const_10^0'=__const_10^post8, tmp___0^0'=tmp___0^post8, ret_foo5^0'=ret_foo5^post8, x6^0'=x6^post8, (-__const_10^post8+__const_10^0 == 0 /\ x4^0-x4^post8 == 0 /\ -x6^post8+x6^0 == 0 /\ 1+tmp___0^0 <= 0 /\ -ret_foo7^post8+ret_foo7^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ il^0-il^post8 == 0 /\ tmp^0-tmp^post8 == 0 /\ -ret_foo5^post8+ret_foo5^0 == 0), cost: 1
  10: l9 -> l4 : tmp^0'=tmp^post10, il^0'=il^post10, x4^0'=x4^post10, ret_foo7^0'=ret_foo7^post10, __const_10^0'=__const_10^post10, tmp___0^0'=tmp___0^post10, ret_foo5^0'=ret_foo5^post10, x6^0'=x6^post10, (x4^0-x4^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ -il^0+__const_10^0 <= 0 /\ -ret_foo5^post10+ret_foo5^0 == 0 /\ -x6^post10+x6^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -ret_foo7^post10+ret_foo7^0 == 0 /\ -__const_10^post10+__const_10^0 == 0 /\ il^0-il^post10 == 0), cost: 1
  11: l9 -> l8 : tmp^0'=tmp^post11, il^0'=il^post11, x4^0'=x4^post11, ret_foo7^0'=ret_foo7^post11, __const_10^0'=__const_10^post11, tmp___0^0'=tmp___0^post11, ret_foo5^0'=ret_foo5^post11, x6^0'=x6^post11, (0 == 0 /\ tmp^0-tmp^post11 == 0 /\ __const_10^0-__const_10^post11 == 0 /\ 1+il^0-__const_10^0 <= 0 /\ -x4^post11+x4^0 == 0 /\ il^0-il^post11 == 0 /\ tmp___0^post11-ret_foo7^post11 == 0 /\ -ret_foo5^post11+ret_foo5^0 == 0 /\ -il^0+x6^post11 == 0), cost: 1
  15: l10 -> l3 : tmp^0'=tmp^post15, il^0'=il^post15, x4^0'=x4^post15, ret_foo7^0'=ret_foo7^post15, __const_10^0'=__const_10^post15, tmp___0^0'=tmp___0^post15, ret_foo5^0'=ret_foo5^post15, x6^0'=x6^post15, (-ret_foo5^post15+ret_foo5^0 == 0 /\ -x6^post15+x6^0 == 0 /\ il^post15 == 0 /\ x4^0-x4^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ ret_foo7^0-ret_foo7^post15 == 0 /\ __const_10^0-__const_10^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1
  16: l11 -> l10 : tmp^0'=tmp^post16, il^0'=il^post16, x4^0'=x4^post16, ret_foo7^0'=ret_foo7^post16, __const_10^0'=__const_10^post16, tmp___0^0'=tmp___0^post16, ret_foo5^0'=ret_foo5^post16, x6^0'=x6^post16, (il^0-il^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -__const_10^post16+__const_10^0 == 0 /\ -ret_foo5^post16+ret_foo5^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ ret_foo7^0-ret_foo7^post16 == 0 /\ -x6^post16+x6^0 == 0 /\ -x4^post16+x4^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l11
   0: l0 -> l1 : tmp^0'=tmp^post0, il^0'=il^post0, x4^0'=x4^post0, ret_foo7^0'=ret_foo7^post0, __const_10^0'=__const_10^post0, tmp___0^0'=tmp___0^post0, ret_foo5^0'=ret_foo5^post0, x6^0'=x6^post0, (tmp^0 <= 0 /\ -x6^post0+x6^0 == 0 /\ -ret_foo5^post0+ret_foo5^0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -ret_foo7^post0+ret_foo7^0 == 0 /\ x4^0-x4^post0 == 0 /\ -tmp^0 <= 0 /\ -il^post0+il^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ __const_10^0-__const_10^post0 == 0), cost: 1
   1: l0 -> l2 : tmp^0'=tmp^post1, il^0'=il^post1, x4^0'=x4^post1, ret_foo7^0'=ret_foo7^post1, __const_10^0'=__const_10^post1, tmp___0^0'=tmp___0^post1, ret_foo5^0'=ret_foo5^post1, x6^0'=x6^post1, (il^0-il^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ ret_foo7^0-ret_foo7^post1 == 0 /\ -ret_foo5^post1+ret_foo5^0 == 0 /\ -x6^post1+x6^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -x4^post1+x4^0 == 0 /\ 1-tmp^0 <= 0), cost: 1
   2: l0 -> l2 : tmp^0'=tmp^post2, il^0'=il^post2, x4^0'=x4^post2, ret_foo7^0'=ret_foo7^post2, __const_10^0'=__const_10^post2, tmp___0^0'=tmp___0^post2, ret_foo5^0'=ret_foo5^post2, x6^0'=x6^post2, (1+tmp^0 <= 0 /\ -x6^post2+x6^0 == 0 /\ x4^0-x4^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -il^post2+il^0 == 0 /\ -ret_foo5^post2+ret_foo5^0 == 0 /\ ret_foo7^0-ret_foo7^post2 == 0), cost: 1
  12: l1 -> l7 : tmp^0'=tmp^post12, il^0'=il^post12, x4^0'=x4^post12, ret_foo7^0'=ret_foo7^post12, __const_10^0'=__const_10^post12, tmp___0^0'=tmp___0^post12, ret_foo5^0'=ret_foo5^post12, x6^0'=x6^post12, (-__const_10^post12+__const_10^0 == 0 /\ -x4^post12+x4^0 == 0 /\ -x6^post12+x6^0 == 0 /\ il^post12 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ ret_foo7^0-ret_foo7^post12 == 0 /\ -ret_foo5^post12+ret_foo5^0 == 0), cost: 1
  13: l2 -> l1 : tmp^0'=tmp^post13, il^0'=il^post13, x4^0'=x4^post13, ret_foo7^0'=ret_foo7^post13, __const_10^0'=__const_10^post13, tmp___0^0'=tmp___0^post13, ret_foo5^0'=ret_foo5^post13, x6^0'=x6^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ __const_10^0-__const_10^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ -ret_foo5^post13+ret_foo5^0 == 0 /\ -il^0+__const_10^0 <= 0 /\ -ret_foo7^post13+ret_foo7^0 == 0 /\ x4^0-x4^post13 == 0 /\ -il^post13+il^0 == 0 /\ -x6^post13+x6^0 == 0), cost: 1
  14: l2 -> l3 : tmp^0'=tmp^post14, il^0'=il^post14, x4^0'=x4^post14, ret_foo7^0'=ret_foo7^post14, __const_10^0'=__const_10^post14, tmp___0^0'=tmp___0^post14, ret_foo5^0'=ret_foo5^post14, x6^0'=x6^post14, (1+il^0-__const_10^0 <= 0 /\ -x4^post14+x4^0 == 0 /\ -x6^post14+x6^0 == 0 /\ -ret_foo5^post14+ret_foo5^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ ret_foo7^0-ret_foo7^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -1-il^0+il^post14 == 0), cost: 1
   3: l3 -> l0 : tmp^0'=tmp^post3, il^0'=il^post3, x4^0'=x4^post3, ret_foo7^0'=ret_foo7^post3, __const_10^0'=__const_10^post3, tmp___0^0'=tmp___0^post3, ret_foo5^0'=ret_foo5^post3, x6^0'=x6^post3, (0 == 0 /\ il^0-il^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -ret_foo5^post3+tmp^post3 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -il^0+x4^post3 == 0 /\ -x6^post3+x6^0 == 0 /\ ret_foo7^0-ret_foo7^post3 == 0), cost: 1
   5: l6 -> l7 : tmp^0'=tmp^post5, il^0'=il^post5, x4^0'=x4^post5, ret_foo7^0'=ret_foo7^post5, __const_10^0'=__const_10^post5, tmp___0^0'=tmp___0^post5, ret_foo5^0'=ret_foo5^post5, x6^0'=x6^post5, (-ret_foo5^post5+ret_foo5^0 == 0 /\ -x6^post5+x6^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_10^post5+__const_10^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ ret_foo7^0-ret_foo7^post5 == 0 /\ -x4^post5+x4^0 == 0 /\ -1-il^0+il^post5 == 0), cost: 1
   9: l7 -> l9 : tmp^0'=tmp^post9, il^0'=il^post9, x4^0'=x4^post9, ret_foo7^0'=ret_foo7^post9, __const_10^0'=__const_10^post9, tmp___0^0'=tmp___0^post9, ret_foo5^0'=ret_foo5^post9, x6^0'=x6^post9, (-x4^post9+x4^0 == 0 /\ ret_foo7^0-ret_foo7^post9 == 0 /\ ret_foo5^0-ret_foo5^post9 == 0 /\ il^0-il^post9 == 0 /\ -x6^post9+x6^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -__const_10^post9+__const_10^0 == 0), cost: 1
   7: l8 -> l6 : tmp^0'=tmp^post7, il^0'=il^post7, x4^0'=x4^post7, ret_foo7^0'=ret_foo7^post7, __const_10^0'=__const_10^post7, tmp___0^0'=tmp___0^post7, ret_foo5^0'=ret_foo5^post7, x6^0'=x6^post7, (tmp^0-tmp^post7 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -x6^post7+x6^0 == 0 /\ ret_foo5^0-ret_foo5^post7 == 0 /\ 1-tmp___0^0 <= 0 /\ -x4^post7+x4^0 == 0 /\ ret_foo7^0-ret_foo7^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ il^0-il^post7 == 0), cost: 1
   8: l8 -> l6 : tmp^0'=tmp^post8, il^0'=il^post8, x4^0'=x4^post8, ret_foo7^0'=ret_foo7^post8, __const_10^0'=__const_10^post8, tmp___0^0'=tmp___0^post8, ret_foo5^0'=ret_foo5^post8, x6^0'=x6^post8, (-__const_10^post8+__const_10^0 == 0 /\ x4^0-x4^post8 == 0 /\ -x6^post8+x6^0 == 0 /\ 1+tmp___0^0 <= 0 /\ -ret_foo7^post8+ret_foo7^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ il^0-il^post8 == 0 /\ tmp^0-tmp^post8 == 0 /\ -ret_foo5^post8+ret_foo5^0 == 0), cost: 1
  11: l9 -> l8 : tmp^0'=tmp^post11, il^0'=il^post11, x4^0'=x4^post11, ret_foo7^0'=ret_foo7^post11, __const_10^0'=__const_10^post11, tmp___0^0'=tmp___0^post11, ret_foo5^0'=ret_foo5^post11, x6^0'=x6^post11, (0 == 0 /\ tmp^0-tmp^post11 == 0 /\ __const_10^0-__const_10^post11 == 0 /\ 1+il^0-__const_10^0 <= 0 /\ -x4^post11+x4^0 == 0 /\ il^0-il^post11 == 0 /\ tmp___0^post11-ret_foo7^post11 == 0 /\ -ret_foo5^post11+ret_foo5^0 == 0 /\ -il^0+x6^post11 == 0), cost: 1
  15: l10 -> l3 : tmp^0'=tmp^post15, il^0'=il^post15, x4^0'=x4^post15, ret_foo7^0'=ret_foo7^post15, __const_10^0'=__const_10^post15, tmp___0^0'=tmp___0^post15, ret_foo5^0'=ret_foo5^post15, x6^0'=x6^post15, (-ret_foo5^post15+ret_foo5^0 == 0 /\ -x6^post15+x6^0 == 0 /\ il^post15 == 0 /\ x4^0-x4^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ ret_foo7^0-ret_foo7^post15 == 0 /\ __const_10^0-__const_10^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1
  16: l11 -> l10 : tmp^0'=tmp^post16, il^0'=il^post16, x4^0'=x4^post16, ret_foo7^0'=ret_foo7^post16, __const_10^0'=__const_10^post16, tmp___0^0'=tmp___0^post16, ret_foo5^0'=ret_foo5^post16, x6^0'=x6^post16, (il^0-il^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -__const_10^post16+__const_10^0 == 0 /\ -ret_foo5^post16+ret_foo5^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ ret_foo7^0-ret_foo7^post16 == 0 /\ -x6^post16+x6^0 == 0 /\ -x4^post16+x4^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : tmp^0'=tmp^post0, il^0'=il^post0, x4^0'=x4^post0, ret_foo7^0'=ret_foo7^post0, __const_10^0'=__const_10^post0, tmp___0^0'=tmp___0^post0, ret_foo5^0'=ret_foo5^post0, x6^0'=x6^post0, (tmp^0 <= 0 /\ -x6^post0+x6^0 == 0 /\ -ret_foo5^post0+ret_foo5^0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -ret_foo7^post0+ret_foo7^0 == 0 /\ x4^0-x4^post0 == 0 /\ -tmp^0 <= 0 /\ -il^post0+il^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ __const_10^0-__const_10^post0 == 0), cost: 1
New rule:
l0 -> l1 : tmp^0 == 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : tmp^0'=tmp^post1, il^0'=il^post1, x4^0'=x4^post1, ret_foo7^0'=ret_foo7^post1, __const_10^0'=__const_10^post1, tmp___0^0'=tmp___0^post1, ret_foo5^0'=ret_foo5^post1, x6^0'=x6^post1, (il^0-il^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ ret_foo7^0-ret_foo7^post1 == 0 /\ -ret_foo5^post1+ret_foo5^0 == 0 /\ -x6^post1+x6^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -x4^post1+x4^0 == 0 /\ 1-tmp^0 <= 0), cost: 1
New rule:
l0 -> l2 : -1+tmp^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : tmp^0'=tmp^post2, il^0'=il^post2, x4^0'=x4^post2, ret_foo7^0'=ret_foo7^post2, __const_10^0'=__const_10^post2, tmp___0^0'=tmp___0^post2, ret_foo5^0'=ret_foo5^post2, x6^0'=x6^post2, (1+tmp^0 <= 0 /\ -x6^post2+x6^0 == 0 /\ x4^0-x4^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ -il^post2+il^0 == 0 /\ -ret_foo5^post2+ret_foo5^0 == 0 /\ ret_foo7^0-ret_foo7^post2 == 0), cost: 1
New rule:
l0 -> l2 : 1+tmp^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l0 : tmp^0'=tmp^post3, il^0'=il^post3, x4^0'=x4^post3, ret_foo7^0'=ret_foo7^post3, __const_10^0'=__const_10^post3, tmp___0^0'=tmp___0^post3, ret_foo5^0'=ret_foo5^post3, x6^0'=x6^post3, (0 == 0 /\ il^0-il^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -ret_foo5^post3+tmp^post3 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -il^0+x4^post3 == 0 /\ -x6^post3+x6^0 == 0 /\ ret_foo7^0-ret_foo7^post3 == 0), cost: 1
New rule:
l3 -> l0 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l7 : tmp^0'=tmp^post5, il^0'=il^post5, x4^0'=x4^post5, ret_foo7^0'=ret_foo7^post5, __const_10^0'=__const_10^post5, tmp___0^0'=tmp___0^post5, ret_foo5^0'=ret_foo5^post5, x6^0'=x6^post5, (-ret_foo5^post5+ret_foo5^0 == 0 /\ -x6^post5+x6^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_10^post5+__const_10^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ ret_foo7^0-ret_foo7^post5 == 0 /\ -x4^post5+x4^0 == 0 /\ -1-il^0+il^post5 == 0), cost: 1
New rule:
l6 -> l7 : il^0'=1+il^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : tmp^0'=tmp^post7, il^0'=il^post7, x4^0'=x4^post7, ret_foo7^0'=ret_foo7^post7, __const_10^0'=__const_10^post7, tmp___0^0'=tmp___0^post7, ret_foo5^0'=ret_foo5^post7, x6^0'=x6^post7, (tmp^0-tmp^post7 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -x6^post7+x6^0 == 0 /\ ret_foo5^0-ret_foo5^post7 == 0 /\ 1-tmp___0^0 <= 0 /\ -x4^post7+x4^0 == 0 /\ ret_foo7^0-ret_foo7^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ il^0-il^post7 == 0), cost: 1
New rule:
l8 -> l6 : -1+tmp___0^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : tmp^0'=tmp^post8, il^0'=il^post8, x4^0'=x4^post8, ret_foo7^0'=ret_foo7^post8, __const_10^0'=__const_10^post8, tmp___0^0'=tmp___0^post8, ret_foo5^0'=ret_foo5^post8, x6^0'=x6^post8, (-__const_10^post8+__const_10^0 == 0 /\ x4^0-x4^post8 == 0 /\ -x6^post8+x6^0 == 0 /\ 1+tmp___0^0 <= 0 /\ -ret_foo7^post8+ret_foo7^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ il^0-il^post8 == 0 /\ tmp^0-tmp^post8 == 0 /\ -ret_foo5^post8+ret_foo5^0 == 0), cost: 1
New rule:
l8 -> l6 : 1+tmp___0^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l9 : tmp^0'=tmp^post9, il^0'=il^post9, x4^0'=x4^post9, ret_foo7^0'=ret_foo7^post9, __const_10^0'=__const_10^post9, tmp___0^0'=tmp___0^post9, ret_foo5^0'=ret_foo5^post9, x6^0'=x6^post9, (-x4^post9+x4^0 == 0 /\ ret_foo7^0-ret_foo7^post9 == 0 /\ ret_foo5^0-ret_foo5^post9 == 0 /\ il^0-il^post9 == 0 /\ -x6^post9+x6^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -__const_10^post9+__const_10^0 == 0), cost: 1
New rule:
l7 -> l9 : TRUE, cost: 1

Applied preprocessing
Original rule:
l9 -> l8 : tmp^0'=tmp^post11, il^0'=il^post11, x4^0'=x4^post11, ret_foo7^0'=ret_foo7^post11, __const_10^0'=__const_10^post11, tmp___0^0'=tmp___0^post11, ret_foo5^0'=ret_foo5^post11, x6^0'=x6^post11, (0 == 0 /\ tmp^0-tmp^post11 == 0 /\ __const_10^0-__const_10^post11 == 0 /\ 1+il^0-__const_10^0 <= 0 /\ -x4^post11+x4^0 == 0 /\ il^0-il^post11 == 0 /\ tmp___0^post11-ret_foo7^post11 == 0 /\ -ret_foo5^post11+ret_foo5^0 == 0 /\ -il^0+x6^post11 == 0), cost: 1
New rule:
l9 -> l8 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, 1+il^0-__const_10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l7 : tmp^0'=tmp^post12, il^0'=il^post12, x4^0'=x4^post12, ret_foo7^0'=ret_foo7^post12, __const_10^0'=__const_10^post12, tmp___0^0'=tmp___0^post12, ret_foo5^0'=ret_foo5^post12, x6^0'=x6^post12, (-__const_10^post12+__const_10^0 == 0 /\ -x4^post12+x4^0 == 0 /\ -x6^post12+x6^0 == 0 /\ il^post12 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ ret_foo7^0-ret_foo7^post12 == 0 /\ -ret_foo5^post12+ret_foo5^0 == 0), cost: 1
New rule:
l1 -> l7 : il^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l1 : tmp^0'=tmp^post13, il^0'=il^post13, x4^0'=x4^post13, ret_foo7^0'=ret_foo7^post13, __const_10^0'=__const_10^post13, tmp___0^0'=tmp___0^post13, ret_foo5^0'=ret_foo5^post13, x6^0'=x6^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ __const_10^0-__const_10^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ -ret_foo5^post13+ret_foo5^0 == 0 /\ -il^0+__const_10^0 <= 0 /\ -ret_foo7^post13+ret_foo7^0 == 0 /\ x4^0-x4^post13 == 0 /\ -il^post13+il^0 == 0 /\ -x6^post13+x6^0 == 0), cost: 1
New rule:
l2 -> l1 : -il^0+__const_10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : tmp^0'=tmp^post14, il^0'=il^post14, x4^0'=x4^post14, ret_foo7^0'=ret_foo7^post14, __const_10^0'=__const_10^post14, tmp___0^0'=tmp___0^post14, ret_foo5^0'=ret_foo5^post14, x6^0'=x6^post14, (1+il^0-__const_10^0 <= 0 /\ -x4^post14+x4^0 == 0 /\ -x6^post14+x6^0 == 0 /\ -ret_foo5^post14+ret_foo5^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ ret_foo7^0-ret_foo7^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -1-il^0+il^post14 == 0), cost: 1
New rule:
l2 -> l3 : il^0'=1+il^0, 1+il^0-__const_10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l3 : tmp^0'=tmp^post15, il^0'=il^post15, x4^0'=x4^post15, ret_foo7^0'=ret_foo7^post15, __const_10^0'=__const_10^post15, tmp___0^0'=tmp___0^post15, ret_foo5^0'=ret_foo5^post15, x6^0'=x6^post15, (-ret_foo5^post15+ret_foo5^0 == 0 /\ -x6^post15+x6^0 == 0 /\ il^post15 == 0 /\ x4^0-x4^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ ret_foo7^0-ret_foo7^post15 == 0 /\ __const_10^0-__const_10^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1
New rule:
l10 -> l3 : il^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : tmp^0'=tmp^post16, il^0'=il^post16, x4^0'=x4^post16, ret_foo7^0'=ret_foo7^post16, __const_10^0'=__const_10^post16, tmp___0^0'=tmp___0^post16, ret_foo5^0'=ret_foo5^post16, x6^0'=x6^post16, (il^0-il^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -__const_10^post16+__const_10^0 == 0 /\ -ret_foo5^post16+ret_foo5^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ ret_foo7^0-ret_foo7^post16 == 0 /\ -x6^post16+x6^0 == 0 /\ -x4^post16+x4^0 == 0), cost: 1
New rule:
l11 -> l10 : TRUE, cost: 1

Simplified rules
Start location: l11
  17: l0 -> l1 : tmp^0 == 0, cost: 1
  18: l0 -> l2 : -1+tmp^0 >= 0, cost: 1
  19: l0 -> l2 : 1+tmp^0 <= 0, cost: 1
  26: l1 -> l7 : il^0'=0, TRUE, cost: 1
  27: l2 -> l1 : -il^0+__const_10^0 <= 0, cost: 1
  28: l2 -> l3 : il^0'=1+il^0, 1+il^0-__const_10^0 <= 0, cost: 1
  20: l3 -> l0 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 0 == 0, cost: 1
  21: l6 -> l7 : il^0'=1+il^0, TRUE, cost: 1
  24: l7 -> l9 : TRUE, cost: 1
  22: l8 -> l6 : -1+tmp___0^0 >= 0, cost: 1
  23: l8 -> l6 : 1+tmp___0^0 <= 0, cost: 1
  25: l9 -> l8 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, 1+il^0-__const_10^0 <= 0, cost: 1
  29: l10 -> l3 : il^0'=0, TRUE, cost: 1
  30: l11 -> l10 : TRUE, cost: 1


Eliminating location l10 by chaining:

Applied chaining
First rule:
l11 -> l10 : TRUE, cost: 1
Second rule:
l10 -> l3 : il^0'=0, TRUE, cost: 1
New rule:
l11 -> l3 : il^0'=0, TRUE, cost: 2

Applied deletion
Removed the following rules: 29 30

Eliminating location l9 by chaining:

Applied chaining
First rule:
l7 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l8 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, 1+il^0-__const_10^0 <= 0, cost: 1
New rule:
l7 -> l8 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, 1+il^0-__const_10^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 24 25

Eliminated locations on linear paths
Start location: l11
  17: l0 -> l1 : tmp^0 == 0, cost: 1
  18: l0 -> l2 : -1+tmp^0 >= 0, cost: 1
  19: l0 -> l2 : 1+tmp^0 <= 0, cost: 1
  26: l1 -> l7 : il^0'=0, TRUE, cost: 1
  27: l2 -> l1 : -il^0+__const_10^0 <= 0, cost: 1
  28: l2 -> l3 : il^0'=1+il^0, 1+il^0-__const_10^0 <= 0, cost: 1
  20: l3 -> l0 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 0 == 0, cost: 1
  21: l6 -> l7 : il^0'=1+il^0, TRUE, cost: 1
  32: l7 -> l8 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, 1+il^0-__const_10^0 <= 0, cost: 2
  22: l8 -> l6 : -1+tmp___0^0 >= 0, cost: 1
  23: l8 -> l6 : 1+tmp___0^0 <= 0, cost: 1
  31: l11 -> l3 : il^0'=0, TRUE, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l3 -> l0 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 0 == 0, cost: 1
Second rule:
l0 -> l1 : tmp^0 == 0, cost: 1
New rule:
l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (0 == 0 /\ tmp^post3 == 0), cost: 2

Applied simplification
Original rule:
l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (0 == 0 /\ tmp^post3 == 0), cost: 2
New rule:
l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, tmp^post3 == 0, cost: 2

Applied chaining
First rule:
l3 -> l0 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 0 == 0, cost: 1
Second rule:
l0 -> l2 : -1+tmp^0 >= 0, cost: 1
New rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (0 == 0 /\ -1+tmp^post3 >= 0), cost: 2

Applied simplification
Original rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (0 == 0 /\ -1+tmp^post3 >= 0), cost: 2
New rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, -1+tmp^post3 >= 0, cost: 2

Applied chaining
First rule:
l3 -> l0 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 0 == 0, cost: 1
Second rule:
l0 -> l2 : 1+tmp^0 <= 0, cost: 1
New rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (0 == 0 /\ 1+tmp^post3 <= 0), cost: 2

Applied simplification
Original rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (0 == 0 /\ 1+tmp^post3 <= 0), cost: 2
New rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 1+tmp^post3 <= 0, cost: 2

Applied deletion
Removed the following rules: 17 18 19 20

Eliminating location l8 by chaining:

Applied chaining
First rule:
l7 -> l8 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, 1+il^0-__const_10^0 <= 0, cost: 2
Second rule:
l8 -> l6 : -1+tmp___0^0 >= 0, cost: 1
New rule:
l7 -> l6 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ -1+ret_foo7^post11 >= 0), cost: 3

Applied chaining
First rule:
l7 -> l8 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, 1+il^0-__const_10^0 <= 0, cost: 2
Second rule:
l8 -> l6 : 1+tmp___0^0 <= 0, cost: 1
New rule:
l7 -> l6 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ 1+ret_foo7^post11 <= 0), cost: 3

Applied deletion
Removed the following rules: 22 23 32

Eliminated locations on tree-shaped paths
Start location: l11
  26: l1 -> l7 : il^0'=0, TRUE, cost: 1
  27: l2 -> l1 : -il^0+__const_10^0 <= 0, cost: 1
  28: l2 -> l3 : il^0'=1+il^0, 1+il^0-__const_10^0 <= 0, cost: 1
  33: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, tmp^post3 == 0, cost: 2
  34: l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, -1+tmp^post3 >= 0, cost: 2
  35: l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 1+tmp^post3 <= 0, cost: 2
  21: l6 -> l7 : il^0'=1+il^0, TRUE, cost: 1
  36: l7 -> l6 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ -1+ret_foo7^post11 >= 0), cost: 3
  37: l7 -> l6 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ 1+ret_foo7^post11 <= 0), cost: 3
  31: l11 -> l3 : il^0'=0, TRUE, cost: 2


Eliminating location l2 by chaining:

Applied chaining
First rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, -1+tmp^post3 >= 0, cost: 2
Second rule:
l2 -> l1 : -il^0+__const_10^0 <= 0, cost: 1
New rule:
l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -il^0+__const_10^0 <= 0), cost: 3

Applied chaining
First rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, -1+tmp^post3 >= 0, cost: 2
Second rule:
l2 -> l3 : il^0'=1+il^0, 1+il^0-__const_10^0 <= 0, cost: 1
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=1+il^0, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ 1+il^0-__const_10^0 <= 0), cost: 3

Applied chaining
First rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 1+tmp^post3 <= 0, cost: 2
Second rule:
l2 -> l1 : -il^0+__const_10^0 <= 0, cost: 1
New rule:
l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-il^0+__const_10^0 <= 0 /\ 1+tmp^post3 <= 0), cost: 3

Applied chaining
First rule:
l3 -> l2 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, 1+tmp^post3 <= 0, cost: 2
Second rule:
l2 -> l3 : il^0'=1+il^0, 1+il^0-__const_10^0 <= 0, cost: 1
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=1+il^0, x4^0'=il^0, ret_foo5^0'=tmp^post3, (1+il^0-__const_10^0 <= 0 /\ 1+tmp^post3 <= 0), cost: 3

Applied deletion
Removed the following rules: 27 28 34 35

Eliminating location l6 by chaining:

Applied chaining
First rule:
l7 -> l6 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ -1+ret_foo7^post11 >= 0), cost: 3
Second rule:
l6 -> l7 : il^0'=1+il^0, TRUE, cost: 1
New rule:
l7 -> l7 : il^0'=1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ -1+ret_foo7^post11 >= 0), cost: 4

Applied chaining
First rule:
l7 -> l6 : ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ 1+ret_foo7^post11 <= 0), cost: 3
Second rule:
l6 -> l7 : il^0'=1+il^0, TRUE, cost: 1
New rule:
l7 -> l7 : il^0'=1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ 1+ret_foo7^post11 <= 0), cost: 4

Applied deletion
Removed the following rules: 21 36 37

Eliminated locations on tree-shaped paths
Start location: l11
  26: l1 -> l7 : il^0'=0, TRUE, cost: 1
  33: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, tmp^post3 == 0, cost: 2
  38: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -il^0+__const_10^0 <= 0), cost: 3
  39: l3 -> l3 : tmp^0'=tmp^post3, il^0'=1+il^0, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ 1+il^0-__const_10^0 <= 0), cost: 3
  40: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-il^0+__const_10^0 <= 0 /\ 1+tmp^post3 <= 0), cost: 3
  41: l3 -> l3 : tmp^0'=tmp^post3, il^0'=1+il^0, x4^0'=il^0, ret_foo5^0'=tmp^post3, (1+il^0-__const_10^0 <= 0 /\ 1+tmp^post3 <= 0), cost: 3
  42: l7 -> l7 : il^0'=1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ -1+ret_foo7^post11 >= 0), cost: 4
  43: l7 -> l7 : il^0'=1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ 1+ret_foo7^post11 <= 0), cost: 4
  31: l11 -> l3 : il^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=1+il^0, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ 1+il^0-__const_10^0 <= 0), cost: 3
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=il^0+n, x4^0'=-1+il^0+n, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -il^0-n+__const_10^0 >= 0 /\ -1+n >= 0), cost: 3*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_aapAnm.txt

Applied instantiation
Original rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=il^0+n, x4^0'=-1+il^0+n, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -il^0-n+__const_10^0 >= 0 /\ -1+n >= 0), cost: 3*n
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (0 >= 0 /\ -1+tmp^post3 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -3*il^0+3*__const_10^0

Applied acceleration
Original rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=1+il^0, x4^0'=il^0, ret_foo5^0'=tmp^post3, (1+il^0-__const_10^0 <= 0 /\ 1+tmp^post3 <= 0), cost: 3
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=il^0+n0, x4^0'=-1+il^0+n0, ret_foo5^0'=tmp^post3, (-1+n0 >= 0 /\ -il^0+__const_10^0-n0 >= 0 /\ -1-tmp^post3 >= 0), cost: 3*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bPchbk.txt

Applied instantiation
Original rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=il^0+n0, x4^0'=-1+il^0+n0, ret_foo5^0'=tmp^post3, (-1+n0 >= 0 /\ -il^0+__const_10^0-n0 >= 0 /\ -1-tmp^post3 >= 0), cost: 3*n0
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (0 >= 0 /\ -1-il^0+__const_10^0 >= 0 /\ -1-tmp^post3 >= 0), cost: -3*il^0+3*__const_10^0

Applied simplification
Original rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (0 >= 0 /\ -1+tmp^post3 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -3*il^0+3*__const_10^0
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -3*il^0+3*__const_10^0

Applied simplification
Original rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (0 >= 0 /\ -1-il^0+__const_10^0 >= 0 /\ -1-tmp^post3 >= 0), cost: -3*il^0+3*__const_10^0
New rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1-il^0+__const_10^0 >= 0 /\ 1+tmp^post3 <= 0), cost: -3*il^0+3*__const_10^0

Applied deletion
Removed the following rules: 39 41

Applied acceleration
Original rule:
l7 -> l7 : il^0'=1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ -1+ret_foo7^post11 >= 0), cost: 4
New rule:
l7 -> l7 : il^0'=n1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+n1+il^0, (-1+ret_foo7^post11 >= 0 /\ -1+n1 >= 0 /\ -n1-il^0+__const_10^0 >= 0), cost: 4*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kjidEH.txt

Applied instantiation
Original rule:
l7 -> l7 : il^0'=n1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+n1+il^0, (-1+ret_foo7^post11 >= 0 /\ -1+n1 >= 0 /\ -n1-il^0+__const_10^0 >= 0), cost: 4*n1
New rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (0 >= 0 /\ -1+ret_foo7^post11 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0

Applied acceleration
Original rule:
l7 -> l7 : il^0'=1+il^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=il^0, (1+il^0-__const_10^0 <= 0 /\ 1+ret_foo7^post11 <= 0), cost: 4
New rule:
l7 -> l7 : il^0'=il^0+n2, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+il^0+n2, (-il^0+__const_10^0-n2 >= 0 /\ -1-ret_foo7^post11 >= 0 /\ -1+n2 >= 0), cost: 4*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_olplpm.txt

Applied instantiation
Original rule:
l7 -> l7 : il^0'=il^0+n2, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+il^0+n2, (-il^0+__const_10^0-n2 >= 0 /\ -1-ret_foo7^post11 >= 0 /\ -1+n2 >= 0), cost: 4*n2
New rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (0 >= 0 /\ -1-ret_foo7^post11 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0

Applied simplification
Original rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (0 >= 0 /\ -1+ret_foo7^post11 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0
New rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (-1+ret_foo7^post11 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0

Applied simplification
Original rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (0 >= 0 /\ -1-ret_foo7^post11 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0
New rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (1+ret_foo7^post11 <= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0

Applied deletion
Removed the following rules: 42 43

Accelerated simple loops
Start location: l11
  26: l1 -> l7 : il^0'=0, TRUE, cost: 1
  33: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, tmp^post3 == 0, cost: 2
  38: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -il^0+__const_10^0 <= 0), cost: 3
  40: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-il^0+__const_10^0 <= 0 /\ 1+tmp^post3 <= 0), cost: 3
  46: l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -3*il^0+3*__const_10^0
  47: l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1-il^0+__const_10^0 >= 0 /\ 1+tmp^post3 <= 0), cost: -3*il^0+3*__const_10^0
  50: l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (-1+ret_foo7^post11 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0
  51: l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (1+ret_foo7^post11 <= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0
  31: l11 -> l3 : il^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l11 -> l3 : il^0'=0, TRUE, cost: 2
Second rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -3*il^0+3*__const_10^0
New rule:
l11 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -1+__const_10^0 >= 0), cost: 2+3*__const_10^0

Applied chaining
First rule:
l11 -> l3 : il^0'=0, TRUE, cost: 2
Second rule:
l3 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1-il^0+__const_10^0 >= 0 /\ 1+tmp^post3 <= 0), cost: -3*il^0+3*__const_10^0
New rule:
l11 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (1+tmp^post3 <= 0 /\ -1+__const_10^0 >= 0), cost: 2+3*__const_10^0

Applied deletion
Removed the following rules: 46 47

Applied chaining
First rule:
l1 -> l7 : il^0'=0, TRUE, cost: 1
Second rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (-1+ret_foo7^post11 >= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0
New rule:
l1 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (-1+ret_foo7^post11 >= 0 /\ -1+__const_10^0 >= 0), cost: 1+4*__const_10^0

Applied chaining
First rule:
l1 -> l7 : il^0'=0, TRUE, cost: 1
Second rule:
l7 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (1+ret_foo7^post11 <= 0 /\ -1-il^0+__const_10^0 >= 0), cost: -4*il^0+4*__const_10^0
New rule:
l1 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (1+ret_foo7^post11 <= 0 /\ -1+__const_10^0 >= 0), cost: 1+4*__const_10^0

Applied deletion
Removed the following rules: 50 51

Chained accelerated rules with incoming rules
Start location: l11
  26: l1 -> l7 : il^0'=0, TRUE, cost: 1
  54: l1 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (-1+ret_foo7^post11 >= 0 /\ -1+__const_10^0 >= 0), cost: 1+4*__const_10^0
  55: l1 -> l7 : il^0'=__const_10^0, ret_foo7^0'=ret_foo7^post11, tmp___0^0'=ret_foo7^post11, x6^0'=-1+__const_10^0, (1+ret_foo7^post11 <= 0 /\ -1+__const_10^0 >= 0), cost: 1+4*__const_10^0
  33: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, tmp^post3 == 0, cost: 2
  38: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -il^0+__const_10^0 <= 0), cost: 3
  40: l3 -> l1 : tmp^0'=tmp^post3, x4^0'=il^0, ret_foo5^0'=tmp^post3, (-il^0+__const_10^0 <= 0 /\ 1+tmp^post3 <= 0), cost: 3
  31: l11 -> l3 : il^0'=0, TRUE, cost: 2
  52: l11 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (-1+tmp^post3 >= 0 /\ -1+__const_10^0 >= 0), cost: 2+3*__const_10^0
  53: l11 -> l3 : tmp^0'=tmp^post3, il^0'=__const_10^0, x4^0'=-1+__const_10^0, ret_foo5^0'=tmp^post3, (1+tmp^post3 <= 0 /\ -1+__const_10^0 >= 0), cost: 2+3*__const_10^0


Removed unreachable locations and irrelevant leafs
Start location: l11
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0