NO

Initial ITS
Start location: l15
   0: l0 -> l1 : tmp^0'=tmp^post0, loop_max^0'=loop_max^post0, nPackets^0'=nPackets^post0, loop_count^0'=loop_count^post0, tmp___0^0'=tmp___0^post0, nPacketsOld^0'=nPacketsOld^post0, (loop_max^0-loop_max^post0 == 0 /\ -nPackets^post0+nPackets^0 == 0 /\ -loop_count^post0+loop_count^0 == 0 /\ -nPacketsOld^post0+nPacketsOld^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ tmp^0-tmp^post0 == 0), cost: 1
  23: l1 -> l14 : tmp^0'=tmp^post23, loop_max^0'=loop_max^post23, nPackets^0'=nPackets^post23, loop_count^0'=loop_count^post23, tmp___0^0'=tmp___0^post23, nPacketsOld^0'=nPacketsOld^post23, (-tmp___0^post23+tmp___0^0 == 0 /\ loop_count^0-loop_count^post23 == 0 /\ nPackets^0-nPackets^post23 == 0 /\ -nPacketsOld^post23+nPacketsOld^0 == 0 /\ -loop_max^post23+loop_max^0 == 0 /\ tmp^0-tmp^post23 == 0), cost: 1
   1: l2 -> l0 : tmp^0'=tmp^post1, loop_max^0'=loop_max^post1, nPackets^0'=nPackets^post1, loop_count^0'=loop_count^post1, tmp___0^0'=tmp___0^post1, nPacketsOld^0'=nPacketsOld^post1, (-tmp___0^post1+tmp___0^0 == 0 /\ -loop_count^post1+loop_count^0 == 0 /\ -nPacketsOld^post1+nPacketsOld^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ nPackets^0-nPackets^post1 == 0 /\ loop_max^0-loop_max^post1 == 0), cost: 1
   2: l2 -> l0 : tmp^0'=tmp^post2, loop_max^0'=loop_max^post2, nPackets^0'=nPackets^post2, loop_count^0'=loop_count^post2, tmp___0^0'=tmp___0^post2, nPacketsOld^0'=nPacketsOld^post2, (-nPacketsOld^post2+nPacketsOld^0 == 0 /\ loop_count^0-loop_count^post2 == 0 /\ loop_max^0-loop_max^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ nPackets^0-nPackets^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0), cost: 1
   3: l2 -> l3 : tmp^0'=tmp^post3, loop_max^0'=loop_max^post3, nPackets^0'=nPackets^post3, loop_count^0'=loop_count^post3, tmp___0^0'=tmp___0^post3, nPacketsOld^0'=nPacketsOld^post3, (loop_count^0-loop_count^post3 == 0 /\ -nPacketsOld^post3+nPacketsOld^0 == 0 /\ nPackets^0-nPackets^post3 == 0 /\ loop_max^0-loop_max^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0), cost: 1
  10: l3 -> l8 : tmp^0'=tmp^post10, loop_max^0'=loop_max^post10, nPackets^0'=nPackets^post10, loop_count^0'=loop_count^post10, tmp___0^0'=tmp___0^post10, nPacketsOld^0'=nPacketsOld^post10, (tmp^0-tmp^post10 == 0 /\ -loop_max^post10+loop_max^0 == 0 /\ nPackets^0-nPackets^post10 == 0 /\ loop_count^0-loop_count^post10 == 0 /\ -nPacketsOld^post10+nPacketsOld^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ 1-nPackets^0+nPacketsOld^0 <= 0), cost: 1
  11: l3 -> l8 : tmp^0'=tmp^post11, loop_max^0'=loop_max^post11, nPackets^0'=nPackets^post11, loop_count^0'=loop_count^post11, tmp___0^0'=tmp___0^post11, nPacketsOld^0'=nPacketsOld^post11, (loop_count^0-loop_count^post11 == 0 /\ -nPacketsOld^post11+nPacketsOld^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ 1+nPackets^0-nPacketsOld^0 <= 0 /\ nPackets^0-nPackets^post11 == 0 /\ loop_max^0-loop_max^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0), cost: 1
  12: l3 -> l6 : tmp^0'=tmp^post12, loop_max^0'=loop_max^post12, nPackets^0'=nPackets^post12, loop_count^0'=loop_count^post12, tmp___0^0'=tmp___0^post12, nPacketsOld^0'=nPacketsOld^post12, (tmp^0-tmp^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ nPackets^0-nPacketsOld^0 <= 0 /\ loop_max^0-loop_max^post12 == 0 /\ -nPacketsOld^post12+nPacketsOld^0 == 0 /\ -nPackets^post12+nPackets^0 == 0 /\ -nPackets^0+nPacketsOld^0 <= 0 /\ -loop_count^post12+loop_count^0 == 0), cost: 1
   4: l4 -> l2 : tmp^0'=tmp^post4, loop_max^0'=loop_max^post4, nPackets^0'=nPackets^post4, loop_count^0'=loop_count^post4, tmp___0^0'=tmp___0^post4, nPacketsOld^0'=nPacketsOld^post4, (nPackets^0-nPackets^post4 == 0 /\ loop_count^0-loop_count^post4 == 0 /\ -loop_max^post4+loop_max^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -nPacketsOld^post4+nPacketsOld^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0), cost: 1
   5: l4 -> l2 : tmp^0'=tmp^post5, loop_max^0'=loop_max^post5, nPackets^0'=nPackets^post5, loop_count^0'=loop_count^post5, tmp___0^0'=tmp___0^post5, nPacketsOld^0'=nPacketsOld^post5, (-nPacketsOld^post5+nPacketsOld^0 == 0 /\ -nPackets^post5+nPackets^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ loop_count^0-loop_count^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ loop_max^0-loop_max^post5 == 0), cost: 1
   6: l4 -> l3 : tmp^0'=tmp^post6, loop_max^0'=loop_max^post6, nPackets^0'=nPackets^post6, loop_count^0'=loop_count^post6, tmp___0^0'=tmp___0^post6, nPacketsOld^0'=nPacketsOld^post6, (tmp^0-tmp^post6 == 0 /\ -nPacketsOld^post6+nPacketsOld^0 == 0 /\ -nPackets^post6+nPackets^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -loop_count^post6+loop_count^0 == 0 /\ loop_max^0-loop_max^post6 == 0), cost: 1
   7: l5 -> l4 : tmp^0'=tmp^post7, loop_max^0'=loop_max^post7, nPackets^0'=nPackets^post7, loop_count^0'=loop_count^post7, tmp___0^0'=tmp___0^post7, nPacketsOld^0'=nPacketsOld^post7, (nPacketsOld^0-nPacketsOld^post7 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ nPackets^0-nPackets^post7 == 0 /\ loop_max^0-loop_max^post7 == 0 /\ -loop_count^post7+loop_count^0 == 0), cost: 1
   8: l5 -> l6 : tmp^0'=tmp^post8, loop_max^0'=loop_max^post8, nPackets^0'=nPackets^post8, loop_count^0'=loop_count^post8, tmp___0^0'=tmp___0^post8, nPacketsOld^0'=nPacketsOld^post8, (loop_max^0-loop_count^0 <= 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -nPacketsOld^post8+nPacketsOld^0 == 0 /\ -loop_count^post8+loop_count^0 == 0 /\ nPackets^0-nPackets^post8 == 0 /\ loop_max^0-loop_max^post8 == 0 /\ tmp^0-tmp^post8 == 0), cost: 1
   9: l6 -> l7 : tmp^0'=tmp^post9, loop_max^0'=loop_max^post9, nPackets^0'=nPackets^post9, loop_count^0'=loop_count^post9, tmp___0^0'=tmp___0^post9, nPacketsOld^0'=nPacketsOld^post9, (-tmp___0^post9+tmp___0^0 == 0 /\ -loop_count^post9+loop_count^0 == 0 /\ loop_max^0-loop_max^post9 == 0 /\ -nPacketsOld^post9+nPacketsOld^0 == 0 /\ nPackets^0-nPackets^post9 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1
  24: l8 -> l5 : tmp^0'=tmp^post24, loop_max^0'=loop_max^post24, nPackets^0'=nPackets^post24, loop_count^0'=loop_count^post24, tmp___0^0'=tmp___0^post24, nPacketsOld^0'=nPacketsOld^post24, (-nPackets^post24+nPackets^0 == 0 /\ nPacketsOld^post24-nPackets^0 == 0 /\ -loop_max^post24+loop_max^0 == 0 /\ tmp^0-tmp^post24 == 0 /\ loop_count^0-loop_count^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0), cost: 1
  13: l9 -> l3 : tmp^0'=tmp^post13, loop_max^0'=loop_max^post13, nPackets^0'=nPackets^post13, loop_count^0'=loop_count^post13, tmp___0^0'=tmp___0^post13, nPacketsOld^0'=nPacketsOld^post13, (tmp^0-tmp^post13 == 0 /\ loop_max^0-loop_max^post13 == 0 /\ -nPackets^post13+nPackets^0 == 0 /\ -nPacketsOld^post13+nPacketsOld^0 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -1+loop_count^post13-loop_count^0 == 0), cost: 1
  14: l10 -> l3 : tmp^0'=tmp^post14, loop_max^0'=loop_max^post14, nPackets^0'=nPackets^post14, loop_count^0'=loop_count^post14, tmp___0^0'=tmp___0^post14, nPacketsOld^0'=nPacketsOld^post14, (loop_max^0-loop_max^post14 == 0 /\ tmp^0-tmp^post14 == 0 /\ -nPackets^post14+nPackets^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ nPacketsOld^0-nPacketsOld^post14 == 0 /\ -tmp___0^0 <= 0 /\ tmp___0^0 <= 0 /\ -loop_count^post14+loop_count^0 == 0), cost: 1
  15: l10 -> l9 : tmp^0'=tmp^post15, loop_max^0'=loop_max^post15, nPackets^0'=nPackets^post15, loop_count^0'=loop_count^post15, tmp___0^0'=tmp___0^post15, nPacketsOld^0'=nPacketsOld^post15, (nPacketsOld^0-nPacketsOld^post15 == 0 /\ -loop_count^post15+loop_count^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ 1-tmp___0^0 <= 0 /\ loop_max^0-loop_max^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ nPackets^0-nPackets^post15 == 0), cost: 1
  16: l10 -> l9 : tmp^0'=tmp^post16, loop_max^0'=loop_max^post16, nPackets^0'=nPackets^post16, loop_count^0'=loop_count^post16, tmp___0^0'=tmp___0^post16, nPacketsOld^0'=nPacketsOld^post16, (tmp^0-tmp^post16 == 0 /\ 1+tmp___0^0 <= 0 /\ nPackets^0-nPackets^post16 == 0 /\ -loop_max^post16+loop_max^0 == 0 /\ -loop_count^post16+loop_count^0 == 0 /\ -nPacketsOld^post16+nPacketsOld^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1
  17: l11 -> l10 : tmp^0'=tmp^post17, loop_max^0'=loop_max^post17, nPackets^0'=nPackets^post17, loop_count^0'=loop_count^post17, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPacketsOld^post17, (0 == 0 /\ -nPacketsOld^post17+nPacketsOld^0 == 0 /\ tmp^0-tmp^post17 == 0 /\ -nPackets^post17+nPackets^0 == 0 /\ loop_count^0-loop_count^post17 == 0 /\ loop_max^0-loop_max^post17 == 0), cost: 1
  18: l12 -> l11 : tmp^0'=tmp^post18, loop_max^0'=loop_max^post18, nPackets^0'=nPackets^post18, loop_count^0'=loop_count^post18, tmp___0^0'=tmp___0^post18, nPacketsOld^0'=nPacketsOld^post18, (tmp^0-tmp^post18 == 0 /\ -1+nPackets^post18-nPackets^0 == 0 /\ loop_max^0-loop_max^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ -loop_count^post18+loop_count^0 == 0 /\ -nPacketsOld^post18+nPacketsOld^0 == 0), cost: 1
  19: l13 -> l11 : tmp^0'=tmp^post19, loop_max^0'=loop_max^post19, nPackets^0'=nPackets^post19, loop_count^0'=loop_count^post19, tmp___0^0'=tmp___0^post19, nPacketsOld^0'=nPacketsOld^post19, (tmp^0 <= 0 /\ tmp^0-tmp^post19 == 0 /\ -loop_count^post19+loop_count^0 == 0 /\ -nPackets^post19+nPackets^0 == 0 /\ loop_max^0-loop_max^post19 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -tmp^0 <= 0 /\ -nPacketsOld^post19+nPacketsOld^0 == 0), cost: 1
  20: l13 -> l12 : tmp^0'=tmp^post20, loop_max^0'=loop_max^post20, nPackets^0'=nPackets^post20, loop_count^0'=loop_count^post20, tmp___0^0'=tmp___0^post20, nPacketsOld^0'=nPacketsOld^post20, (loop_max^0-loop_max^post20 == 0 /\ -nPackets^post20+nPackets^0 == 0 /\ tmp^0-tmp^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ nPacketsOld^0-nPacketsOld^post20 == 0 /\ -loop_count^post20+loop_count^0 == 0 /\ 1-tmp^0 <= 0), cost: 1
  21: l13 -> l12 : tmp^0'=tmp^post21, loop_max^0'=loop_max^post21, nPackets^0'=nPackets^post21, loop_count^0'=loop_count^post21, tmp___0^0'=tmp___0^post21, nPacketsOld^0'=nPacketsOld^post21, (nPacketsOld^0-nPacketsOld^post21 == 0 /\ 1+tmp^0 <= 0 /\ -loop_count^post21+loop_count^0 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ loop_max^0-loop_max^post21 == 0 /\ tmp^0-tmp^post21 == 0 /\ nPackets^0-nPackets^post21 == 0), cost: 1
  22: l14 -> l13 : tmp^0'=tmp^post22, loop_max^0'=loop_max^post22, nPackets^0'=nPackets^post22, loop_count^0'=loop_count^post22, tmp___0^0'=tmp___0^post22, nPacketsOld^0'=nPacketsOld^post22, (0 == 0 /\ -nPacketsOld^post22+nPacketsOld^0 == 0 /\ loop_max^0-loop_max^post22 == 0 /\ loop_count^0-loop_count^post22 == 0 /\ nPackets^0-nPackets^post22 == 0 /\ -tmp___0^post22+tmp___0^0 == 0), cost: 1
  25: l15 -> l8 : tmp^0'=tmp^post25, loop_max^0'=loop_max^post25, nPackets^0'=nPackets^post25, loop_count^0'=loop_count^post25, tmp___0^0'=tmp___0^post25, nPacketsOld^0'=nPacketsOld^post25, (-nPackets^post25+nPackets^0 == 0 /\ -nPacketsOld^post25+nPacketsOld^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ loop_max^0-loop_max^post25 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ loop_count^0-loop_count^post25 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l15
   0: l0 -> l1 : tmp^0'=tmp^post0, loop_max^0'=loop_max^post0, nPackets^0'=nPackets^post0, loop_count^0'=loop_count^post0, tmp___0^0'=tmp___0^post0, nPacketsOld^0'=nPacketsOld^post0, (loop_max^0-loop_max^post0 == 0 /\ -nPackets^post0+nPackets^0 == 0 /\ -loop_count^post0+loop_count^0 == 0 /\ -nPacketsOld^post0+nPacketsOld^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ tmp^0-tmp^post0 == 0), cost: 1
  23: l1 -> l14 : tmp^0'=tmp^post23, loop_max^0'=loop_max^post23, nPackets^0'=nPackets^post23, loop_count^0'=loop_count^post23, tmp___0^0'=tmp___0^post23, nPacketsOld^0'=nPacketsOld^post23, (-tmp___0^post23+tmp___0^0 == 0 /\ loop_count^0-loop_count^post23 == 0 /\ nPackets^0-nPackets^post23 == 0 /\ -nPacketsOld^post23+nPacketsOld^0 == 0 /\ -loop_max^post23+loop_max^0 == 0 /\ tmp^0-tmp^post23 == 0), cost: 1
   1: l2 -> l0 : tmp^0'=tmp^post1, loop_max^0'=loop_max^post1, nPackets^0'=nPackets^post1, loop_count^0'=loop_count^post1, tmp___0^0'=tmp___0^post1, nPacketsOld^0'=nPacketsOld^post1, (-tmp___0^post1+tmp___0^0 == 0 /\ -loop_count^post1+loop_count^0 == 0 /\ -nPacketsOld^post1+nPacketsOld^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ nPackets^0-nPackets^post1 == 0 /\ loop_max^0-loop_max^post1 == 0), cost: 1
   2: l2 -> l0 : tmp^0'=tmp^post2, loop_max^0'=loop_max^post2, nPackets^0'=nPackets^post2, loop_count^0'=loop_count^post2, tmp___0^0'=tmp___0^post2, nPacketsOld^0'=nPacketsOld^post2, (-nPacketsOld^post2+nPacketsOld^0 == 0 /\ loop_count^0-loop_count^post2 == 0 /\ loop_max^0-loop_max^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ nPackets^0-nPackets^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0), cost: 1
   3: l2 -> l3 : tmp^0'=tmp^post3, loop_max^0'=loop_max^post3, nPackets^0'=nPackets^post3, loop_count^0'=loop_count^post3, tmp___0^0'=tmp___0^post3, nPacketsOld^0'=nPacketsOld^post3, (loop_count^0-loop_count^post3 == 0 /\ -nPacketsOld^post3+nPacketsOld^0 == 0 /\ nPackets^0-nPackets^post3 == 0 /\ loop_max^0-loop_max^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0), cost: 1
  10: l3 -> l8 : tmp^0'=tmp^post10, loop_max^0'=loop_max^post10, nPackets^0'=nPackets^post10, loop_count^0'=loop_count^post10, tmp___0^0'=tmp___0^post10, nPacketsOld^0'=nPacketsOld^post10, (tmp^0-tmp^post10 == 0 /\ -loop_max^post10+loop_max^0 == 0 /\ nPackets^0-nPackets^post10 == 0 /\ loop_count^0-loop_count^post10 == 0 /\ -nPacketsOld^post10+nPacketsOld^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ 1-nPackets^0+nPacketsOld^0 <= 0), cost: 1
  11: l3 -> l8 : tmp^0'=tmp^post11, loop_max^0'=loop_max^post11, nPackets^0'=nPackets^post11, loop_count^0'=loop_count^post11, tmp___0^0'=tmp___0^post11, nPacketsOld^0'=nPacketsOld^post11, (loop_count^0-loop_count^post11 == 0 /\ -nPacketsOld^post11+nPacketsOld^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ 1+nPackets^0-nPacketsOld^0 <= 0 /\ nPackets^0-nPackets^post11 == 0 /\ loop_max^0-loop_max^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0), cost: 1
   4: l4 -> l2 : tmp^0'=tmp^post4, loop_max^0'=loop_max^post4, nPackets^0'=nPackets^post4, loop_count^0'=loop_count^post4, tmp___0^0'=tmp___0^post4, nPacketsOld^0'=nPacketsOld^post4, (nPackets^0-nPackets^post4 == 0 /\ loop_count^0-loop_count^post4 == 0 /\ -loop_max^post4+loop_max^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -nPacketsOld^post4+nPacketsOld^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0), cost: 1
   5: l4 -> l2 : tmp^0'=tmp^post5, loop_max^0'=loop_max^post5, nPackets^0'=nPackets^post5, loop_count^0'=loop_count^post5, tmp___0^0'=tmp___0^post5, nPacketsOld^0'=nPacketsOld^post5, (-nPacketsOld^post5+nPacketsOld^0 == 0 /\ -nPackets^post5+nPackets^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ loop_count^0-loop_count^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ loop_max^0-loop_max^post5 == 0), cost: 1
   6: l4 -> l3 : tmp^0'=tmp^post6, loop_max^0'=loop_max^post6, nPackets^0'=nPackets^post6, loop_count^0'=loop_count^post6, tmp___0^0'=tmp___0^post6, nPacketsOld^0'=nPacketsOld^post6, (tmp^0-tmp^post6 == 0 /\ -nPacketsOld^post6+nPacketsOld^0 == 0 /\ -nPackets^post6+nPackets^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -loop_count^post6+loop_count^0 == 0 /\ loop_max^0-loop_max^post6 == 0), cost: 1
   7: l5 -> l4 : tmp^0'=tmp^post7, loop_max^0'=loop_max^post7, nPackets^0'=nPackets^post7, loop_count^0'=loop_count^post7, tmp___0^0'=tmp___0^post7, nPacketsOld^0'=nPacketsOld^post7, (nPacketsOld^0-nPacketsOld^post7 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ nPackets^0-nPackets^post7 == 0 /\ loop_max^0-loop_max^post7 == 0 /\ -loop_count^post7+loop_count^0 == 0), cost: 1
  24: l8 -> l5 : tmp^0'=tmp^post24, loop_max^0'=loop_max^post24, nPackets^0'=nPackets^post24, loop_count^0'=loop_count^post24, tmp___0^0'=tmp___0^post24, nPacketsOld^0'=nPacketsOld^post24, (-nPackets^post24+nPackets^0 == 0 /\ nPacketsOld^post24-nPackets^0 == 0 /\ -loop_max^post24+loop_max^0 == 0 /\ tmp^0-tmp^post24 == 0 /\ loop_count^0-loop_count^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0), cost: 1
  13: l9 -> l3 : tmp^0'=tmp^post13, loop_max^0'=loop_max^post13, nPackets^0'=nPackets^post13, loop_count^0'=loop_count^post13, tmp___0^0'=tmp___0^post13, nPacketsOld^0'=nPacketsOld^post13, (tmp^0-tmp^post13 == 0 /\ loop_max^0-loop_max^post13 == 0 /\ -nPackets^post13+nPackets^0 == 0 /\ -nPacketsOld^post13+nPacketsOld^0 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -1+loop_count^post13-loop_count^0 == 0), cost: 1
  14: l10 -> l3 : tmp^0'=tmp^post14, loop_max^0'=loop_max^post14, nPackets^0'=nPackets^post14, loop_count^0'=loop_count^post14, tmp___0^0'=tmp___0^post14, nPacketsOld^0'=nPacketsOld^post14, (loop_max^0-loop_max^post14 == 0 /\ tmp^0-tmp^post14 == 0 /\ -nPackets^post14+nPackets^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ nPacketsOld^0-nPacketsOld^post14 == 0 /\ -tmp___0^0 <= 0 /\ tmp___0^0 <= 0 /\ -loop_count^post14+loop_count^0 == 0), cost: 1
  15: l10 -> l9 : tmp^0'=tmp^post15, loop_max^0'=loop_max^post15, nPackets^0'=nPackets^post15, loop_count^0'=loop_count^post15, tmp___0^0'=tmp___0^post15, nPacketsOld^0'=nPacketsOld^post15, (nPacketsOld^0-nPacketsOld^post15 == 0 /\ -loop_count^post15+loop_count^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ 1-tmp___0^0 <= 0 /\ loop_max^0-loop_max^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ nPackets^0-nPackets^post15 == 0), cost: 1
  16: l10 -> l9 : tmp^0'=tmp^post16, loop_max^0'=loop_max^post16, nPackets^0'=nPackets^post16, loop_count^0'=loop_count^post16, tmp___0^0'=tmp___0^post16, nPacketsOld^0'=nPacketsOld^post16, (tmp^0-tmp^post16 == 0 /\ 1+tmp___0^0 <= 0 /\ nPackets^0-nPackets^post16 == 0 /\ -loop_max^post16+loop_max^0 == 0 /\ -loop_count^post16+loop_count^0 == 0 /\ -nPacketsOld^post16+nPacketsOld^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1
  17: l11 -> l10 : tmp^0'=tmp^post17, loop_max^0'=loop_max^post17, nPackets^0'=nPackets^post17, loop_count^0'=loop_count^post17, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPacketsOld^post17, (0 == 0 /\ -nPacketsOld^post17+nPacketsOld^0 == 0 /\ tmp^0-tmp^post17 == 0 /\ -nPackets^post17+nPackets^0 == 0 /\ loop_count^0-loop_count^post17 == 0 /\ loop_max^0-loop_max^post17 == 0), cost: 1
  18: l12 -> l11 : tmp^0'=tmp^post18, loop_max^0'=loop_max^post18, nPackets^0'=nPackets^post18, loop_count^0'=loop_count^post18, tmp___0^0'=tmp___0^post18, nPacketsOld^0'=nPacketsOld^post18, (tmp^0-tmp^post18 == 0 /\ -1+nPackets^post18-nPackets^0 == 0 /\ loop_max^0-loop_max^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ -loop_count^post18+loop_count^0 == 0 /\ -nPacketsOld^post18+nPacketsOld^0 == 0), cost: 1
  19: l13 -> l11 : tmp^0'=tmp^post19, loop_max^0'=loop_max^post19, nPackets^0'=nPackets^post19, loop_count^0'=loop_count^post19, tmp___0^0'=tmp___0^post19, nPacketsOld^0'=nPacketsOld^post19, (tmp^0 <= 0 /\ tmp^0-tmp^post19 == 0 /\ -loop_count^post19+loop_count^0 == 0 /\ -nPackets^post19+nPackets^0 == 0 /\ loop_max^0-loop_max^post19 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -tmp^0 <= 0 /\ -nPacketsOld^post19+nPacketsOld^0 == 0), cost: 1
  20: l13 -> l12 : tmp^0'=tmp^post20, loop_max^0'=loop_max^post20, nPackets^0'=nPackets^post20, loop_count^0'=loop_count^post20, tmp___0^0'=tmp___0^post20, nPacketsOld^0'=nPacketsOld^post20, (loop_max^0-loop_max^post20 == 0 /\ -nPackets^post20+nPackets^0 == 0 /\ tmp^0-tmp^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ nPacketsOld^0-nPacketsOld^post20 == 0 /\ -loop_count^post20+loop_count^0 == 0 /\ 1-tmp^0 <= 0), cost: 1
  21: l13 -> l12 : tmp^0'=tmp^post21, loop_max^0'=loop_max^post21, nPackets^0'=nPackets^post21, loop_count^0'=loop_count^post21, tmp___0^0'=tmp___0^post21, nPacketsOld^0'=nPacketsOld^post21, (nPacketsOld^0-nPacketsOld^post21 == 0 /\ 1+tmp^0 <= 0 /\ -loop_count^post21+loop_count^0 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ loop_max^0-loop_max^post21 == 0 /\ tmp^0-tmp^post21 == 0 /\ nPackets^0-nPackets^post21 == 0), cost: 1
  22: l14 -> l13 : tmp^0'=tmp^post22, loop_max^0'=loop_max^post22, nPackets^0'=nPackets^post22, loop_count^0'=loop_count^post22, tmp___0^0'=tmp___0^post22, nPacketsOld^0'=nPacketsOld^post22, (0 == 0 /\ -nPacketsOld^post22+nPacketsOld^0 == 0 /\ loop_max^0-loop_max^post22 == 0 /\ loop_count^0-loop_count^post22 == 0 /\ nPackets^0-nPackets^post22 == 0 /\ -tmp___0^post22+tmp___0^0 == 0), cost: 1
  25: l15 -> l8 : tmp^0'=tmp^post25, loop_max^0'=loop_max^post25, nPackets^0'=nPackets^post25, loop_count^0'=loop_count^post25, tmp___0^0'=tmp___0^post25, nPacketsOld^0'=nPacketsOld^post25, (-nPackets^post25+nPackets^0 == 0 /\ -nPacketsOld^post25+nPacketsOld^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ loop_max^0-loop_max^post25 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ loop_count^0-loop_count^post25 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : tmp^0'=tmp^post0, loop_max^0'=loop_max^post0, nPackets^0'=nPackets^post0, loop_count^0'=loop_count^post0, tmp___0^0'=tmp___0^post0, nPacketsOld^0'=nPacketsOld^post0, (loop_max^0-loop_max^post0 == 0 /\ -nPackets^post0+nPackets^0 == 0 /\ -loop_count^post0+loop_count^0 == 0 /\ -nPacketsOld^post0+nPacketsOld^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ tmp^0-tmp^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : tmp^0'=tmp^post1, loop_max^0'=loop_max^post1, nPackets^0'=nPackets^post1, loop_count^0'=loop_count^post1, tmp___0^0'=tmp___0^post1, nPacketsOld^0'=nPacketsOld^post1, (-tmp___0^post1+tmp___0^0 == 0 /\ -loop_count^post1+loop_count^0 == 0 /\ -nPacketsOld^post1+nPacketsOld^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ nPackets^0-nPackets^post1 == 0 /\ loop_max^0-loop_max^post1 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : tmp^0'=tmp^post2, loop_max^0'=loop_max^post2, nPackets^0'=nPackets^post2, loop_count^0'=loop_count^post2, tmp___0^0'=tmp___0^post2, nPacketsOld^0'=nPacketsOld^post2, (-nPacketsOld^post2+nPacketsOld^0 == 0 /\ loop_count^0-loop_count^post2 == 0 /\ loop_max^0-loop_max^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ nPackets^0-nPackets^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : tmp^0'=tmp^post3, loop_max^0'=loop_max^post3, nPackets^0'=nPackets^post3, loop_count^0'=loop_count^post3, tmp___0^0'=tmp___0^post3, nPacketsOld^0'=nPacketsOld^post3, (loop_count^0-loop_count^post3 == 0 /\ -nPacketsOld^post3+nPacketsOld^0 == 0 /\ nPackets^0-nPackets^post3 == 0 /\ loop_max^0-loop_max^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0), cost: 1
New rule:
l2 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : tmp^0'=tmp^post4, loop_max^0'=loop_max^post4, nPackets^0'=nPackets^post4, loop_count^0'=loop_count^post4, tmp___0^0'=tmp___0^post4, nPacketsOld^0'=nPacketsOld^post4, (nPackets^0-nPackets^post4 == 0 /\ loop_count^0-loop_count^post4 == 0 /\ -loop_max^post4+loop_max^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -nPacketsOld^post4+nPacketsOld^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0), cost: 1
New rule:
l4 -> l2 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : tmp^0'=tmp^post5, loop_max^0'=loop_max^post5, nPackets^0'=nPackets^post5, loop_count^0'=loop_count^post5, tmp___0^0'=tmp___0^post5, nPacketsOld^0'=nPacketsOld^post5, (-nPacketsOld^post5+nPacketsOld^0 == 0 /\ -nPackets^post5+nPackets^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ loop_count^0-loop_count^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ loop_max^0-loop_max^post5 == 0), cost: 1
New rule:
l4 -> l2 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : tmp^0'=tmp^post6, loop_max^0'=loop_max^post6, nPackets^0'=nPackets^post6, loop_count^0'=loop_count^post6, tmp___0^0'=tmp___0^post6, nPacketsOld^0'=nPacketsOld^post6, (tmp^0-tmp^post6 == 0 /\ -nPacketsOld^post6+nPacketsOld^0 == 0 /\ -nPackets^post6+nPackets^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -loop_count^post6+loop_count^0 == 0 /\ loop_max^0-loop_max^post6 == 0), cost: 1
New rule:
l4 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l4 : tmp^0'=tmp^post7, loop_max^0'=loop_max^post7, nPackets^0'=nPackets^post7, loop_count^0'=loop_count^post7, tmp___0^0'=tmp___0^post7, nPacketsOld^0'=nPacketsOld^post7, (nPacketsOld^0-nPacketsOld^post7 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ nPackets^0-nPackets^post7 == 0 /\ loop_max^0-loop_max^post7 == 0 /\ -loop_count^post7+loop_count^0 == 0), cost: 1
New rule:
l5 -> l4 : 1-loop_max^0+loop_count^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l8 : tmp^0'=tmp^post10, loop_max^0'=loop_max^post10, nPackets^0'=nPackets^post10, loop_count^0'=loop_count^post10, tmp___0^0'=tmp___0^post10, nPacketsOld^0'=nPacketsOld^post10, (tmp^0-tmp^post10 == 0 /\ -loop_max^post10+loop_max^0 == 0 /\ nPackets^0-nPackets^post10 == 0 /\ loop_count^0-loop_count^post10 == 0 /\ -nPacketsOld^post10+nPacketsOld^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ 1-nPackets^0+nPacketsOld^0 <= 0), cost: 1
New rule:
l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l8 : tmp^0'=tmp^post11, loop_max^0'=loop_max^post11, nPackets^0'=nPackets^post11, loop_count^0'=loop_count^post11, tmp___0^0'=tmp___0^post11, nPacketsOld^0'=nPacketsOld^post11, (loop_count^0-loop_count^post11 == 0 /\ -nPacketsOld^post11+nPacketsOld^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ 1+nPackets^0-nPacketsOld^0 <= 0 /\ nPackets^0-nPackets^post11 == 0 /\ loop_max^0-loop_max^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0), cost: 1
New rule:
l3 -> l8 : 1+nPackets^0-nPacketsOld^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l3 : tmp^0'=tmp^post13, loop_max^0'=loop_max^post13, nPackets^0'=nPackets^post13, loop_count^0'=loop_count^post13, tmp___0^0'=tmp___0^post13, nPacketsOld^0'=nPacketsOld^post13, (tmp^0-tmp^post13 == 0 /\ loop_max^0-loop_max^post13 == 0 /\ -nPackets^post13+nPackets^0 == 0 /\ -nPacketsOld^post13+nPacketsOld^0 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -1+loop_count^post13-loop_count^0 == 0), cost: 1
New rule:
l9 -> l3 : loop_count^0'=1+loop_count^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l3 : tmp^0'=tmp^post14, loop_max^0'=loop_max^post14, nPackets^0'=nPackets^post14, loop_count^0'=loop_count^post14, tmp___0^0'=tmp___0^post14, nPacketsOld^0'=nPacketsOld^post14, (loop_max^0-loop_max^post14 == 0 /\ tmp^0-tmp^post14 == 0 /\ -nPackets^post14+nPackets^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ nPacketsOld^0-nPacketsOld^post14 == 0 /\ -tmp___0^0 <= 0 /\ tmp___0^0 <= 0 /\ -loop_count^post14+loop_count^0 == 0), cost: 1
New rule:
l10 -> l3 : tmp___0^0 == 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l9 : tmp^0'=tmp^post15, loop_max^0'=loop_max^post15, nPackets^0'=nPackets^post15, loop_count^0'=loop_count^post15, tmp___0^0'=tmp___0^post15, nPacketsOld^0'=nPacketsOld^post15, (nPacketsOld^0-nPacketsOld^post15 == 0 /\ -loop_count^post15+loop_count^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ 1-tmp___0^0 <= 0 /\ loop_max^0-loop_max^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ nPackets^0-nPackets^post15 == 0), cost: 1
New rule:
l10 -> l9 : -1+tmp___0^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l9 : tmp^0'=tmp^post16, loop_max^0'=loop_max^post16, nPackets^0'=nPackets^post16, loop_count^0'=loop_count^post16, tmp___0^0'=tmp___0^post16, nPacketsOld^0'=nPacketsOld^post16, (tmp^0-tmp^post16 == 0 /\ 1+tmp___0^0 <= 0 /\ nPackets^0-nPackets^post16 == 0 /\ -loop_max^post16+loop_max^0 == 0 /\ -loop_count^post16+loop_count^0 == 0 /\ -nPacketsOld^post16+nPacketsOld^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1
New rule:
l10 -> l9 : 1+tmp___0^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : tmp^0'=tmp^post17, loop_max^0'=loop_max^post17, nPackets^0'=nPackets^post17, loop_count^0'=loop_count^post17, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPacketsOld^post17, (0 == 0 /\ -nPacketsOld^post17+nPacketsOld^0 == 0 /\ tmp^0-tmp^post17 == 0 /\ -nPackets^post17+nPackets^0 == 0 /\ loop_count^0-loop_count^post17 == 0 /\ loop_max^0-loop_max^post17 == 0), cost: 1
New rule:
l11 -> l10 : tmp___0^0'=tmp___0^post17, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l11 : tmp^0'=tmp^post18, loop_max^0'=loop_max^post18, nPackets^0'=nPackets^post18, loop_count^0'=loop_count^post18, tmp___0^0'=tmp___0^post18, nPacketsOld^0'=nPacketsOld^post18, (tmp^0-tmp^post18 == 0 /\ -1+nPackets^post18-nPackets^0 == 0 /\ loop_max^0-loop_max^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ -loop_count^post18+loop_count^0 == 0 /\ -nPacketsOld^post18+nPacketsOld^0 == 0), cost: 1
New rule:
l12 -> l11 : nPackets^0'=1+nPackets^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l13 -> l11 : tmp^0'=tmp^post19, loop_max^0'=loop_max^post19, nPackets^0'=nPackets^post19, loop_count^0'=loop_count^post19, tmp___0^0'=tmp___0^post19, nPacketsOld^0'=nPacketsOld^post19, (tmp^0 <= 0 /\ tmp^0-tmp^post19 == 0 /\ -loop_count^post19+loop_count^0 == 0 /\ -nPackets^post19+nPackets^0 == 0 /\ loop_max^0-loop_max^post19 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -tmp^0 <= 0 /\ -nPacketsOld^post19+nPacketsOld^0 == 0), cost: 1
New rule:
l13 -> l11 : tmp^0 == 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : tmp^0'=tmp^post20, loop_max^0'=loop_max^post20, nPackets^0'=nPackets^post20, loop_count^0'=loop_count^post20, tmp___0^0'=tmp___0^post20, nPacketsOld^0'=nPacketsOld^post20, (loop_max^0-loop_max^post20 == 0 /\ -nPackets^post20+nPackets^0 == 0 /\ tmp^0-tmp^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ nPacketsOld^0-nPacketsOld^post20 == 0 /\ -loop_count^post20+loop_count^0 == 0 /\ 1-tmp^0 <= 0), cost: 1
New rule:
l13 -> l12 : -1+tmp^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : tmp^0'=tmp^post21, loop_max^0'=loop_max^post21, nPackets^0'=nPackets^post21, loop_count^0'=loop_count^post21, tmp___0^0'=tmp___0^post21, nPacketsOld^0'=nPacketsOld^post21, (nPacketsOld^0-nPacketsOld^post21 == 0 /\ 1+tmp^0 <= 0 /\ -loop_count^post21+loop_count^0 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ loop_max^0-loop_max^post21 == 0 /\ tmp^0-tmp^post21 == 0 /\ nPackets^0-nPackets^post21 == 0), cost: 1
New rule:
l13 -> l12 : 1+tmp^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l13 : tmp^0'=tmp^post22, loop_max^0'=loop_max^post22, nPackets^0'=nPackets^post22, loop_count^0'=loop_count^post22, tmp___0^0'=tmp___0^post22, nPacketsOld^0'=nPacketsOld^post22, (0 == 0 /\ -nPacketsOld^post22+nPacketsOld^0 == 0 /\ loop_max^0-loop_max^post22 == 0 /\ loop_count^0-loop_count^post22 == 0 /\ nPackets^0-nPackets^post22 == 0 /\ -tmp___0^post22+tmp___0^0 == 0), cost: 1
New rule:
l14 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l14 : tmp^0'=tmp^post23, loop_max^0'=loop_max^post23, nPackets^0'=nPackets^post23, loop_count^0'=loop_count^post23, tmp___0^0'=tmp___0^post23, nPacketsOld^0'=nPacketsOld^post23, (-tmp___0^post23+tmp___0^0 == 0 /\ loop_count^0-loop_count^post23 == 0 /\ nPackets^0-nPackets^post23 == 0 /\ -nPacketsOld^post23+nPacketsOld^0 == 0 /\ -loop_max^post23+loop_max^0 == 0 /\ tmp^0-tmp^post23 == 0), cost: 1
New rule:
l1 -> l14 : TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l5 : tmp^0'=tmp^post24, loop_max^0'=loop_max^post24, nPackets^0'=nPackets^post24, loop_count^0'=loop_count^post24, tmp___0^0'=tmp___0^post24, nPacketsOld^0'=nPacketsOld^post24, (-nPackets^post24+nPackets^0 == 0 /\ nPacketsOld^post24-nPackets^0 == 0 /\ -loop_max^post24+loop_max^0 == 0 /\ tmp^0-tmp^post24 == 0 /\ loop_count^0-loop_count^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0), cost: 1
New rule:
l8 -> l5 : nPacketsOld^0'=nPackets^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l15 -> l8 : tmp^0'=tmp^post25, loop_max^0'=loop_max^post25, nPackets^0'=nPackets^post25, loop_count^0'=loop_count^post25, tmp___0^0'=tmp___0^post25, nPacketsOld^0'=nPacketsOld^post25, (-nPackets^post25+nPackets^0 == 0 /\ -nPacketsOld^post25+nPacketsOld^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ loop_max^0-loop_max^post25 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ loop_count^0-loop_count^post25 == 0), cost: 1
New rule:
l15 -> l8 : TRUE, cost: 1

Simplified rules
Start location: l15
  26: l0 -> l1 : TRUE, cost: 1
  44: l1 -> l14 : TRUE, cost: 1
  27: l2 -> l0 : TRUE, cost: 1
  28: l2 -> l3 : TRUE, cost: 1
  32: l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
  33: l3 -> l8 : 1+nPackets^0-nPacketsOld^0 <= 0, cost: 1
  29: l4 -> l2 : TRUE, cost: 1
  30: l4 -> l3 : TRUE, cost: 1
  31: l5 -> l4 : 1-loop_max^0+loop_count^0 <= 0, cost: 1
  45: l8 -> l5 : nPacketsOld^0'=nPackets^0, TRUE, cost: 1
  34: l9 -> l3 : loop_count^0'=1+loop_count^0, TRUE, cost: 1
  35: l10 -> l3 : tmp___0^0 == 0, cost: 1
  36: l10 -> l9 : -1+tmp___0^0 >= 0, cost: 1
  37: l10 -> l9 : 1+tmp___0^0 <= 0, cost: 1
  38: l11 -> l10 : tmp___0^0'=tmp___0^post17, 0 == 0, cost: 1
  39: l12 -> l11 : nPackets^0'=1+nPackets^0, TRUE, cost: 1
  40: l13 -> l11 : tmp^0 == 0, cost: 1
  41: l13 -> l12 : -1+tmp^0 >= 0, cost: 1
  42: l13 -> l12 : 1+tmp^0 <= 0, cost: 1
  43: l14 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 1
  46: l15 -> l8 : TRUE, cost: 1


Eliminating location l5 by chaining:

Applied chaining
First rule:
l8 -> l5 : nPacketsOld^0'=nPackets^0, TRUE, cost: 1
Second rule:
l5 -> l4 : 1-loop_max^0+loop_count^0 <= 0, cost: 1
New rule:
l8 -> l4 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 31 45

Eliminating location l0 by chaining:

Applied chaining
First rule:
l2 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l1 : TRUE, cost: 1
New rule:
l2 -> l1 : TRUE, cost: 2

Applied deletion
Removed the following rules: 26 27

Eliminating location l1 by chaining:

Applied chaining
First rule:
l2 -> l1 : TRUE, cost: 2
Second rule:
l1 -> l14 : TRUE, cost: 1
New rule:
l2 -> l14 : TRUE, cost: 3

Applied deletion
Removed the following rules: 44 48

Eliminating location l14 by chaining:

Applied chaining
First rule:
l2 -> l14 : TRUE, cost: 3
Second rule:
l14 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 1
New rule:
l2 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 4

Applied deletion
Removed the following rules: 43 49

Eliminated locations on linear paths
Start location: l15
  28: l2 -> l3 : TRUE, cost: 1
  50: l2 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 4
  32: l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
  33: l3 -> l8 : 1+nPackets^0-nPacketsOld^0 <= 0, cost: 1
  29: l4 -> l2 : TRUE, cost: 1
  30: l4 -> l3 : TRUE, cost: 1
  47: l8 -> l4 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 2
  34: l9 -> l3 : loop_count^0'=1+loop_count^0, TRUE, cost: 1
  35: l10 -> l3 : tmp___0^0 == 0, cost: 1
  36: l10 -> l9 : -1+tmp___0^0 >= 0, cost: 1
  37: l10 -> l9 : 1+tmp___0^0 <= 0, cost: 1
  38: l11 -> l10 : tmp___0^0'=tmp___0^post17, 0 == 0, cost: 1
  39: l12 -> l11 : nPackets^0'=1+nPackets^0, TRUE, cost: 1
  40: l13 -> l11 : tmp^0 == 0, cost: 1
  41: l13 -> l12 : -1+tmp^0 >= 0, cost: 1
  42: l13 -> l12 : 1+tmp^0 <= 0, cost: 1
  46: l15 -> l8 : TRUE, cost: 1


Eliminating location l4 by chaining:

Applied chaining
First rule:
l8 -> l4 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 2
Second rule:
l4 -> l2 : TRUE, cost: 1
New rule:
l8 -> l2 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3

Applied chaining
First rule:
l8 -> l4 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 2
Second rule:
l4 -> l3 : TRUE, cost: 1
New rule:
l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3

Applied deletion
Removed the following rules: 29 30 47

Eliminating location l13 by chaining:

Applied chaining
First rule:
l2 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 4
Second rule:
l13 -> l11 : tmp^0 == 0, cost: 1
New rule:
l2 -> l11 : tmp^0'=tmp^post22, (0 == 0 /\ tmp^post22 == 0), cost: 5

Applied simplification
Original rule:
l2 -> l11 : tmp^0'=tmp^post22, (0 == 0 /\ tmp^post22 == 0), cost: 5
New rule:
l2 -> l11 : tmp^0'=tmp^post22, tmp^post22 == 0, cost: 5

Applied chaining
First rule:
l2 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 4
Second rule:
l13 -> l12 : -1+tmp^0 >= 0, cost: 1
New rule:
l2 -> l12 : tmp^0'=tmp^post22, (0 == 0 /\ -1+tmp^post22 >= 0), cost: 5

Applied simplification
Original rule:
l2 -> l12 : tmp^0'=tmp^post22, (0 == 0 /\ -1+tmp^post22 >= 0), cost: 5
New rule:
l2 -> l12 : tmp^0'=tmp^post22, -1+tmp^post22 >= 0, cost: 5

Applied chaining
First rule:
l2 -> l13 : tmp^0'=tmp^post22, 0 == 0, cost: 4
Second rule:
l13 -> l12 : 1+tmp^0 <= 0, cost: 1
New rule:
l2 -> l12 : tmp^0'=tmp^post22, (0 == 0 /\ 1+tmp^post22 <= 0), cost: 5

Applied simplification
Original rule:
l2 -> l12 : tmp^0'=tmp^post22, (0 == 0 /\ 1+tmp^post22 <= 0), cost: 5
New rule:
l2 -> l12 : tmp^0'=tmp^post22, 1+tmp^post22 <= 0, cost: 5

Applied deletion
Removed the following rules: 40 41 42 50

Eliminating location l10 by chaining:

Applied chaining
First rule:
l11 -> l10 : tmp___0^0'=tmp___0^post17, 0 == 0, cost: 1
Second rule:
l10 -> l3 : tmp___0^0 == 0, cost: 1
New rule:
l11 -> l3 : tmp___0^0'=tmp___0^post17, (0 == 0 /\ tmp___0^post17 == 0), cost: 2

Applied simplification
Original rule:
l11 -> l3 : tmp___0^0'=tmp___0^post17, (0 == 0 /\ tmp___0^post17 == 0), cost: 2
New rule:
l11 -> l3 : tmp___0^0'=tmp___0^post17, tmp___0^post17 == 0, cost: 2

Applied chaining
First rule:
l11 -> l10 : tmp___0^0'=tmp___0^post17, 0 == 0, cost: 1
Second rule:
l10 -> l9 : -1+tmp___0^0 >= 0, cost: 1
New rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, (0 == 0 /\ -1+tmp___0^post17 >= 0), cost: 2

Applied simplification
Original rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, (0 == 0 /\ -1+tmp___0^post17 >= 0), cost: 2
New rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 2

Applied chaining
First rule:
l11 -> l10 : tmp___0^0'=tmp___0^post17, 0 == 0, cost: 1
Second rule:
l10 -> l9 : 1+tmp___0^0 <= 0, cost: 1
New rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, (0 == 0 /\ 1+tmp___0^post17 <= 0), cost: 2

Applied simplification
Original rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, (0 == 0 /\ 1+tmp___0^post17 <= 0), cost: 2
New rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 2

Applied deletion
Removed the following rules: 35 36 37 38

Eliminated locations on tree-shaped paths
Start location: l15
  28: l2 -> l3 : TRUE, cost: 1
  53: l2 -> l11 : tmp^0'=tmp^post22, tmp^post22 == 0, cost: 5
  54: l2 -> l12 : tmp^0'=tmp^post22, -1+tmp^post22 >= 0, cost: 5
  55: l2 -> l12 : tmp^0'=tmp^post22, 1+tmp^post22 <= 0, cost: 5
  32: l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
  33: l3 -> l8 : 1+nPackets^0-nPacketsOld^0 <= 0, cost: 1
  51: l8 -> l2 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
  52: l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
  34: l9 -> l3 : loop_count^0'=1+loop_count^0, TRUE, cost: 1
  56: l11 -> l3 : tmp___0^0'=tmp___0^post17, tmp___0^post17 == 0, cost: 2
  57: l11 -> l9 : tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 2
  58: l11 -> l9 : tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 2
  39: l12 -> l11 : nPackets^0'=1+nPackets^0, TRUE, cost: 1
  46: l15 -> l8 : TRUE, cost: 1


Eliminating location l2 by chaining:

Applied chaining
First rule:
l8 -> l2 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
Second rule:
l2 -> l3 : TRUE, cost: 1
New rule:
l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 4

Applied chaining
First rule:
l8 -> l2 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
Second rule:
l2 -> l11 : tmp^0'=tmp^post22, tmp^post22 == 0, cost: 5
New rule:
l8 -> l11 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 8

Applied chaining
First rule:
l8 -> l2 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
Second rule:
l2 -> l12 : tmp^0'=tmp^post22, -1+tmp^post22 >= 0, cost: 5
New rule:
l8 -> l12 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 8

Applied chaining
First rule:
l8 -> l2 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
Second rule:
l2 -> l12 : tmp^0'=tmp^post22, 1+tmp^post22 <= 0, cost: 5
New rule:
l8 -> l12 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 8

Applied deletion
Removed the following rules: 28 51 53 54 55

Eliminating location l9 by chaining:

Applied chaining
First rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 2
Second rule:
l9 -> l3 : loop_count^0'=1+loop_count^0, TRUE, cost: 1
New rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 3

Applied chaining
First rule:
l11 -> l9 : tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 2
Second rule:
l9 -> l3 : loop_count^0'=1+loop_count^0, TRUE, cost: 1
New rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 3

Applied deletion
Removed the following rules: 34 57 58

Eliminated locations on tree-shaped paths
Start location: l15
  32: l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
  33: l3 -> l8 : 1+nPackets^0-nPacketsOld^0 <= 0, cost: 1
  52: l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
  59: l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 4
  60: l8 -> l11 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 8
  61: l8 -> l12 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 8
  62: l8 -> l12 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 8
  56: l11 -> l3 : tmp___0^0'=tmp___0^post17, tmp___0^post17 == 0, cost: 2
  63: l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 3
  64: l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 3
  39: l12 -> l11 : nPackets^0'=1+nPackets^0, TRUE, cost: 1
  46: l15 -> l8 : TRUE, cost: 1


Eliminating location l12 by chaining:

Applied chaining
First rule:
l8 -> l12 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 8
Second rule:
l12 -> l11 : nPackets^0'=1+nPackets^0, TRUE, cost: 1
New rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 9

Applied chaining
First rule:
l8 -> l12 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 8
Second rule:
l12 -> l11 : nPackets^0'=1+nPackets^0, TRUE, cost: 1
New rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 9

Applied deletion
Removed the following rules: 39 61 62

Eliminated locations on tree-shaped paths
Start location: l15
  32: l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
  33: l3 -> l8 : 1+nPackets^0-nPacketsOld^0 <= 0, cost: 1
  52: l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
  59: l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 4
  60: l8 -> l11 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 8
  65: l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 9
  66: l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 9
  56: l11 -> l3 : tmp___0^0'=tmp___0^post17, tmp___0^post17 == 0, cost: 2
  63: l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 3
  64: l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 3
  46: l15 -> l8 : TRUE, cost: 1


Eliminating location l11 by chaining:

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 8
Second rule:
l11 -> l3 : tmp___0^0'=tmp___0^post17, tmp___0^post17 == 0, cost: 2
New rule:
l8 -> l3 : tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 10

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 8
Second rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 3
New rule:
l8 -> l3 : tmp^0'=tmp^post22, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0 /\ -1+tmp___0^post17 >= 0), cost: 11

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 8
Second rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 3
New rule:
l8 -> l3 : tmp^0'=tmp^post22, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 11

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 9
Second rule:
l11 -> l3 : tmp___0^0'=tmp___0^post17, tmp___0^post17 == 0, cost: 2
New rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 11

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 9
Second rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 3
New rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 12

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 9
Second rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 3
New rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 9
Second rule:
l11 -> l3 : tmp___0^0'=tmp___0^post17, tmp___0^post17 == 0, cost: 2
New rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 11

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 9
Second rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, -1+tmp___0^post17 >= 0, cost: 3
New rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 12

Applied chaining
First rule:
l8 -> l11 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 9
Second rule:
l11 -> l3 : loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, 1+tmp___0^post17 <= 0, cost: 3
New rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12

Applied deletion
Removed the following rules: 56 60 63 64 65 66

Eliminated locations on tree-shaped paths
Start location: l15
  32: l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
  33: l3 -> l8 : 1+nPackets^0-nPacketsOld^0 <= 0, cost: 1
  52: l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 3
  59: l8 -> l3 : nPacketsOld^0'=nPackets^0, 1-loop_max^0+loop_count^0 <= 0, cost: 4
  67: l8 -> l3 : tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 10
  68: l8 -> l3 : tmp^0'=tmp^post22, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0 /\ -1+tmp___0^post17 >= 0), cost: 11
  69: l8 -> l3 : tmp^0'=tmp^post22, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ tmp^post22 == 0), cost: 11
  70: l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 11
  71: l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 12
  72: l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12
  73: l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 11
  74: l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 12
  75: l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12
  46: l15 -> l8 : TRUE, cost: 1


Eliminating location l3 by chaining:

Applied chaining
First rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 11
Second rule:
l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12

Applied chaining
First rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 12
Second rule:
l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13

Applied chaining
First rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12
Second rule:
l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ -1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 13

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ -1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 13

Applied chaining
First rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 11
Second rule:
l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12

Applied chaining
First rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 12
Second rule:
l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13

Applied chaining
First rule:
l8 -> l3 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12
Second rule:
l3 -> l8 : 1-nPackets^0+nPacketsOld^0 <= 0, cost: 1
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 13

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (0 <= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 13

Applied deletion
Removed the following rules: 32 33 52 59 67 68 69 70 71 72 73 74 75

Eliminated locations on tree-shaped paths
Start location: l15
  76: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12
  77: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
  78: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 13
  79: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12
  80: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
  81: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 13
  46: l15 -> l8 : TRUE, cost: 1


Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ -1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (tmp___0^post17 == 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12

Simplified simple loops
Start location: l15
  77: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
  78: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 13
  80: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
  81: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 13
  82: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12
  83: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12
  46: l15 -> l8 : TRUE, cost: 1


Applied acceleration
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=n+nPackets^0, loop_count^0'=n+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+n+nPackets^0, (loop_max^0-n-loop_count^0 >= 0 /\ -1+tmp^post22 >= 0 /\ -1+n >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_jNhNON.txt

Applied instantiation
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=n+nPackets^0, loop_count^0'=n+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+n+nPackets^0, (loop_max^0-n-loop_count^0 >= 0 /\ -1+tmp^post22 >= 0 /\ -1+n >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*n
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied acceleration
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=n0+nPackets^0, loop_count^0'=n0+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+n0+nPackets^0, (-1+tmp^post22 >= 0 /\ -1-tmp___0^post17 >= 0 /\ -n0+loop_max^0-loop_count^0 >= 0 /\ -1+n0 >= 0), cost: 13*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_BOGlgP.txt

Applied instantiation
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=n0+nPackets^0, loop_count^0'=n0+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+n0+nPackets^0, (-1+tmp^post22 >= 0 /\ -1-tmp___0^post17 >= 0 /\ -n0+loop_max^0-loop_count^0 >= 0 /\ -1+n0 >= 0), cost: 13*n0
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1+tmp^post22 >= 0 /\ -1-tmp___0^post17 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied acceleration
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+tmp___0^post17 >= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=n1+nPackets^0, loop_count^0'=n1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+n1+nPackets^0, (-n1+loop_max^0-loop_count^0 >= 0 /\ -1+n1 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_jLMBol.txt

Applied instantiation
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=n1+nPackets^0, loop_count^0'=n1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+n1+nPackets^0, (-n1+loop_max^0-loop_count^0 >= 0 /\ -1+n1 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*n1
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied acceleration
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, loop_count^0'=1+loop_count^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=nPackets^0, (1+tmp___0^post17 <= 0 /\ 1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 13
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=nPackets^0+n2, loop_count^0'=loop_count^0+n2, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+nPackets^0+n2, (-1+n2 >= 0 /\ -1-tmp___0^post17 >= 0 /\ loop_max^0-loop_count^0-n2 >= 0 /\ -1-tmp^post22 >= 0), cost: 13*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pFkkFA.txt

Applied instantiation
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=nPackets^0+n2, loop_count^0'=loop_count^0+n2, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+nPackets^0+n2, (-1+n2 >= 0 /\ -1-tmp___0^post17 >= 0 /\ loop_max^0-loop_count^0-n2 >= 0 /\ -1-tmp^post22 >= 0), cost: 13*n2
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1-tmp___0^post17 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied nonterm
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=0, nPacketsOld^0'=nPackets^0, (-1+tmp^post22 >= 0 /\ 1-loop_max^0+loop_count^0 <= 0), cost: 12
New rule:
l8 -> [16] : (-1+n3 >= 0 /\ -1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ammFge.txt

Applied nonterm
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=1+nPackets^0, tmp___0^0'=0, nPacketsOld^0'=nPackets^0, (1-loop_max^0+loop_count^0 <= 0 /\ 1+tmp^post22 <= 0), cost: 12
New rule:
l8 -> [16] : (-1+n4 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_cGOENi.txt

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1+tmp^post22 >= 0 /\ -1-tmp___0^post17 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied simplification
Original rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (0 >= 0 /\ -1-tmp___0^post17 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp___0^post17 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0

Applied simplification
Original rule:
l8 -> [16] : (-1+n4 >= 0 /\ -1-tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM
New rule:
l8 -> [16] : (-1+n4 >= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 77 78 80 81 82 83

Accelerated simple loops
Start location: l15
  88: l8 -> [16] : (-1+n3 >= 0 /\ -1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM
  90: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0
  91: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0
  92: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0
  93: l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp___0^post17 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0
  94: l8 -> [16] : (-1+n4 >= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM
  46: l15 -> l8 : TRUE, cost: 1


Applied chaining
First rule:
l15 -> l8 : TRUE, cost: 1
Second rule:
l8 -> [16] : (-1+n3 >= 0 /\ -1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM
New rule:
l15 -> [16] : -1+loop_max^0-loop_count^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l15 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 1+13*loop_max^0-13*loop_count^0

Applied chaining
First rule:
l15 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 1+13*loop_max^0-13*loop_count^0

Applied chaining
First rule:
l15 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 1+13*loop_max^0-13*loop_count^0

Applied chaining
First rule:
l15 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp___0^post17 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 13*loop_max^0-13*loop_count^0
New rule:
l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp___0^post17 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 1+13*loop_max^0-13*loop_count^0

Applied chaining
First rule:
l15 -> l8 : TRUE, cost: 1
Second rule:
l8 -> [16] : (-1+n4 >= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: NONTERM
New rule:
l15 -> [16] : -1+loop_max^0-loop_count^0 >= 0, cost: NONTERM

Applied deletion
Removed the following rules: 88 90 91 92 93 94

Chained accelerated rules with incoming rules
Start location: l15
  46: l15 -> l8 : TRUE, cost: 1
  95: l15 -> [16] : -1+loop_max^0-loop_count^0 >= 0, cost: NONTERM
  96: l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 1+13*loop_max^0-13*loop_count^0
  97: l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (-1+tmp^post22 >= 0 /\ 1+tmp___0^post17 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 1+13*loop_max^0-13*loop_count^0
  98: l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0 /\ -1+tmp___0^post17 >= 0), cost: 1+13*loop_max^0-13*loop_count^0
  99: l15 -> l8 : tmp^0'=tmp^post22, nPackets^0'=loop_max^0+nPackets^0-loop_count^0, loop_count^0'=loop_max^0, tmp___0^0'=tmp___0^post17, nPacketsOld^0'=-1+loop_max^0+nPackets^0-loop_count^0, (1+tmp___0^post17 <= 0 /\ 1+tmp^post22 <= 0 /\ -1+loop_max^0-loop_count^0 >= 0), cost: 1+13*loop_max^0-13*loop_count^0


Removed unreachable locations and irrelevant leafs
Start location: l15
  95: l15 -> [16] : -1+loop_max^0-loop_count^0 >= 0, cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 95 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  -1+loop_max^0-loop_count^0 >= 0