unknown

Initial ITS

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
   0: l0 -> l1 : edgecount^0'=edgecount^post1, i^0'=i^post1, j^0'=j^post1, nodecount^0'=nodecount^post1, source^0'=source^post1, x^0'=x^post1, y^0'=y^post1, (-nodecount^post1+nodecount^0 == 0 /\ -i^post1+i^0 == 0 /\ nodecount^0-i^0 <= 0 /\ -j^post1+j^0 == 0 /\ x^0-x^post1 == 0 /\ edgecount^0-edgecount^post1 == 0 /\ source^0-source^post1 == 0 /\ -y^post1+y^0 == 0), cost: 1
   1: l0 -> l2 : edgecount^0'=edgecount^post2, i^0'=i^post2, j^0'=j^post2, nodecount^0'=nodecount^post2, source^0'=source^post2, x^0'=x^post2, y^0'=y^post2, (-x^post2+x^0 == 0 /\ y^0-y^post2 == 0 /\ source^0-source^post2 == 0 /\ edgecount^0-edgecount^post2 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -nodecount^post2+nodecount^0 == 0 /\ -j^post2+j^0 == 0 /\ -1+i^post2-i^0 == 0), cost: 1
  22: l2 -> l0 : edgecount^0'=edgecount^post23, i^0'=i^post23, j^0'=j^post23, nodecount^0'=nodecount^post23, source^0'=source^post23, x^0'=x^post23, y^0'=y^post23, (y^0-y^post23 == 0 /\ -x^post23+x^0 == 0 /\ j^0-j^post23 == 0 /\ nodecount^0-nodecount^post23 == 0 /\ -i^post23+i^0 == 0 /\ edgecount^0-edgecount^post23 == 0 /\ -source^post23+source^0 == 0), cost: 1
   2: l3 -> l4 : edgecount^0'=edgecount^post3, i^0'=i^post3, j^0'=j^post3, nodecount^0'=nodecount^post3, source^0'=source^post3, x^0'=x^post3, y^0'=y^post3, (edgecount^0-edgecount^post3 == 0 /\ -i^post3+i^0 == 0 /\ -x^post3+x^0 == 0 /\ y^0-y^post3 == 0 /\ j^0-j^post3 == 0 /\ source^0-source^post3 == 0 /\ -nodecount^post3+nodecount^0 == 0), cost: 1
  20: l4 -> l8 : edgecount^0'=edgecount^post21, i^0'=i^post21, j^0'=j^post21, nodecount^0'=nodecount^post21, source^0'=source^post21, x^0'=x^post21, y^0'=y^post21, (-j^post21+j^0 == 0 /\ nodecount^0-i^0 <= 0 /\ edgecount^0-edgecount^post21 == 0 /\ source^0-source^post21 == 0 /\ -x^post21+x^0 == 0 /\ -y^post21+y^0 == 0 /\ i^post21 == 0 /\ -nodecount^post21+nodecount^0 == 0), cost: 1
  21: l4 -> l15 : edgecount^0'=edgecount^post22, i^0'=i^post22, j^0'=j^post22, nodecount^0'=nodecount^post22, source^0'=source^post22, x^0'=x^post22, y^0'=y^post22, (-x^post22+x^0 == 0 /\ y^0-y^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ source^0-source^post22 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -i^post22+i^0 == 0 /\ edgecount^0-edgecount^post22 == 0 /\ j^0-j^post22 == 0), cost: 1
   3: l5 -> l6 : edgecount^0'=edgecount^post4, i^0'=i^post4, j^0'=j^post4, nodecount^0'=nodecount^post4, source^0'=source^post4, x^0'=x^post4, y^0'=y^post4, (-1+i^post4-i^0 == 0 /\ -source^post4+source^0 == 0 /\ j^0-j^post4 == 0 /\ y^0-y^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ edgecount^0-edgecount^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1
   4: l5 -> l1 : edgecount^0'=edgecount^post5, i^0'=i^post5, j^0'=j^post5, nodecount^0'=nodecount^post5, source^0'=source^post5, x^0'=x^post5, y^0'=y^post5, (nodecount^0-nodecount^post5 == 0 /\ y^0-y^post5 == 0 /\ source^0-source^post5 == 0 /\ edgecount^0-edgecount^post5 == 0 /\ -i^post5+i^0 == 0 /\ -x^post5+x^0 == 0 /\ j^0-j^post5 == 0), cost: 1
  16: l6 -> l7 : edgecount^0'=edgecount^post17, i^0'=i^post17, j^0'=j^post17, nodecount^0'=nodecount^post17, source^0'=source^post17, x^0'=x^post17, y^0'=y^post17, (-source^post17+source^0 == 0 /\ j^0-j^post17 == 0 /\ -i^post17+i^0 == 0 /\ nodecount^0-nodecount^post17 == 0 /\ y^0-y^post17 == 0 /\ -x^post17+x^0 == 0 /\ edgecount^0-edgecount^post17 == 0), cost: 1
   5: l7 -> l2 : edgecount^0'=edgecount^post6, i^0'=i^post6, j^0'=j^post6, nodecount^0'=nodecount^post6, source^0'=source^post6, x^0'=x^post6, y^0'=y^post6, (source^0-source^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ i^post6 == 0 /\ edgecount^0-i^0 <= 0 /\ -y^post6+y^0 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ x^0-x^post6 == 0), cost: 1
   6: l7 -> l5 : edgecount^0'=edgecount^post7, i^0'=i^post7, j^0'=j^post7, nodecount^0'=nodecount^post7, source^0'=source^post7, x^0'=x^post7, y^0'=y^post7, (0 == 0 /\ -i^post7+i^0 == 0 /\ source^0-source^post7 == 0 /\ -nodecount^post7+nodecount^0 == 0 /\ -j^post7+j^0 == 0 /\ edgecount^0-edgecount^post7 == 0 /\ 1-edgecount^0+i^0 <= 0), cost: 1
   7: l8 -> l9 : edgecount^0'=edgecount^post8, i^0'=i^post8, j^0'=j^post8, nodecount^0'=nodecount^post8, source^0'=source^post8, x^0'=x^post8, y^0'=y^post8, (-i^post8+i^0 == 0 /\ -x^post8+x^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ edgecount^0-edgecount^post8 == 0 /\ y^0-y^post8 == 0 /\ j^0-j^post8 == 0 /\ -source^post8+source^0 == 0), cost: 1
  12: l9 -> l6 : edgecount^0'=edgecount^post13, i^0'=i^post13, j^0'=j^post13, nodecount^0'=nodecount^post13, source^0'=source^post13, x^0'=x^post13, y^0'=y^post13, (i^post13 == 0 /\ source^0-source^post13 == 0 /\ j^0-j^post13 == 0 /\ edgecount^0-edgecount^post13 == 0 /\ nodecount^0-i^0 <= 0 /\ -x^post13+x^0 == 0 /\ y^0-y^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0), cost: 1
  13: l9 -> l11 : edgecount^0'=edgecount^post14, i^0'=i^post14, j^0'=j^post14, nodecount^0'=nodecount^post14, source^0'=source^post14, x^0'=x^post14, y^0'=y^post14, (nodecount^0-nodecount^post14 == 0 /\ y^0-y^post14 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -i^post14+i^0 == 0 /\ j^post14 == 0 /\ source^0-source^post14 == 0 /\ -x^post14+x^0 == 0 /\ edgecount^0-edgecount^post14 == 0), cost: 1
   8: l10 -> l11 : edgecount^0'=edgecount^post9, i^0'=i^post9, j^0'=j^post9, nodecount^0'=nodecount^post9, source^0'=source^post9, x^0'=x^post9, y^0'=y^post9, (nodecount^0-nodecount^post9 == 0 /\ source^0-source^post9 == 0 /\ -1-j^0+j^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^post9+i^0 == 0 /\ -x^post9+x^0 == 0 /\ -y^post9+y^0 == 0), cost: 1
   9: l11 -> l12 : edgecount^0'=edgecount^post10, i^0'=i^post10, j^0'=j^post10, nodecount^0'=nodecount^post10, source^0'=source^post10, x^0'=x^post10, y^0'=y^post10, (-i^post10+i^0 == 0 /\ -y^post10+y^0 == 0 /\ j^0-j^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ x^0-x^post10 == 0 /\ source^0-source^post10 == 0 /\ edgecount^0-edgecount^post10 == 0), cost: 1
  10: l12 -> l8 : edgecount^0'=edgecount^post11, i^0'=i^post11, j^0'=j^post11, nodecount^0'=nodecount^post11, source^0'=source^post11, x^0'=x^post11, y^0'=y^post11, (-j^post11+j^0 == 0 /\ -j^0+edgecount^0 <= 0 /\ -1+i^post11-i^0 == 0 /\ -y^post11+y^0 == 0 /\ source^0-source^post11 == 0 /\ -x^post11+x^0 == 0 /\ edgecount^0-edgecount^post11 == 0 /\ -nodecount^post11+nodecount^0 == 0), cost: 1
  11: l12 -> l10 : edgecount^0'=edgecount^post12, i^0'=i^post12, j^0'=j^post12, nodecount^0'=nodecount^post12, source^0'=source^post12, x^0'=x^post12, y^0'=y^post12, (0 == 0 /\ edgecount^0-edgecount^post12 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post12 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0), cost: 1
  14: l13 -> l14 : edgecount^0'=edgecount^post15, i^0'=i^post15, j^0'=j^post15, nodecount^0'=nodecount^post15, source^0'=source^post15, x^0'=x^post15, y^0'=y^post15, (-i^post15+i^0 == 0 /\ -edgecount^post15+edgecount^0 == 0 /\ source^0-source^post15 == 0 /\ j^0-j^post15 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ -x^post15+x^0 == 0 /\ -y^post15+y^0 == 0), cost: 1
  15: l14 -> l3 : edgecount^0'=edgecount^post16, i^0'=i^post16, j^0'=j^post16, nodecount^0'=nodecount^post16, source^0'=source^post16, x^0'=x^post16, y^0'=y^post16, (y^0-y^post16 == 0 /\ -1+i^post16-i^0 == 0 /\ j^0-j^post16 == 0 /\ -x^post16+x^0 == 0 /\ -nodecount^post16+nodecount^0 == 0 /\ edgecount^0-edgecount^post16 == 0 /\ source^0-source^post16 == 0), cost: 1
  17: l15 -> l13 : edgecount^0'=edgecount^post18, i^0'=i^post18, j^0'=j^post18, nodecount^0'=nodecount^post18, source^0'=source^post18, x^0'=x^post18, y^0'=y^post18, (nodecount^0-nodecount^post18 == 0 /\ 1+source^0-i^0 <= 0 /\ y^0-y^post18 == 0 /\ j^0-j^post18 == 0 /\ source^0-source^post18 == 0 /\ -x^post18+x^0 == 0 /\ edgecount^0-edgecount^post18 == 0 /\ -i^post18+i^0 == 0), cost: 1
  18: l15 -> l13 : edgecount^0'=edgecount^post19, i^0'=i^post19, j^0'=j^post19, nodecount^0'=nodecount^post19, source^0'=source^post19, x^0'=x^post19, y^0'=y^post19, (j^0-j^post19 == 0 /\ source^0-source^post19 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ 1-source^0+i^0 <= 0 /\ -y^post19+y^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ -i^post19+i^0 == 0 /\ x^0-x^post19 == 0), cost: 1
  19: l15 -> l14 : edgecount^0'=edgecount^post20, i^0'=i^post20, j^0'=j^post20, nodecount^0'=nodecount^post20, source^0'=source^post20, x^0'=x^post20, y^0'=y^post20, (source^0-i^0 <= 0 /\ -i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^0 == 0 /\ -source^0+i^0 <= 0 /\ -j^post20+j^0 == 0 /\ x^0-x^post20 == 0 /\ edgecount^0-edgecount^post20 == 0 /\ source^0-source^post20 == 0 /\ -y^post20+y^0 == 0), cost: 1
  23: l16 -> l3 : edgecount^0'=edgecount^post24, i^0'=i^post24, j^0'=j^post24, nodecount^0'=nodecount^post24, source^0'=source^post24, x^0'=x^post24, y^0'=y^post24, (y^0-y^post24 == 0 /\ -5+nodecount^post24 == 0 /\ source^post24 == 0 /\ i^post24 == 0 /\ -6+edgecount^post24 == 0 /\ -x^post24+x^0 == 0 /\ j^0-j^post24 == 0), cost: 1
  24: l17 -> l16 : edgecount^0'=edgecount^post25, i^0'=i^post25, j^0'=j^post25, nodecount^0'=nodecount^post25, source^0'=source^post25, x^0'=x^post25, y^0'=y^post25, (j^0-j^post25 == 0 /\ source^0-source^post25 == 0 /\ y^0-y^post25 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1

Chained Linear Paths

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
   0: l0 -> l1 : edgecount^0'=edgecount^post1, i^0'=i^post1, j^0'=j^post1, nodecount^0'=nodecount^post1, source^0'=source^post1, x^0'=x^post1, y^0'=y^post1, (-nodecount^post1+nodecount^0 == 0 /\ -i^post1+i^0 == 0 /\ nodecount^0-i^0 <= 0 /\ -j^post1+j^0 == 0 /\ x^0-x^post1 == 0 /\ edgecount^0-edgecount^post1 == 0 /\ source^0-source^post1 == 0 /\ -y^post1+y^0 == 0), cost: 1
   1: l0 -> l2 : edgecount^0'=edgecount^post2, i^0'=i^post2, j^0'=j^post2, nodecount^0'=nodecount^post2, source^0'=source^post2, x^0'=x^post2, y^0'=y^post2, (-x^post2+x^0 == 0 /\ y^0-y^post2 == 0 /\ source^0-source^post2 == 0 /\ edgecount^0-edgecount^post2 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -nodecount^post2+nodecount^0 == 0 /\ -j^post2+j^0 == 0 /\ -1+i^post2-i^0 == 0), cost: 1
  22: l2 -> l0 : edgecount^0'=edgecount^post23, i^0'=i^post23, j^0'=j^post23, nodecount^0'=nodecount^post23, source^0'=source^post23, x^0'=x^post23, y^0'=y^post23, (y^0-y^post23 == 0 /\ -x^post23+x^0 == 0 /\ j^0-j^post23 == 0 /\ nodecount^0-nodecount^post23 == 0 /\ -i^post23+i^0 == 0 /\ edgecount^0-edgecount^post23 == 0 /\ -source^post23+source^0 == 0), cost: 1
   2: l3 -> l4 : edgecount^0'=edgecount^post3, i^0'=i^post3, j^0'=j^post3, nodecount^0'=nodecount^post3, source^0'=source^post3, x^0'=x^post3, y^0'=y^post3, (edgecount^0-edgecount^post3 == 0 /\ -i^post3+i^0 == 0 /\ -x^post3+x^0 == 0 /\ y^0-y^post3 == 0 /\ j^0-j^post3 == 0 /\ source^0-source^post3 == 0 /\ -nodecount^post3+nodecount^0 == 0), cost: 1
  20: l4 -> l8 : edgecount^0'=edgecount^post21, i^0'=i^post21, j^0'=j^post21, nodecount^0'=nodecount^post21, source^0'=source^post21, x^0'=x^post21, y^0'=y^post21, (-j^post21+j^0 == 0 /\ nodecount^0-i^0 <= 0 /\ edgecount^0-edgecount^post21 == 0 /\ source^0-source^post21 == 0 /\ -x^post21+x^0 == 0 /\ -y^post21+y^0 == 0 /\ i^post21 == 0 /\ -nodecount^post21+nodecount^0 == 0), cost: 1
  21: l4 -> l15 : edgecount^0'=edgecount^post22, i^0'=i^post22, j^0'=j^post22, nodecount^0'=nodecount^post22, source^0'=source^post22, x^0'=x^post22, y^0'=y^post22, (-x^post22+x^0 == 0 /\ y^0-y^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ source^0-source^post22 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -i^post22+i^0 == 0 /\ edgecount^0-edgecount^post22 == 0 /\ j^0-j^post22 == 0), cost: 1
   3: l5 -> l6 : edgecount^0'=edgecount^post4, i^0'=i^post4, j^0'=j^post4, nodecount^0'=nodecount^post4, source^0'=source^post4, x^0'=x^post4, y^0'=y^post4, (-1+i^post4-i^0 == 0 /\ -source^post4+source^0 == 0 /\ j^0-j^post4 == 0 /\ y^0-y^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ edgecount^0-edgecount^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1
   4: l5 -> l1 : edgecount^0'=edgecount^post5, i^0'=i^post5, j^0'=j^post5, nodecount^0'=nodecount^post5, source^0'=source^post5, x^0'=x^post5, y^0'=y^post5, (nodecount^0-nodecount^post5 == 0 /\ y^0-y^post5 == 0 /\ source^0-source^post5 == 0 /\ edgecount^0-edgecount^post5 == 0 /\ -i^post5+i^0 == 0 /\ -x^post5+x^0 == 0 /\ j^0-j^post5 == 0), cost: 1
  16: l6 -> l7 : edgecount^0'=edgecount^post17, i^0'=i^post17, j^0'=j^post17, nodecount^0'=nodecount^post17, source^0'=source^post17, x^0'=x^post17, y^0'=y^post17, (-source^post17+source^0 == 0 /\ j^0-j^post17 == 0 /\ -i^post17+i^0 == 0 /\ nodecount^0-nodecount^post17 == 0 /\ y^0-y^post17 == 0 /\ -x^post17+x^0 == 0 /\ edgecount^0-edgecount^post17 == 0), cost: 1
   5: l7 -> l2 : edgecount^0'=edgecount^post6, i^0'=i^post6, j^0'=j^post6, nodecount^0'=nodecount^post6, source^0'=source^post6, x^0'=x^post6, y^0'=y^post6, (source^0-source^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ i^post6 == 0 /\ edgecount^0-i^0 <= 0 /\ -y^post6+y^0 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ x^0-x^post6 == 0), cost: 1
   6: l7 -> l5 : edgecount^0'=edgecount^post7, i^0'=i^post7, j^0'=j^post7, nodecount^0'=nodecount^post7, source^0'=source^post7, x^0'=x^post7, y^0'=y^post7, (0 == 0 /\ -i^post7+i^0 == 0 /\ source^0-source^post7 == 0 /\ -nodecount^post7+nodecount^0 == 0 /\ -j^post7+j^0 == 0 /\ edgecount^0-edgecount^post7 == 0 /\ 1-edgecount^0+i^0 <= 0), cost: 1
   7: l8 -> l9 : edgecount^0'=edgecount^post8, i^0'=i^post8, j^0'=j^post8, nodecount^0'=nodecount^post8, source^0'=source^post8, x^0'=x^post8, y^0'=y^post8, (-i^post8+i^0 == 0 /\ -x^post8+x^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ edgecount^0-edgecount^post8 == 0 /\ y^0-y^post8 == 0 /\ j^0-j^post8 == 0 /\ -source^post8+source^0 == 0), cost: 1
  12: l9 -> l6 : edgecount^0'=edgecount^post13, i^0'=i^post13, j^0'=j^post13, nodecount^0'=nodecount^post13, source^0'=source^post13, x^0'=x^post13, y^0'=y^post13, (i^post13 == 0 /\ source^0-source^post13 == 0 /\ j^0-j^post13 == 0 /\ edgecount^0-edgecount^post13 == 0 /\ nodecount^0-i^0 <= 0 /\ -x^post13+x^0 == 0 /\ y^0-y^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0), cost: 1
  13: l9 -> l11 : edgecount^0'=edgecount^post14, i^0'=i^post14, j^0'=j^post14, nodecount^0'=nodecount^post14, source^0'=source^post14, x^0'=x^post14, y^0'=y^post14, (nodecount^0-nodecount^post14 == 0 /\ y^0-y^post14 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -i^post14+i^0 == 0 /\ j^post14 == 0 /\ source^0-source^post14 == 0 /\ -x^post14+x^0 == 0 /\ edgecount^0-edgecount^post14 == 0), cost: 1
   9: l11 -> l12 : edgecount^0'=edgecount^post10, i^0'=i^post10, j^0'=j^post10, nodecount^0'=nodecount^post10, source^0'=source^post10, x^0'=x^post10, y^0'=y^post10, (-i^post10+i^0 == 0 /\ -y^post10+y^0 == 0 /\ j^0-j^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ x^0-x^post10 == 0 /\ source^0-source^post10 == 0 /\ edgecount^0-edgecount^post10 == 0), cost: 1
  10: l12 -> l8 : edgecount^0'=edgecount^post11, i^0'=i^post11, j^0'=j^post11, nodecount^0'=nodecount^post11, source^0'=source^post11, x^0'=x^post11, y^0'=y^post11, (-j^post11+j^0 == 0 /\ -j^0+edgecount^0 <= 0 /\ -1+i^post11-i^0 == 0 /\ -y^post11+y^0 == 0 /\ source^0-source^post11 == 0 /\ -x^post11+x^0 == 0 /\ edgecount^0-edgecount^post11 == 0 /\ -nodecount^post11+nodecount^0 == 0), cost: 1
  26: l12 -> l11 : edgecount^0'=edgecount^post9, i^0'=i^post9, j^0'=j^post9, nodecount^0'=nodecount^post9, source^0'=source^post9, x^0'=x^post9, y^0'=y^post9, (0 == 0 /\ -1-j^post12+j^post9 == 0 /\ x^post12-x^post9 == 0 /\ edgecount^0-edgecount^post12 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ -edgecount^post9+edgecount^post12 == 0 /\ source^0-source^post12 == 0 /\ nodecount^post12-nodecount^post9 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -source^post9+source^post12 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0 /\ -i^post9+i^post12 == 0 /\ -y^post9+y^post12 == 0), cost: 1
  14: l13 -> l14 : edgecount^0'=edgecount^post15, i^0'=i^post15, j^0'=j^post15, nodecount^0'=nodecount^post15, source^0'=source^post15, x^0'=x^post15, y^0'=y^post15, (-i^post15+i^0 == 0 /\ -edgecount^post15+edgecount^0 == 0 /\ source^0-source^post15 == 0 /\ j^0-j^post15 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ -x^post15+x^0 == 0 /\ -y^post15+y^0 == 0), cost: 1
  15: l14 -> l3 : edgecount^0'=edgecount^post16, i^0'=i^post16, j^0'=j^post16, nodecount^0'=nodecount^post16, source^0'=source^post16, x^0'=x^post16, y^0'=y^post16, (y^0-y^post16 == 0 /\ -1+i^post16-i^0 == 0 /\ j^0-j^post16 == 0 /\ -x^post16+x^0 == 0 /\ -nodecount^post16+nodecount^0 == 0 /\ edgecount^0-edgecount^post16 == 0 /\ source^0-source^post16 == 0), cost: 1
  17: l15 -> l13 : edgecount^0'=edgecount^post18, i^0'=i^post18, j^0'=j^post18, nodecount^0'=nodecount^post18, source^0'=source^post18, x^0'=x^post18, y^0'=y^post18, (nodecount^0-nodecount^post18 == 0 /\ 1+source^0-i^0 <= 0 /\ y^0-y^post18 == 0 /\ j^0-j^post18 == 0 /\ source^0-source^post18 == 0 /\ -x^post18+x^0 == 0 /\ edgecount^0-edgecount^post18 == 0 /\ -i^post18+i^0 == 0), cost: 1
  18: l15 -> l13 : edgecount^0'=edgecount^post19, i^0'=i^post19, j^0'=j^post19, nodecount^0'=nodecount^post19, source^0'=source^post19, x^0'=x^post19, y^0'=y^post19, (j^0-j^post19 == 0 /\ source^0-source^post19 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ 1-source^0+i^0 <= 0 /\ -y^post19+y^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ -i^post19+i^0 == 0 /\ x^0-x^post19 == 0), cost: 1
  19: l15 -> l14 : edgecount^0'=edgecount^post20, i^0'=i^post20, j^0'=j^post20, nodecount^0'=nodecount^post20, source^0'=source^post20, x^0'=x^post20, y^0'=y^post20, (source^0-i^0 <= 0 /\ -i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^0 == 0 /\ -source^0+i^0 <= 0 /\ -j^post20+j^0 == 0 /\ x^0-x^post20 == 0 /\ edgecount^0-edgecount^post20 == 0 /\ source^0-source^post20 == 0 /\ -y^post20+y^0 == 0), cost: 1
  25: l17 -> l3 : edgecount^0'=edgecount^post24, i^0'=i^post24, j^0'=j^post24, nodecount^0'=nodecount^post24, source^0'=source^post24, x^0'=x^post24, y^0'=y^post24, (j^0-j^post25 == 0 /\ y^post25-y^post24 == 0 /\ source^0-source^post25 == 0 /\ y^0-y^post25 == 0 /\ -j^post24+j^post25 == 0 /\ -5+nodecount^post24 == 0 /\ source^post24 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ i^post24 == 0 /\ -6+edgecount^post24 == 0 /\ -x^post24+x^post25 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1

	Eliminating location l16 by chaining:

	Applied chaining

	First rule:
	l17 -> l16 : edgecount^0'=edgecount^post25, i^0'=i^post25, j^0'=j^post25, nodecount^0'=nodecount^post25, source^0'=source^post25, x^0'=x^post25, y^0'=y^post25, (j^0-j^post25 == 0 /\ source^0-source^post25 == 0 /\ y^0-y^post25 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1
	Second rule:
	l16 -> l3 : edgecount^0'=edgecount^post24, i^0'=i^post24, j^0'=j^post24, nodecount^0'=nodecount^post24, source^0'=source^post24, x^0'=x^post24, y^0'=y^post24, (y^0-y^post24 == 0 /\ -5+nodecount^post24 == 0 /\ source^post24 == 0 /\ i^post24 == 0 /\ -6+edgecount^post24 == 0 /\ -x^post24+x^0 == 0 /\ j^0-j^post24 == 0), cost: 1
	New rule:
	l17 -> l3 : edgecount^0'=edgecount^post24, i^0'=i^post24, j^0'=j^post24, nodecount^0'=nodecount^post24, source^0'=source^post24, x^0'=x^post24, y^0'=y^post24, (j^0-j^post25 == 0 /\ y^post25-y^post24 == 0 /\ source^0-source^post25 == 0 /\ y^0-y^post25 == 0 /\ -j^post24+j^post25 == 0 /\ -5+nodecount^post24 == 0 /\ source^post24 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ i^post24 == 0 /\ -6+edgecount^post24 == 0 /\ -x^post24+x^post25 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 23 24
	
	Eliminating location l10 by chaining:

	Applied chaining

	First rule:
	l12 -> l10 : edgecount^0'=edgecount^post12, i^0'=i^post12, j^0'=j^post12, nodecount^0'=nodecount^post12, source^0'=source^post12, x^0'=x^post12, y^0'=y^post12, (0 == 0 /\ edgecount^0-edgecount^post12 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post12 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0), cost: 1
	Second rule:
	l10 -> l11 : edgecount^0'=edgecount^post9, i^0'=i^post9, j^0'=j^post9, nodecount^0'=nodecount^post9, source^0'=source^post9, x^0'=x^post9, y^0'=y^post9, (nodecount^0-nodecount^post9 == 0 /\ source^0-source^post9 == 0 /\ -1-j^0+j^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^post9+i^0 == 0 /\ -x^post9+x^0 == 0 /\ -y^post9+y^0 == 0), cost: 1
	New rule:
	l12 -> l11 : edgecount^0'=edgecount^post9, i^0'=i^post9, j^0'=j^post9, nodecount^0'=nodecount^post9, source^0'=source^post9, x^0'=x^post9, y^0'=y^post9, (0 == 0 /\ -1-j^post12+j^post9 == 0 /\ x^post12-x^post9 == 0 /\ edgecount^0-edgecount^post12 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ -edgecount^post9+edgecount^post12 == 0 /\ source^0-source^post12 == 0 /\ nodecount^post12-nodecount^post9 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -source^post9+source^post12 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0 /\ -i^post9+i^post12 == 0 /\ -y^post9+y^post12 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 8 11

Simplified Transitions

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
  27: l0 -> l1 : nodecount^0-i^0 <= 0, cost: 1
  28: l0 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
  47: l2 -> l0 : T, cost: 1
  29: l3 -> l4 : T, cost: 1
  45: l4 -> l8 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  46: l4 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1
  30: l5 -> l6 : i^0'=1+i^0, T, cost: 1
  31: l5 -> l1 : T, cost: 1
  41: l6 -> l7 : T, cost: 1
  32: l7 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1
  33: l7 -> l5 : x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
  34: l8 -> l9 : T, cost: 1
  37: l9 -> l6 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  38: l9 -> l11 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1
  35: l11 -> l12 : T, cost: 1
  36: l12 -> l8 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1
  49: l12 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
  39: l13 -> l14 : T, cost: 1
  40: l14 -> l3 : i^0'=1+i^0, T, cost: 1
  42: l15 -> l13 : 1+source^0-i^0 <= 0, cost: 1
  43: l15 -> l13 : 1-source^0+i^0 <= 0, cost: 1
  44: l15 -> l14 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
  48: l17 -> l3 : edgecount^0'=6, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : edgecount^0'=edgecount^post1, i^0'=i^post1, j^0'=j^post1, nodecount^0'=nodecount^post1, source^0'=source^post1, x^0'=x^post1, y^0'=y^post1, (-nodecount^post1+nodecount^0 == 0 /\ -i^post1+i^0 == 0 /\ nodecount^0-i^0 <= 0 /\ -j^post1+j^0 == 0 /\ x^0-x^post1 == 0 /\ edgecount^0-edgecount^post1 == 0 /\ source^0-source^post1 == 0 /\ -y^post1+y^0 == 0), cost: 1
	New rule:
	l0 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ nodecount^0-i^0 <= 0), cost: 1
	
		propagated equality nodecount^post1 = nodecount^0
		
		propagated equality i^post1 = i^0
		
		propagated equality j^post1 = j^0
		
		propagated equality x^post1 = x^0
		
		propagated equality edgecount^post1 = edgecount^0
		
		propagated equality source^post1 = source^0
		
		propagated equality y^post1 = y^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ nodecount^0-i^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, nodecount^0-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, nodecount^0-i^0 <= 0, cost: 1
	New rule:
	l0 -> l1 : nodecount^0-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l2 : edgecount^0'=edgecount^post2, i^0'=i^post2, j^0'=j^post2, nodecount^0'=nodecount^post2, source^0'=source^post2, x^0'=x^post2, y^0'=y^post2, (-x^post2+x^0 == 0 /\ y^0-y^post2 == 0 /\ source^0-source^post2 == 0 /\ edgecount^0-edgecount^post2 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -nodecount^post2+nodecount^0 == 0 /\ -j^post2+j^0 == 0 /\ -1+i^post2-i^0 == 0), cost: 1
	New rule:
	l0 -> l2 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-nodecount^0+i^0 <= 0), cost: 1
	
		propagated equality x^post2 = x^0
		
		propagated equality y^post2 = y^0
		
		propagated equality source^post2 = source^0
		
		propagated equality edgecount^post2 = edgecount^0
		
		propagated equality nodecount^post2 = nodecount^0
		
		propagated equality j^post2 = j^0
		
		propagated equality i^post2 = 1+i^0
		
	Simplified Guard

	Original rule:
	l0 -> l2 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-nodecount^0+i^0 <= 0), cost: 1
	New rule:
	l0 -> l2 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-nodecount^0+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l2 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-nodecount^0+i^0 <= 0, cost: 1
	New rule:
	l0 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l4 : edgecount^0'=edgecount^post3, i^0'=i^post3, j^0'=j^post3, nodecount^0'=nodecount^post3, source^0'=source^post3, x^0'=x^post3, y^0'=y^post3, (edgecount^0-edgecount^post3 == 0 /\ -i^post3+i^0 == 0 /\ -x^post3+x^0 == 0 /\ y^0-y^post3 == 0 /\ j^0-j^post3 == 0 /\ source^0-source^post3 == 0 /\ -nodecount^post3+nodecount^0 == 0), cost: 1
	New rule:
	l3 -> l4 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality edgecount^post3 = edgecount^0
		
		propagated equality i^post3 = i^0
		
		propagated equality x^post3 = x^0
		
		propagated equality y^post3 = y^0
		
		propagated equality j^post3 = j^0
		
		propagated equality source^post3 = source^0
		
		propagated equality nodecount^post3 = nodecount^0
		
	Simplified Guard

	Original rule:
	l3 -> l4 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l3 -> l4 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l4 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l3 -> l4 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : edgecount^0'=edgecount^post4, i^0'=i^post4, j^0'=j^post4, nodecount^0'=nodecount^post4, source^0'=source^post4, x^0'=x^post4, y^0'=y^post4, (-1+i^post4-i^0 == 0 /\ -source^post4+source^0 == 0 /\ j^0-j^post4 == 0 /\ y^0-y^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ edgecount^0-edgecount^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1
	New rule:
	l5 -> l6 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality i^post4 = 1+i^0
		
		propagated equality source^post4 = source^0
		
		propagated equality j^post4 = j^0
		
		propagated equality y^post4 = y^0
		
		propagated equality nodecount^post4 = nodecount^0
		
		propagated equality edgecount^post4 = edgecount^0
		
		propagated equality x^post4 = x^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l5 -> l6 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l5 -> l6 : i^0'=1+i^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l1 : edgecount^0'=edgecount^post5, i^0'=i^post5, j^0'=j^post5, nodecount^0'=nodecount^post5, source^0'=source^post5, x^0'=x^post5, y^0'=y^post5, (nodecount^0-nodecount^post5 == 0 /\ y^0-y^post5 == 0 /\ source^0-source^post5 == 0 /\ edgecount^0-edgecount^post5 == 0 /\ -i^post5+i^0 == 0 /\ -x^post5+x^0 == 0 /\ j^0-j^post5 == 0), cost: 1
	New rule:
	l5 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality nodecount^post5 = nodecount^0
		
		propagated equality y^post5 = y^0
		
		propagated equality source^post5 = source^0
		
		propagated equality edgecount^post5 = edgecount^0
		
		propagated equality i^post5 = i^0
		
		propagated equality x^post5 = x^0
		
		propagated equality j^post5 = j^0
		
	Simplified Guard

	Original rule:
	l5 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l5 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l1 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l5 -> l1 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l2 : edgecount^0'=edgecount^post6, i^0'=i^post6, j^0'=j^post6, nodecount^0'=nodecount^post6, source^0'=source^post6, x^0'=x^post6, y^0'=y^post6, (source^0-source^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ i^post6 == 0 /\ edgecount^0-i^0 <= 0 /\ -y^post6+y^0 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ x^0-x^post6 == 0), cost: 1
	New rule:
	l7 -> l2 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ edgecount^0-i^0 <= 0), cost: 1
	
		propagated equality source^post6 = source^0
		
		propagated equality j^post6 = j^0
		
		propagated equality edgecount^post6 = edgecount^0
		
		propagated equality i^post6 = 0
		
		propagated equality y^post6 = y^0
		
		propagated equality nodecount^post6 = nodecount^0
		
		propagated equality x^post6 = x^0
		
	Simplified Guard

	Original rule:
	l7 -> l2 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ edgecount^0-i^0 <= 0), cost: 1
	New rule:
	l7 -> l2 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, edgecount^0-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l2 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, edgecount^0-i^0 <= 0, cost: 1
	New rule:
	l7 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l5 : edgecount^0'=edgecount^post7, i^0'=i^post7, j^0'=j^post7, nodecount^0'=nodecount^post7, source^0'=source^post7, x^0'=x^post7, y^0'=y^post7, (0 == 0 /\ -i^post7+i^0 == 0 /\ source^0-source^post7 == 0 /\ -nodecount^post7+nodecount^0 == 0 /\ -j^post7+j^0 == 0 /\ edgecount^0-edgecount^post7 == 0 /\ 1-edgecount^0+i^0 <= 0), cost: 1
	New rule:
	l7 -> l5 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post7, y^0'=y^post7, (0 == 0 /\ 1-edgecount^0+i^0 <= 0), cost: 1
	
		propagated equality i^post7 = i^0
		
		propagated equality source^post7 = source^0
		
		propagated equality nodecount^post7 = nodecount^0
		
		propagated equality j^post7 = j^0
		
		propagated equality edgecount^post7 = edgecount^0
		
	Simplified Guard

	Original rule:
	l7 -> l5 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post7, y^0'=y^post7, (0 == 0 /\ 1-edgecount^0+i^0 <= 0), cost: 1
	New rule:
	l7 -> l5 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l5 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
	New rule:
	l7 -> l5 : x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l9 : edgecount^0'=edgecount^post8, i^0'=i^post8, j^0'=j^post8, nodecount^0'=nodecount^post8, source^0'=source^post8, x^0'=x^post8, y^0'=y^post8, (-i^post8+i^0 == 0 /\ -x^post8+x^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ edgecount^0-edgecount^post8 == 0 /\ y^0-y^post8 == 0 /\ j^0-j^post8 == 0 /\ -source^post8+source^0 == 0), cost: 1
	New rule:
	l8 -> l9 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality i^post8 = i^0
		
		propagated equality x^post8 = x^0
		
		propagated equality nodecount^post8 = nodecount^0
		
		propagated equality edgecount^post8 = edgecount^0
		
		propagated equality y^post8 = y^0
		
		propagated equality j^post8 = j^0
		
		propagated equality source^post8 = source^0
		
	Simplified Guard

	Original rule:
	l8 -> l9 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l8 -> l9 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l9 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l8 -> l9 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l11 -> l12 : edgecount^0'=edgecount^post10, i^0'=i^post10, j^0'=j^post10, nodecount^0'=nodecount^post10, source^0'=source^post10, x^0'=x^post10, y^0'=y^post10, (-i^post10+i^0 == 0 /\ -y^post10+y^0 == 0 /\ j^0-j^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ x^0-x^post10 == 0 /\ source^0-source^post10 == 0 /\ edgecount^0-edgecount^post10 == 0), cost: 1
	New rule:
	l11 -> l12 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality i^post10 = i^0
		
		propagated equality y^post10 = y^0
		
		propagated equality j^post10 = j^0
		
		propagated equality nodecount^post10 = nodecount^0
		
		propagated equality x^post10 = x^0
		
		propagated equality source^post10 = source^0
		
		propagated equality edgecount^post10 = edgecount^0
		
	Simplified Guard

	Original rule:
	l11 -> l12 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l11 -> l12 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l11 -> l12 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l11 -> l12 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l8 : edgecount^0'=edgecount^post11, i^0'=i^post11, j^0'=j^post11, nodecount^0'=nodecount^post11, source^0'=source^post11, x^0'=x^post11, y^0'=y^post11, (-j^post11+j^0 == 0 /\ -j^0+edgecount^0 <= 0 /\ -1+i^post11-i^0 == 0 /\ -y^post11+y^0 == 0 /\ source^0-source^post11 == 0 /\ -x^post11+x^0 == 0 /\ edgecount^0-edgecount^post11 == 0 /\ -nodecount^post11+nodecount^0 == 0), cost: 1
	New rule:
	l12 -> l8 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ -j^0+edgecount^0 <= 0), cost: 1
	
		propagated equality j^post11 = j^0
		
		propagated equality i^post11 = 1+i^0
		
		propagated equality y^post11 = y^0
		
		propagated equality source^post11 = source^0
		
		propagated equality x^post11 = x^0
		
		propagated equality edgecount^post11 = edgecount^0
		
		propagated equality nodecount^post11 = nodecount^0
		
	Simplified Guard

	Original rule:
	l12 -> l8 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ -j^0+edgecount^0 <= 0), cost: 1
	New rule:
	l12 -> l8 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, -j^0+edgecount^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l8 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, -j^0+edgecount^0 <= 0, cost: 1
	New rule:
	l12 -> l8 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l6 : edgecount^0'=edgecount^post13, i^0'=i^post13, j^0'=j^post13, nodecount^0'=nodecount^post13, source^0'=source^post13, x^0'=x^post13, y^0'=y^post13, (i^post13 == 0 /\ source^0-source^post13 == 0 /\ j^0-j^post13 == 0 /\ edgecount^0-edgecount^post13 == 0 /\ nodecount^0-i^0 <= 0 /\ -x^post13+x^0 == 0 /\ y^0-y^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0), cost: 1
	New rule:
	l9 -> l6 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ nodecount^0-i^0 <= 0), cost: 1
	
		propagated equality i^post13 = 0
		
		propagated equality source^post13 = source^0
		
		propagated equality j^post13 = j^0
		
		propagated equality edgecount^post13 = edgecount^0
		
		propagated equality x^post13 = x^0
		
		propagated equality y^post13 = y^0
		
		propagated equality nodecount^post13 = nodecount^0
		
	Simplified Guard

	Original rule:
	l9 -> l6 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ nodecount^0-i^0 <= 0), cost: 1
	New rule:
	l9 -> l6 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, nodecount^0-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l6 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, nodecount^0-i^0 <= 0, cost: 1
	New rule:
	l9 -> l6 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l11 : edgecount^0'=edgecount^post14, i^0'=i^post14, j^0'=j^post14, nodecount^0'=nodecount^post14, source^0'=source^post14, x^0'=x^post14, y^0'=y^post14, (nodecount^0-nodecount^post14 == 0 /\ y^0-y^post14 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -i^post14+i^0 == 0 /\ j^post14 == 0 /\ source^0-source^post14 == 0 /\ -x^post14+x^0 == 0 /\ edgecount^0-edgecount^post14 == 0), cost: 1
	New rule:
	l9 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-nodecount^0+i^0 <= 0), cost: 1
	
		propagated equality nodecount^post14 = nodecount^0
		
		propagated equality y^post14 = y^0
		
		propagated equality i^post14 = i^0
		
		propagated equality j^post14 = 0
		
		propagated equality source^post14 = source^0
		
		propagated equality x^post14 = x^0
		
		propagated equality edgecount^post14 = edgecount^0
		
	Simplified Guard

	Original rule:
	l9 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-nodecount^0+i^0 <= 0), cost: 1
	New rule:
	l9 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-nodecount^0+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-nodecount^0+i^0 <= 0, cost: 1
	New rule:
	l9 -> l11 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l13 -> l14 : edgecount^0'=edgecount^post15, i^0'=i^post15, j^0'=j^post15, nodecount^0'=nodecount^post15, source^0'=source^post15, x^0'=x^post15, y^0'=y^post15, (-i^post15+i^0 == 0 /\ -edgecount^post15+edgecount^0 == 0 /\ source^0-source^post15 == 0 /\ j^0-j^post15 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ -x^post15+x^0 == 0 /\ -y^post15+y^0 == 0), cost: 1
	New rule:
	l13 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality i^post15 = i^0
		
		propagated equality edgecount^post15 = edgecount^0
		
		propagated equality source^post15 = source^0
		
		propagated equality j^post15 = j^0
		
		propagated equality nodecount^post15 = nodecount^0
		
		propagated equality x^post15 = x^0
		
		propagated equality y^post15 = y^0
		
	Simplified Guard

	Original rule:
	l13 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l13 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l13 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l13 -> l14 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l14 -> l3 : edgecount^0'=edgecount^post16, i^0'=i^post16, j^0'=j^post16, nodecount^0'=nodecount^post16, source^0'=source^post16, x^0'=x^post16, y^0'=y^post16, (y^0-y^post16 == 0 /\ -1+i^post16-i^0 == 0 /\ j^0-j^post16 == 0 /\ -x^post16+x^0 == 0 /\ -nodecount^post16+nodecount^0 == 0 /\ edgecount^0-edgecount^post16 == 0 /\ source^0-source^post16 == 0), cost: 1
	New rule:
	l14 -> l3 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality y^post16 = y^0
		
		propagated equality i^post16 = 1+i^0
		
		propagated equality j^post16 = j^0
		
		propagated equality x^post16 = x^0
		
		propagated equality nodecount^post16 = nodecount^0
		
		propagated equality edgecount^post16 = edgecount^0
		
		propagated equality source^post16 = source^0
		
	Simplified Guard

	Original rule:
	l14 -> l3 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l14 -> l3 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l14 -> l3 : edgecount^0'=edgecount^0, i^0'=1+i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l14 -> l3 : i^0'=1+i^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l7 : edgecount^0'=edgecount^post17, i^0'=i^post17, j^0'=j^post17, nodecount^0'=nodecount^post17, source^0'=source^post17, x^0'=x^post17, y^0'=y^post17, (-source^post17+source^0 == 0 /\ j^0-j^post17 == 0 /\ -i^post17+i^0 == 0 /\ nodecount^0-nodecount^post17 == 0 /\ y^0-y^post17 == 0 /\ -x^post17+x^0 == 0 /\ edgecount^0-edgecount^post17 == 0), cost: 1
	New rule:
	l6 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality source^post17 = source^0
		
		propagated equality j^post17 = j^0
		
		propagated equality i^post17 = i^0
		
		propagated equality nodecount^post17 = nodecount^0
		
		propagated equality y^post17 = y^0
		
		propagated equality x^post17 = x^0
		
		propagated equality edgecount^post17 = edgecount^0
		
	Simplified Guard

	Original rule:
	l6 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l6 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l6 -> l7 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l13 : edgecount^0'=edgecount^post18, i^0'=i^post18, j^0'=j^post18, nodecount^0'=nodecount^post18, source^0'=source^post18, x^0'=x^post18, y^0'=y^post18, (nodecount^0-nodecount^post18 == 0 /\ 1+source^0-i^0 <= 0 /\ y^0-y^post18 == 0 /\ j^0-j^post18 == 0 /\ source^0-source^post18 == 0 /\ -x^post18+x^0 == 0 /\ edgecount^0-edgecount^post18 == 0 /\ -i^post18+i^0 == 0), cost: 1
	New rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1+source^0-i^0 <= 0), cost: 1
	
		propagated equality nodecount^post18 = nodecount^0
		
		propagated equality y^post18 = y^0
		
		propagated equality j^post18 = j^0
		
		propagated equality source^post18 = source^0
		
		propagated equality x^post18 = x^0
		
		propagated equality edgecount^post18 = edgecount^0
		
		propagated equality i^post18 = i^0
		
	Simplified Guard

	Original rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1+source^0-i^0 <= 0), cost: 1
	New rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1+source^0-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1+source^0-i^0 <= 0, cost: 1
	New rule:
	l15 -> l13 : 1+source^0-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l13 : edgecount^0'=edgecount^post19, i^0'=i^post19, j^0'=j^post19, nodecount^0'=nodecount^post19, source^0'=source^post19, x^0'=x^post19, y^0'=y^post19, (j^0-j^post19 == 0 /\ source^0-source^post19 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ 1-source^0+i^0 <= 0 /\ -y^post19+y^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ -i^post19+i^0 == 0 /\ x^0-x^post19 == 0), cost: 1
	New rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-source^0+i^0 <= 0), cost: 1
	
		propagated equality j^post19 = j^0
		
		propagated equality source^post19 = source^0
		
		propagated equality edgecount^post19 = edgecount^0
		
		propagated equality y^post19 = y^0
		
		propagated equality nodecount^post19 = nodecount^0
		
		propagated equality i^post19 = i^0
		
		propagated equality x^post19 = x^0
		
	Simplified Guard

	Original rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-source^0+i^0 <= 0), cost: 1
	New rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-source^0+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l13 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-source^0+i^0 <= 0, cost: 1
	New rule:
	l15 -> l13 : 1-source^0+i^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l15 -> l14 : edgecount^0'=edgecount^post20, i^0'=i^post20, j^0'=j^post20, nodecount^0'=nodecount^post20, source^0'=source^post20, x^0'=x^post20, y^0'=y^post20, (source^0-i^0 <= 0 /\ -i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^0 == 0 /\ -source^0+i^0 <= 0 /\ -j^post20+j^0 == 0 /\ x^0-x^post20 == 0 /\ edgecount^0-edgecount^post20 == 0 /\ source^0-source^post20 == 0 /\ -y^post20+y^0 == 0), cost: 1
	New rule:
	l15 -> l14 : edgecount^0'=edgecount^post20, i^0'=i^post20, j^0'=j^post20, nodecount^0'=nodecount^post20, source^0'=source^post20, x^0'=x^post20, y^0'=y^post20, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^0 == 0 /\ -source^0+i^0 <= 0 /\ -j^post20+j^0 == 0 /\ x^0-x^post20 == 0 /\ edgecount^0-edgecount^post20 == 0 /\ source^0-source^post20 == 0 /\ -y^post20+y^0 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l14 : edgecount^0'=edgecount^post20, i^0'=i^post20, j^0'=j^post20, nodecount^0'=nodecount^post20, source^0'=source^post20, x^0'=x^post20, y^0'=y^post20, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^0 == 0 /\ -source^0+i^0 <= 0 /\ -j^post20+j^0 == 0 /\ x^0-x^post20 == 0 /\ edgecount^0-edgecount^post20 == 0 /\ source^0-source^post20 == 0 /\ -y^post20+y^0 == 0), cost: 1
	New rule:
	l15 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
	
		propagated equality i^post20 = i^0
		
		propagated equality nodecount^post20 = nodecount^0
		
		propagated equality j^post20 = j^0
		
		propagated equality x^post20 = x^0
		
		propagated equality edgecount^post20 = edgecount^0
		
		propagated equality source^post20 = source^0
		
		propagated equality y^post20 = y^0
		
	Simplified Guard

	Original rule:
	l15 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
	New rule:
	l15 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l15 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
	New rule:
	l15 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l14 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
	New rule:
	l15 -> l14 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l8 : edgecount^0'=edgecount^post21, i^0'=i^post21, j^0'=j^post21, nodecount^0'=nodecount^post21, source^0'=source^post21, x^0'=x^post21, y^0'=y^post21, (-j^post21+j^0 == 0 /\ nodecount^0-i^0 <= 0 /\ edgecount^0-edgecount^post21 == 0 /\ source^0-source^post21 == 0 /\ -x^post21+x^0 == 0 /\ -y^post21+y^0 == 0 /\ i^post21 == 0 /\ -nodecount^post21+nodecount^0 == 0), cost: 1
	New rule:
	l4 -> l8 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ nodecount^0-i^0 <= 0), cost: 1
	
		propagated equality j^post21 = j^0
		
		propagated equality edgecount^post21 = edgecount^0
		
		propagated equality source^post21 = source^0
		
		propagated equality x^post21 = x^0
		
		propagated equality y^post21 = y^0
		
		propagated equality i^post21 = 0
		
		propagated equality nodecount^post21 = nodecount^0
		
	Simplified Guard

	Original rule:
	l4 -> l8 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ nodecount^0-i^0 <= 0), cost: 1
	New rule:
	l4 -> l8 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, nodecount^0-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l8 : edgecount^0'=edgecount^0, i^0'=0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, nodecount^0-i^0 <= 0, cost: 1
	New rule:
	l4 -> l8 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l15 : edgecount^0'=edgecount^post22, i^0'=i^post22, j^0'=j^post22, nodecount^0'=nodecount^post22, source^0'=source^post22, x^0'=x^post22, y^0'=y^post22, (-x^post22+x^0 == 0 /\ y^0-y^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ source^0-source^post22 == 0 /\ 1-nodecount^0+i^0 <= 0 /\ -i^post22+i^0 == 0 /\ edgecount^0-edgecount^post22 == 0 /\ j^0-j^post22 == 0), cost: 1
	New rule:
	l4 -> l15 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-nodecount^0+i^0 <= 0), cost: 1
	
		propagated equality x^post22 = x^0
		
		propagated equality y^post22 = y^0
		
		propagated equality nodecount^post22 = nodecount^0
		
		propagated equality source^post22 = source^0
		
		propagated equality i^post22 = i^0
		
		propagated equality edgecount^post22 = edgecount^0
		
		propagated equality j^post22 = j^0
		
	Simplified Guard

	Original rule:
	l4 -> l15 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-nodecount^0+i^0 <= 0), cost: 1
	New rule:
	l4 -> l15 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-nodecount^0+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l15 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 1-nodecount^0+i^0 <= 0, cost: 1
	New rule:
	l4 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l0 : edgecount^0'=edgecount^post23, i^0'=i^post23, j^0'=j^post23, nodecount^0'=nodecount^post23, source^0'=source^post23, x^0'=x^post23, y^0'=y^post23, (y^0-y^post23 == 0 /\ -x^post23+x^0 == 0 /\ j^0-j^post23 == 0 /\ nodecount^0-nodecount^post23 == 0 /\ -i^post23+i^0 == 0 /\ edgecount^0-edgecount^post23 == 0 /\ -source^post23+source^0 == 0), cost: 1
	New rule:
	l2 -> l0 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality y^post23 = y^0
		
		propagated equality x^post23 = x^0
		
		propagated equality j^post23 = j^0
		
		propagated equality nodecount^post23 = nodecount^0
		
		propagated equality i^post23 = i^0
		
		propagated equality edgecount^post23 = edgecount^0
		
		propagated equality source^post23 = source^0
		
	Simplified Guard

	Original rule:
	l2 -> l0 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l2 -> l0 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l0 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l2 -> l0 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l17 -> l3 : edgecount^0'=edgecount^post24, i^0'=i^post24, j^0'=j^post24, nodecount^0'=nodecount^post24, source^0'=source^post24, x^0'=x^post24, y^0'=y^post24, (j^0-j^post25 == 0 /\ y^post25-y^post24 == 0 /\ source^0-source^post25 == 0 /\ y^0-y^post25 == 0 /\ -j^post24+j^post25 == 0 /\ -5+nodecount^post24 == 0 /\ source^post24 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ i^post24 == 0 /\ -6+edgecount^post24 == 0 /\ -x^post24+x^post25 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1
	New rule:
	l17 -> l3 : edgecount^0'=6, i^0'=0, j^0'=j^post25, nodecount^0'=5, source^0'=0, x^0'=x^post25, y^0'=y^post25, (0 == 0 /\ j^0-j^post25 == 0 /\ source^0-source^post25 == 0 /\ y^0-y^post25 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1
	
		propagated equality y^post24 = y^post25
		
		propagated equality j^post24 = j^post25
		
		propagated equality nodecount^post24 = 5
		
		propagated equality source^post24 = 0
		
		propagated equality i^post24 = 0
		
		propagated equality edgecount^post24 = 6
		
		propagated equality x^post24 = x^post25
		
	Propagated Equalities

	Original rule:
	l17 -> l3 : edgecount^0'=6, i^0'=0, j^0'=j^post25, nodecount^0'=5, source^0'=0, x^0'=x^post25, y^0'=y^post25, (0 == 0 /\ j^0-j^post25 == 0 /\ source^0-source^post25 == 0 /\ y^0-y^post25 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1
	New rule:
	l17 -> l3 : edgecount^0'=6, i^0'=0, j^0'=j^0, nodecount^0'=5, source^0'=0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	
		propagated equality j^post25 = j^0
		
		propagated equality source^post25 = source^0
		
		propagated equality y^post25 = y^0
		
		propagated equality edgecount^post25 = edgecount^0
		
		propagated equality x^post25 = x^0
		
		propagated equality nodecount^post25 = nodecount^0
		
		propagated equality i^post25 = i^0
		
	Simplified Guard

	Original rule:
	l17 -> l3 : edgecount^0'=6, i^0'=0, j^0'=j^0, nodecount^0'=5, source^0'=0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1
	New rule:
	l17 -> l3 : edgecount^0'=6, i^0'=0, j^0'=j^0, nodecount^0'=5, source^0'=0, x^0'=x^0, y^0'=y^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l17 -> l3 : edgecount^0'=6, i^0'=0, j^0'=j^0, nodecount^0'=5, source^0'=0, x^0'=x^0, y^0'=y^0, T, cost: 1
	New rule:
	l17 -> l3 : edgecount^0'=6, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l11 : edgecount^0'=edgecount^post9, i^0'=i^post9, j^0'=j^post9, nodecount^0'=nodecount^post9, source^0'=source^post9, x^0'=x^post9, y^0'=y^post9, (0 == 0 /\ -1-j^post12+j^post9 == 0 /\ x^post12-x^post9 == 0 /\ edgecount^0-edgecount^post12 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ -edgecount^post9+edgecount^post12 == 0 /\ source^0-source^post12 == 0 /\ nodecount^post12-nodecount^post9 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -source^post9+source^post12 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0 /\ -i^post9+i^post12 == 0 /\ -y^post9+y^post12 == 0), cost: 1
	New rule:
	l12 -> l11 : edgecount^0'=edgecount^post12, i^0'=i^post12, j^0'=1+j^post12, nodecount^0'=nodecount^post12, source^0'=source^post12, x^0'=x^post12, y^0'=y^post12, (0 == 0 /\ edgecount^0-edgecount^post12 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post12 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0), cost: 1
	
		propagated equality j^post9 = 1+j^post12
		
		propagated equality x^post9 = x^post12
		
		propagated equality edgecount^post9 = edgecount^post12
		
		propagated equality nodecount^post9 = nodecount^post12
		
		propagated equality source^post9 = source^post12
		
		propagated equality i^post9 = i^post12
		
		propagated equality y^post9 = y^post12
		
	Propagated Equalities

	Original rule:
	l12 -> l11 : edgecount^0'=edgecount^post12, i^0'=i^post12, j^0'=1+j^post12, nodecount^0'=nodecount^post12, source^0'=source^post12, x^0'=x^post12, y^0'=y^post12, (0 == 0 /\ edgecount^0-edgecount^post12 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post12 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0), cost: 1
	New rule:
	l12 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post12, y^0'=y^post12, (0 == 0 /\ 1+j^0-edgecount^0 <= 0), cost: 1
	
		propagated equality edgecount^post12 = edgecount^0
		
		propagated equality source^post12 = source^0
		
		propagated equality nodecount^post12 = nodecount^0
		
		propagated equality i^post12 = i^0
		
		propagated equality j^post12 = j^0
		
	Simplified Guard

	Original rule:
	l12 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post12, y^0'=y^post12, (0 == 0 /\ 1+j^0-edgecount^0 <= 0), cost: 1
	New rule:
	l12 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l11 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
	New rule:
	l12 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1

Step with 48

	Trace

	48[T]
	
	Blocked

	[{}, {}]

Step with 29

	Trace

	48[T], 29[T]
	
	Blocked

	[{}, {}, {}]

Step with 46

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}]

Step with 44

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}]

Step with 40

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 29

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 46

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 42

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {}, {}, {44[T]}, {}]

Step with 39

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)], 39[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {}, {}, {44[T]}, {}, {}]

Accelerate

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
  27: l0 -> l1 : nodecount^0-i^0 <= 0, cost: 1
  28: l0 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
  47: l2 -> l0 : T, cost: 1
  29: l3 -> l4 : T, cost: 1
  45: l4 -> l8 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  46: l4 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1
  30: l5 -> l6 : i^0'=1+i^0, T, cost: 1
  31: l5 -> l1 : T, cost: 1
  41: l6 -> l7 : T, cost: 1
  32: l7 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1
  33: l7 -> l5 : x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
  34: l8 -> l9 : T, cost: 1
  37: l9 -> l6 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  38: l9 -> l11 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1
  35: l11 -> l12 : T, cost: 1
  36: l12 -> l8 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1
  49: l12 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
  39: l13 -> l14 : T, cost: 1
  40: l14 -> l3 : i^0'=1+i^0, T, cost: 1
  50: l14 -> l14 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1
  42: l15 -> l13 : 1+source^0-i^0 <= 0, cost: 1
  43: l15 -> l13 : 1-source^0+i^0 <= 0, cost: 1
  44: l15 -> l14 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
  48: l17 -> l3 : edgecount^0'=6, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l14 -> l14 : i^0'=1+i^0, (source^0-i^0 <= 0 /\ 2-nodecount^0+i^0 <= 0), cost: 1
	New rule:
	l14 -> l14 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1

		-2+nodecount^0-i^0 >= 0 [0]: montonic decrease yields -1-n+nodecount^0-i^0 >= 0
		
		-2+nodecount^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -2+nodecount^0-i^0 >= 0)
		
		-source^0+i^0 >= 0 [0]: monotonic increase yields -source^0+i^0 >= 0
		
		Replacement map: {-2+nodecount^0-i^0 >= 0 -> -1-n+nodecount^0-i^0 >= 0, -source^0+i^0 >= 0 -> -source^0+i^0 >= 0}

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}]

Step with 40

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 29

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 46

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 42

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {}, {}, {}]

Step with 39

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)], 39[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {}, {}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {}, {}, {39[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {}, {42[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}]

Step with 45

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}]

Step with 34

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {}]

Step with 38

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {36[T]}, {}]

Accelerate

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
  27: l0 -> l1 : nodecount^0-i^0 <= 0, cost: 1
  28: l0 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
  47: l2 -> l0 : T, cost: 1
  29: l3 -> l4 : T, cost: 1
  45: l4 -> l8 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  46: l4 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1
  30: l5 -> l6 : i^0'=1+i^0, T, cost: 1
  31: l5 -> l1 : T, cost: 1
  41: l6 -> l7 : T, cost: 1
  32: l7 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1
  33: l7 -> l5 : x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
  34: l8 -> l9 : T, cost: 1
  37: l9 -> l6 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  38: l9 -> l11 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1
  35: l11 -> l12 : T, cost: 1
  51: l11 -> l11 : j^0'=j^0+n2, x^0'=x^post12, y^0'=y^post12, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1
  36: l12 -> l8 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1
  49: l12 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
  39: l13 -> l14 : T, cost: 1
  40: l14 -> l3 : i^0'=1+i^0, T, cost: 1
  50: l14 -> l14 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1
  42: l15 -> l13 : 1+source^0-i^0 <= 0, cost: 1
  43: l15 -> l13 : 1-source^0+i^0 <= 0, cost: 1
  44: l15 -> l14 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
  48: l17 -> l3 : edgecount^0'=6, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l11 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
	New rule:
	l11 -> l11 : j^0'=j^0+n2, x^0'=x^post12, y^0'=y^post12, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1

		-1-j^0+edgecount^0 >= 0 [0]: montonic decrease yields -j^0-n2+edgecount^0 >= 0
		
		-1-j^0+edgecount^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-j^0+edgecount^0 >= 0)
		
		Replacement map: {-1-j^0+edgecount^0 >= 0 -> -j^0-n2+edgecount^0 >= 0}

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {51[T]}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {51[T]}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {51[T]}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {51[T]}, {49[T]}]

Step with 36

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 36[(-j^0+edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {51[T]}, {49[T]}, {}]

Accelerate

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
  27: l0 -> l1 : nodecount^0-i^0 <= 0, cost: 1
  28: l0 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
  47: l2 -> l0 : T, cost: 1
  29: l3 -> l4 : T, cost: 1
  45: l4 -> l8 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  46: l4 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1
  30: l5 -> l6 : i^0'=1+i^0, T, cost: 1
  31: l5 -> l1 : T, cost: 1
  41: l6 -> l7 : T, cost: 1
  32: l7 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1
  33: l7 -> l5 : x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
  34: l8 -> l9 : T, cost: 1
  52: l8 -> l8 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post122, y^0'=y^post122, (-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 1
  37: l9 -> l6 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  38: l9 -> l11 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1
  35: l11 -> l12 : T, cost: 1
  51: l11 -> l11 : j^0'=j^0+n2, x^0'=x^post12, y^0'=y^post12, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1
  36: l12 -> l8 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1
  49: l12 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
  39: l13 -> l14 : T, cost: 1
  40: l14 -> l3 : i^0'=1+i^0, T, cost: 1
  50: l14 -> l14 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1
  42: l15 -> l13 : 1+source^0-i^0 <= 0, cost: 1
  43: l15 -> l13 : 1-source^0+i^0 <= 0, cost: 1
  44: l15 -> l14 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
  48: l17 -> l3 : edgecount^0'=6, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l8 -> l8 : i^0'=1+i^0, j^0'=edgecount^0, x^0'=x^post122, y^0'=y^post122, (1-nodecount^0+i^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 1
	New rule:
	l8 -> l8 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post122, y^0'=y^post122, (-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 1

		-1+edgecount^0 >= 0 [0]: monotonic increase yields -1+edgecount^0 >= 0
		
		-1+nodecount^0-i^0 >= 0 [0]: montonic decrease yields nodecount^0-n3-i^0 >= 0
		
		-1+nodecount^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+nodecount^0-i^0 >= 0)
		
		Replacement map: {-1+edgecount^0 >= 0 -> -1+edgecount^0 >= 0, -1+nodecount^0-i^0 >= 0 -> nodecount^0-n3-i^0 >= 0}

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}]

Step with 34

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}]

Step with 38

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {}, {36[T]}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {}, {36[T], 49[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}]

Step with 51

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}, {51[T]}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}, {51[T]}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}, {51[T]}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}, {51[T]}, {49[T]}]

Step with 36

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 36[(-j^0+edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}, {51[T]}, {49[T]}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}, {51[T]}, {36[T], 49[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T]}, {35[T], 51[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {}, {35[T], 51[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}]

Step with 37

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}, {}]

Step with 41

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}, {}, {}]

Step with 33

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}, {}, {32[T]}, {}]

Step with 31

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)], 31[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}, {}, {32[T]}, {}, {}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}, {}, {32[T]}, {31[T]}]

Step with 30

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)], 30[T]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}, {}, {32[T]}, {31[T]}, {}]

Accelerate

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
  27: l0 -> l1 : nodecount^0-i^0 <= 0, cost: 1
  28: l0 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
  47: l2 -> l0 : T, cost: 1
  29: l3 -> l4 : T, cost: 1
  45: l4 -> l8 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  46: l4 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1
  30: l5 -> l6 : i^0'=1+i^0, T, cost: 1
  31: l5 -> l1 : T, cost: 1
  41: l6 -> l7 : T, cost: 1
  53: l6 -> l6 : i^0'=n4+i^0, x^0'=x^post71, y^0'=y^post71, (-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0), cost: 1
  32: l7 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1
  33: l7 -> l5 : x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
  34: l8 -> l9 : T, cost: 1
  52: l8 -> l8 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post122, y^0'=y^post122, (-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 1
  37: l9 -> l6 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  38: l9 -> l11 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1
  35: l11 -> l12 : T, cost: 1
  51: l11 -> l11 : j^0'=j^0+n2, x^0'=x^post12, y^0'=y^post12, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1
  36: l12 -> l8 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1
  49: l12 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
  39: l13 -> l14 : T, cost: 1
  40: l14 -> l3 : i^0'=1+i^0, T, cost: 1
  50: l14 -> l14 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1
  42: l15 -> l13 : 1+source^0-i^0 <= 0, cost: 1
  43: l15 -> l13 : 1-source^0+i^0 <= 0, cost: 1
  44: l15 -> l14 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
  48: l17 -> l3 : edgecount^0'=6, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l6 -> l6 : i^0'=1+i^0, x^0'=x^post71, y^0'=y^post71, 1-edgecount^0+i^0 <= 0, cost: 1
	New rule:
	l6 -> l6 : i^0'=n4+i^0, x^0'=x^post71, y^0'=y^post71, (-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0), cost: 1

		-1+edgecount^0-i^0 >= 0 [0]: montonic decrease yields -n4+edgecount^0-i^0 >= 0
		
		-1+edgecount^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+edgecount^0-i^0 >= 0)
		
		Replacement map: {-1+edgecount^0-i^0 >= 0 -> -n4+edgecount^0-i^0 >= 0}

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {42[T], 43[T]}, {}, {50[T]}, {}, {46[T]}, {}, {52[T]}, {38[T]}, {}, {53[T]}]

Restart

Step with 48

	Trace

	48[T]
	
	Blocked

	[{}, {}]

Step with 29

	Trace

	48[T], 29[T]
	
	Blocked

	[{}, {}, {}]

Step with 46

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}]

Step with 44

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}]

Step with 40

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}]

Step with 29

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}, {}]

Step with 46

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}, {}, {}]

Step with 42

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}, {}, {44[T]}, {}]

Step with 39

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)], 39[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}, {}, {44[T]}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}, {}, {44[T]}, {39[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}, {}, {42[T], 44[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {}, {46[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 40[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {}, {29[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}]

Step with 50

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}]

Step with 40

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}]

Step with 29

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {}]

Step with 46

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {}, {}]

Step with 42

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {}, {}, {}]

Step with 39

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)], 39[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {}, {}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 42[(1+source^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {}, {}, {39[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {}, {42[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}]

Step with 45

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}]

Step with 34

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {}]

Step with 38

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {}, {49[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}]

Step with 51

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}, {51[T]}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}, {51[T]}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}, {51[T]}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}, {51[T]}, {49[T]}]

Step with 36

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 36[(-j^0+edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}, {51[T]}, {49[T]}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}, {51[T]}, {36[T], 49[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T]}, {35[T], 51[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T]}, {35[T], 51[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {}, {37[T], 38[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}]

Step with 52

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}]

Step with 34

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}]

Step with 38

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {}, {36[T]}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {}, {36[T], 49[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}]

Step with 51

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}, {51[T]}]

Step with 35

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}, {51[T]}, {}]

Step with 49

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 49[(1+j^0-edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}, {51[T]}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}, {51[T]}, {49[T]}]

Step with 36

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T], 36[(-j^0+edgecount^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}, {51[T]}, {49[T]}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 35[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}, {51[T]}, {36[T], 49[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T]}, {35[T], 51[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 38[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {}, {35[T], 51[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}]

Step with 37

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}]

Step with 41

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}, {}]

Step with 33

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}, {32[T]}, {}]

Step with 31

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)], 31[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}, {32[T]}, {}, {}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}, {32[T]}, {31[T]}]

Step with 30

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)], 30[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}, {32[T]}, {31[T]}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}, {32[T]}, {30[T], 31[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 41[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {}, {32[T], 33[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}]

Step with 53

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}]

Step with 41

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {}]

Step with 33

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {}, {}]

Step with 30

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)], 30[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {}, {30[T]}]

Step with 31

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)], 31[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {}, {30[T]}, {}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 33[(1-edgecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {}, {30[T], 31[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}]

Step with 32

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}]

Step with 47

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 47[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {}]

Step with 28

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 47[T], 28[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {27[T]}, {}]

Accelerate

Start location: l17
Program variables: edgecount^0 i^0 j^0 nodecount^0 source^0 x^0 y^0
  27: l0 -> l1 : nodecount^0-i^0 <= 0, cost: 1
  28: l0 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
  47: l2 -> l0 : T, cost: 1
  54: l2 -> l2 : i^0'=n6+i^0, (nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0), cost: 1
  29: l3 -> l4 : T, cost: 1
  45: l4 -> l8 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  46: l4 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1
  30: l5 -> l6 : i^0'=1+i^0, T, cost: 1
  31: l5 -> l1 : T, cost: 1
  41: l6 -> l7 : T, cost: 1
  53: l6 -> l6 : i^0'=n4+i^0, x^0'=x^post71, y^0'=y^post71, (-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0), cost: 1
  32: l7 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1
  33: l7 -> l5 : x^0'=x^post7, y^0'=y^post7, 1-edgecount^0+i^0 <= 0, cost: 1
  34: l8 -> l9 : T, cost: 1
  52: l8 -> l8 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post122, y^0'=y^post122, (-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 1
  37: l9 -> l6 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1
  38: l9 -> l11 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1
  35: l11 -> l12 : T, cost: 1
  51: l11 -> l11 : j^0'=j^0+n2, x^0'=x^post12, y^0'=y^post12, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1
  36: l12 -> l8 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1
  49: l12 -> l11 : j^0'=1+j^0, x^0'=x^post12, y^0'=y^post12, 1+j^0-edgecount^0 <= 0, cost: 1
  39: l13 -> l14 : T, cost: 1
  40: l14 -> l3 : i^0'=1+i^0, T, cost: 1
  50: l14 -> l14 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1
  42: l15 -> l13 : 1+source^0-i^0 <= 0, cost: 1
  43: l15 -> l13 : 1-source^0+i^0 <= 0, cost: 1
  44: l15 -> l14 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1
  48: l17 -> l3 : edgecount^0'=6, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l2 -> l2 : i^0'=1+i^0, 1-nodecount^0+i^0 <= 0, cost: 1
	New rule:
	l2 -> l2 : i^0'=n6+i^0, (nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0), cost: 1

		-1+nodecount^0-i^0 >= 0 [0]: montonic decrease yields nodecount^0-n6-i^0 >= 0
		
		-1+nodecount^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+nodecount^0-i^0 >= 0)
		
		Replacement map: {-1+nodecount^0-i^0 >= 0 -> nodecount^0-n6-i^0 >= 0}

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {54[T]}]

Step with 47

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {54[T]}, {}]

Step with 28

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T], 28[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {54[T]}, {}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {54[T]}, {28[T]}]

Step with 27

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T], 27[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {54[T]}, {28[T]}, {}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {54[T]}, {27[T], 28[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {}, {47[T], 54[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {54[T]}]

Step with 47

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 47[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {54[T]}, {}]

Step with 28

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 47[T], 28[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {54[T]}, {27[T]}, {}]

Covered

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)], 47[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {54[T]}, {27[T], 28[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T], 32[(edgecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {33[T]}, {47[T], 54[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 41[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {53[T]}, {32[T], 33[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T]}, {41[T], 53[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T], 37[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {38[T]}, {41[T], 53[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 34[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {52[T]}, {37[T], 38[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T]}, {34[T], 52[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T], 45[(nodecount^0-i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {46[T]}, {34[T], 52[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T], 29[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {}, {45[T], 46[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)], 40[T]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {50[T]}, {29[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 50[(-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T]}, {40[T], 50[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)], 44[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {}, {40[T], 50[T]}]

Backtrack

	Trace

	48[T], 29[T], 46[(1-nodecount^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {45[T]}, {44[T]}]

Backtrack

	Trace

	48[T], 29[T]
	
	Blocked

	[{}, {}, {45[T], 46[T]}]

Backtrack

	Trace

	48[T]
	
	Blocked

	[{}, {29[T]}]

Backtrack

	Trace

	Blocked

	[{48[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b