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 /\ -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 /\ -1+i^post3-i^0 == 0), cost: 1 3: l3 -> l1 : 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, (-source^post4+source^0 == 0 /\ j^0-j^post4 == 0 /\ y^0-y^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ -i^post4+i^0 == 0 /\ edgecount^0-edgecount^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1 21: l4 -> l5 : 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 /\ -i^post22+i^0 == 0 /\ edgecount^0-edgecount^post22 == 0 /\ j^0-j^post22 == 0), cost: 1 4: l5 -> l2 : 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 /\ i^post5 == 0 /\ source^0-source^post5 == 0 /\ edgecount^0-edgecount^post5 == 0 /\ edgecount^0-i^0 <= 0 /\ -x^post5+x^0 == 0 /\ j^0-j^post5 == 0), cost: 1 5: l5 -> l3 : 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, (0 == 0 /\ source^0-source^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ 1-edgecount^0+i^0 <= 0 /\ -i^post6+i^0 == 0), cost: 1 6: l6 -> l7 : 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, (-i^post7+i^0 == 0 /\ source^0-source^post7 == 0 /\ -nodecount^post7+nodecount^0 == 0 /\ edgecount^0-edgecount^post7 == 0 /\ -x^post7+x^0 == 0 /\ y^0-y^post7 == 0 /\ -1+j^post7-j^0 == 0), cost: 1 20: l7 -> 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 /\ -i^post21+i^0 == 0 /\ edgecount^0-edgecount^post21 == 0 /\ source^0-source^post21 == 0 /\ -x^post21+x^0 == 0 /\ -y^post21+y^0 == 0 /\ -nodecount^post21+nodecount^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, (-x^post8+x^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ -j^0+edgecount^0 <= 0 /\ edgecount^0-edgecount^post8 == 0 /\ -1+i^post8-i^0 == 0 /\ y^0-y^post8 == 0 /\ j^0-j^post8 == 0 /\ -source^post8+source^0 == 0), cost: 1 8: l8 -> l6 : 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 /\ nodecount^0-nodecount^post9 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^post9+i^0 == 0 /\ j^0-j^post9 == 0), cost: 1 19: l9 -> l10 : 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, (-i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^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 9: l10 -> l4 : 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, (nodecount^0-i^0 <= 0 /\ -y^post10+y^0 == 0 /\ j^0-j^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ i^post10 == 0 /\ x^0-x^post10 == 0 /\ source^0-source^post10 == 0 /\ edgecount^0-edgecount^post10 == 0), cost: 1 10: l10 -> l7 : 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 == 0 /\ 1-nodecount^0+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 /\ -i^post11+i^0 == 0), cost: 1 11: l11 -> l12 : 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, (edgecount^0-edgecount^post12 == 0 /\ y^0-y^post12 == 0 /\ source^0-source^post12 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0 /\ -x^post12+x^0 == 0), cost: 1 13: l12 -> l13 : 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 /\ j^0-j^post14 == 0 /\ y^0-y^post14 == 0 /\ source^0-source^post14 == 0 /\ -x^post14+x^0 == 0 /\ edgecount^0-edgecount^post14 == 0 /\ -1+i^post14-i^0 == 0), cost: 1 12: l13 -> l14 : 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, (source^0-source^post13 == 0 /\ j^0-j^post13 == 0 /\ edgecount^0-edgecount^post13 == 0 /\ -x^post13+x^0 == 0 /\ y^0-y^post13 == 0 /\ -i^post13+i^0 == 0 /\ -nodecount^post13+nodecount^0 == 0), cost: 1 17: l14 -> l9 : 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 /\ nodecount^0-i^0 <= 0 /\ y^0-y^post18 == 0 /\ i^post18 == 0 /\ j^0-j^post18 == 0 /\ source^0-source^post18 == 0 /\ -x^post18+x^0 == 0 /\ edgecount^0-edgecount^post18 == 0), cost: 1 18: l14 -> l15 : 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-nodecount^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 14: l15 -> l11 : 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 /\ 1+source^0-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: l15 -> l11 : 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-source^0+i^0 <= 0 /\ j^0-j^post16 == 0 /\ -x^post16+x^0 == 0 /\ -nodecount^post16+nodecount^0 == 0 /\ -i^post16+i^0 == 0 /\ edgecount^0-edgecount^post16 == 0 /\ source^0-source^post16 == 0), cost: 1 16: l15 -> l12 : 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^0-i^0 <= 0 /\ -source^post17+source^0 == 0 /\ -source^0+i^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 23: l16 -> l13 : 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 /\ -x^post24+x^0 == 0 /\ -15+edgecount^post24 == 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 /\ -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 /\ -1+i^post3-i^0 == 0), cost: 1 3: l3 -> l1 : 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, (-source^post4+source^0 == 0 /\ j^0-j^post4 == 0 /\ y^0-y^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ -i^post4+i^0 == 0 /\ edgecount^0-edgecount^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1 21: l4 -> l5 : 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 /\ -i^post22+i^0 == 0 /\ edgecount^0-edgecount^post22 == 0 /\ j^0-j^post22 == 0), cost: 1 4: l5 -> l2 : 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 /\ i^post5 == 0 /\ source^0-source^post5 == 0 /\ edgecount^0-edgecount^post5 == 0 /\ edgecount^0-i^0 <= 0 /\ -x^post5+x^0 == 0 /\ j^0-j^post5 == 0), cost: 1 5: l5 -> l3 : 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, (0 == 0 /\ source^0-source^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ 1-edgecount^0+i^0 <= 0 /\ -i^post6+i^0 == 0), cost: 1 20: l7 -> 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 /\ -i^post21+i^0 == 0 /\ edgecount^0-edgecount^post21 == 0 /\ source^0-source^post21 == 0 /\ -x^post21+x^0 == 0 /\ -y^post21+y^0 == 0 /\ -nodecount^post21+nodecount^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, (-x^post8+x^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ -j^0+edgecount^0 <= 0 /\ edgecount^0-edgecount^post8 == 0 /\ -1+i^post8-i^0 == 0 /\ y^0-y^post8 == 0 /\ j^0-j^post8 == 0 /\ -source^post8+source^0 == 0), cost: 1 26: l8 -> l7 : 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 /\ -x^post7+x^post9 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ y^post9-y^post7 == 0 /\ source^0-source^post9 == 0 /\ i^post9-i^post7 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -nodecount^post7+nodecount^post9 == 0 /\ edgecount^post9-edgecount^post7 == 0 /\ source^post9-source^post7 == 0 /\ -i^post9+i^0 == 0 /\ j^0-j^post9 == 0 /\ -1+j^post7-j^post9 == 0), cost: 1 19: l9 -> l10 : 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, (-i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^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 9: l10 -> l4 : 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, (nodecount^0-i^0 <= 0 /\ -y^post10+y^0 == 0 /\ j^0-j^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ i^post10 == 0 /\ x^0-x^post10 == 0 /\ source^0-source^post10 == 0 /\ edgecount^0-edgecount^post10 == 0), cost: 1 10: l10 -> l7 : 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 == 0 /\ 1-nodecount^0+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 /\ -i^post11+i^0 == 0), cost: 1 11: l11 -> l12 : 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, (edgecount^0-edgecount^post12 == 0 /\ y^0-y^post12 == 0 /\ source^0-source^post12 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0 /\ -x^post12+x^0 == 0), cost: 1 13: l12 -> l13 : 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 /\ j^0-j^post14 == 0 /\ y^0-y^post14 == 0 /\ source^0-source^post14 == 0 /\ -x^post14+x^0 == 0 /\ edgecount^0-edgecount^post14 == 0 /\ -1+i^post14-i^0 == 0), cost: 1 12: l13 -> l14 : 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, (source^0-source^post13 == 0 /\ j^0-j^post13 == 0 /\ edgecount^0-edgecount^post13 == 0 /\ -x^post13+x^0 == 0 /\ y^0-y^post13 == 0 /\ -i^post13+i^0 == 0 /\ -nodecount^post13+nodecount^0 == 0), cost: 1 17: l14 -> l9 : 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 /\ nodecount^0-i^0 <= 0 /\ y^0-y^post18 == 0 /\ i^post18 == 0 /\ j^0-j^post18 == 0 /\ source^0-source^post18 == 0 /\ -x^post18+x^0 == 0 /\ edgecount^0-edgecount^post18 == 0), cost: 1 18: l14 -> l15 : 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-nodecount^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 14: l15 -> l11 : 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 /\ 1+source^0-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: l15 -> l11 : 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-source^0+i^0 <= 0 /\ j^0-j^post16 == 0 /\ -x^post16+x^0 == 0 /\ -nodecount^post16+nodecount^0 == 0 /\ -i^post16+i^0 == 0 /\ edgecount^0-edgecount^post16 == 0 /\ source^0-source^post16 == 0), cost: 1 16: l15 -> l12 : 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^0-i^0 <= 0 /\ -source^post17+source^0 == 0 /\ -source^0+i^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 25: l17 -> l13 : 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 /\ -x^post24+x^post25 == 0 /\ -15+edgecount^post24 == 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 -> l13 : 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 /\ -x^post24+x^0 == 0 /\ -15+edgecount^post24 == 0 /\ j^0-j^post24 == 0), cost: 1 New rule: l17 -> l13 : 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 /\ -x^post24+x^post25 == 0 /\ -15+edgecount^post24 == 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 l6 by chaining: Applied chaining First rule: l8 -> l6 : 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 /\ nodecount^0-nodecount^post9 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^post9+i^0 == 0 /\ j^0-j^post9 == 0), cost: 1 Second rule: l6 -> l7 : 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, (-i^post7+i^0 == 0 /\ source^0-source^post7 == 0 /\ -nodecount^post7+nodecount^0 == 0 /\ edgecount^0-edgecount^post7 == 0 /\ -x^post7+x^0 == 0 /\ y^0-y^post7 == 0 /\ -1+j^post7-j^0 == 0), cost: 1 New rule: l8 -> l7 : 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 /\ -x^post7+x^post9 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ y^post9-y^post7 == 0 /\ source^0-source^post9 == 0 /\ i^post9-i^post7 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -nodecount^post7+nodecount^post9 == 0 /\ edgecount^post9-edgecount^post7 == 0 /\ source^post9-source^post7 == 0 /\ -i^post9+i^0 == 0 /\ j^0-j^post9 == 0 /\ -1+j^post7-j^post9 == 0), cost: 1 Applied deletion Removed the following rules: 6 8 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 : i^0'=1+i^0, T, cost: 1 30: l3 -> l1 : T, cost: 1 46: l4 -> l5 : T, cost: 1 31: l5 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1 32: l5 -> l3 : x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 45: l7 -> l8 : T, cost: 1 33: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 49: l8 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 44: l9 -> l10 : T, cost: 1 34: l10 -> l4 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 35: l10 -> l7 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1 36: l11 -> l12 : T, cost: 1 38: l12 -> l13 : i^0'=1+i^0, T, cost: 1 37: l13 -> l14 : T, cost: 1 42: l14 -> l9 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 43: l14 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1 39: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 40: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 41: l15 -> l12 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 48: l17 -> l13 : edgecount^0'=15, 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 /\ -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 /\ -1+i^post3-i^0 == 0), cost: 1 New rule: l3 -> l4 : 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 edgecount^post3 = edgecount^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 propagated equality i^post3 = 1+i^0 Simplified Guard Original rule: l3 -> l4 : 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: l3 -> l4 : 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: l3 -> l4 : 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: l3 -> l4 : i^0'=1+i^0, T, cost: 1 Propagated Equalities Original rule: l3 -> l1 : 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, (-source^post4+source^0 == 0 /\ j^0-j^post4 == 0 /\ y^0-y^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ -i^post4+i^0 == 0 /\ edgecount^0-edgecount^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1 New rule: l3 -> 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 source^post4 = source^0 propagated equality j^post4 = j^0 propagated equality y^post4 = y^0 propagated equality nodecount^post4 = nodecount^0 propagated equality i^post4 = i^0 propagated equality edgecount^post4 = edgecount^0 propagated equality x^post4 = x^0 Simplified Guard Original rule: l3 -> 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: l3 -> 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: l3 -> 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: l3 -> l1 : T, cost: 1 Propagated Equalities Original rule: l5 -> l2 : 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 /\ i^post5 == 0 /\ source^0-source^post5 == 0 /\ edgecount^0-edgecount^post5 == 0 /\ edgecount^0-i^0 <= 0 /\ -x^post5+x^0 == 0 /\ j^0-j^post5 == 0), cost: 1 New rule: l5 -> 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 nodecount^post5 = nodecount^0 propagated equality y^post5 = y^0 propagated equality i^post5 = 0 propagated equality source^post5 = source^0 propagated equality edgecount^post5 = edgecount^0 propagated equality x^post5 = x^0 propagated equality j^post5 = j^0 Simplified Guard Original rule: l5 -> 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: l5 -> 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: l5 -> 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: l5 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l3 : 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, (0 == 0 /\ source^0-source^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ 1-edgecount^0+i^0 <= 0 /\ -i^post6+i^0 == 0), cost: 1 New rule: l5 -> l3 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post6, y^0'=y^post6, (0 == 0 /\ 1-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 nodecount^post6 = nodecount^0 propagated equality i^post6 = i^0 Simplified Guard Original rule: l5 -> l3 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post6, y^0'=y^post6, (0 == 0 /\ 1-edgecount^0+i^0 <= 0), cost: 1 New rule: l5 -> l3 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l3 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 New rule: l5 -> l3 : x^0'=x^post6, y^0'=y^post6, 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, (-x^post8+x^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ -j^0+edgecount^0 <= 0 /\ edgecount^0-edgecount^post8 == 0 /\ -1+i^post8-i^0 == 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'=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 x^post8 = x^0 propagated equality nodecount^post8 = nodecount^0 propagated equality edgecount^post8 = edgecount^0 propagated equality i^post8 = 1+i^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'=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: l8 -> l9 : 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: l8 -> l9 : 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: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l4 : 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, (nodecount^0-i^0 <= 0 /\ -y^post10+y^0 == 0 /\ j^0-j^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ i^post10 == 0 /\ x^0-x^post10 == 0 /\ source^0-source^post10 == 0 /\ edgecount^0-edgecount^post10 == 0), cost: 1 New rule: l10 -> l4 : 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 y^post10 = y^0 propagated equality j^post10 = j^0 propagated equality nodecount^post10 = nodecount^0 propagated equality i^post10 = 0 propagated equality x^post10 = x^0 propagated equality source^post10 = source^0 propagated equality edgecount^post10 = edgecount^0 Simplified Guard Original rule: l10 -> l4 : 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: l10 -> l4 : 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: l10 -> l4 : 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: l10 -> l4 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l7 : 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 == 0 /\ 1-nodecount^0+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 /\ -i^post11+i^0 == 0), cost: 1 New rule: l10 -> l7 : 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 j^post11 = 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 propagated equality i^post11 = i^0 Simplified Guard Original rule: l10 -> l7 : 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: l10 -> l7 : 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: l10 -> l7 : 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: l10 -> l7 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l12 : 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, (edgecount^0-edgecount^post12 == 0 /\ y^0-y^post12 == 0 /\ source^0-source^post12 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ -i^post12+i^0 == 0 /\ -j^post12+j^0 == 0 /\ -x^post12+x^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, 0 == 0, cost: 1 propagated equality edgecount^post12 = edgecount^0 propagated equality y^post12 = y^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 propagated equality x^post12 = x^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: l13 -> l14 : 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, (source^0-source^post13 == 0 /\ j^0-j^post13 == 0 /\ edgecount^0-edgecount^post13 == 0 /\ -x^post13+x^0 == 0 /\ y^0-y^post13 == 0 /\ -i^post13+i^0 == 0 /\ -nodecount^post13+nodecount^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 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 i^post13 = i^0 propagated equality nodecount^post13 = nodecount^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: l12 -> l13 : 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 /\ j^0-j^post14 == 0 /\ y^0-y^post14 == 0 /\ source^0-source^post14 == 0 /\ -x^post14+x^0 == 0 /\ edgecount^0-edgecount^post14 == 0 /\ -1+i^post14-i^0 == 0), cost: 1 New rule: l12 -> l13 : 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 nodecount^post14 = nodecount^0 propagated equality j^post14 = j^0 propagated equality y^post14 = y^0 propagated equality source^post14 = source^0 propagated equality x^post14 = x^0 propagated equality edgecount^post14 = edgecount^0 propagated equality i^post14 = 1+i^0 Simplified Guard Original rule: l12 -> l13 : 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: l12 -> l13 : 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: l12 -> l13 : 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: l12 -> l13 : i^0'=1+i^0, T, cost: 1 Propagated Equalities Original rule: l15 -> l11 : 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 /\ 1+source^0-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: l15 -> l11 : 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 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: l15 -> l11 : 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 -> l11 : 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 -> l11 : 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 -> l11 : 1+source^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l15 -> l11 : 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-source^0+i^0 <= 0 /\ j^0-j^post16 == 0 /\ -x^post16+x^0 == 0 /\ -nodecount^post16+nodecount^0 == 0 /\ -i^post16+i^0 == 0 /\ edgecount^0-edgecount^post16 == 0 /\ source^0-source^post16 == 0), cost: 1 New rule: l15 -> l11 : 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 y^post16 = y^0 propagated equality j^post16 = j^0 propagated equality x^post16 = x^0 propagated equality nodecount^post16 = nodecount^0 propagated equality i^post16 = i^0 propagated equality edgecount^post16 = edgecount^0 propagated equality source^post16 = source^0 Simplified Guard Original rule: l15 -> l11 : 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 -> l11 : 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 -> l11 : 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 -> l11 : 1-source^0+i^0 <= 0, cost: 1 made implied equalities explicit Original rule: l15 -> l12 : 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^0-i^0 <= 0 /\ -source^post17+source^0 == 0 /\ -source^0+i^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: l15 -> l12 : 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^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^post17+source^0 == 0 /\ -source^0+i^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 Propagated Equalities Original rule: l15 -> l12 : 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^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^post17+source^0 == 0 /\ -source^0+i^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: l15 -> 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 /\ source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^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: l15 -> 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 /\ source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 New rule: l15 -> 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, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 made implied equalities explicit Original rule: l15 -> 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, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 New rule: l15 -> 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, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l15 -> 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, (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 New rule: l15 -> l12 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 Propagated Equalities Original rule: l14 -> l9 : 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 /\ nodecount^0-i^0 <= 0 /\ y^0-y^post18 == 0 /\ i^post18 == 0 /\ j^0-j^post18 == 0 /\ source^0-source^post18 == 0 /\ -x^post18+x^0 == 0 /\ edgecount^0-edgecount^post18 == 0), cost: 1 New rule: l14 -> l9 : 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 nodecount^post18 = nodecount^0 propagated equality y^post18 = y^0 propagated equality i^post18 = 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 Simplified Guard Original rule: l14 -> l9 : 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: l14 -> l9 : 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: l14 -> l9 : 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: l14 -> l9 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l14 -> l15 : 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-nodecount^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: l14 -> 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 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: l14 -> 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: l14 -> 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: l14 -> 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: l14 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l10 : 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, (-i^post20+i^0 == 0 /\ -nodecount^post20+nodecount^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: l9 -> l10 : 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^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: l9 -> l10 : 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: l9 -> l10 : 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: l9 -> l10 : 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: l9 -> l10 : T, cost: 1 Propagated Equalities Original rule: l7 -> 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 /\ -i^post21+i^0 == 0 /\ edgecount^0-edgecount^post21 == 0 /\ source^0-source^post21 == 0 /\ -x^post21+x^0 == 0 /\ -y^post21+y^0 == 0 /\ -nodecount^post21+nodecount^0 == 0), cost: 1 New rule: l7 -> l8 : 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 j^post21 = j^0 propagated equality i^post21 = i^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 nodecount^post21 = nodecount^0 Simplified Guard Original rule: l7 -> l8 : 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: l7 -> l8 : 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: l7 -> l8 : 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: l7 -> l8 : T, cost: 1 Propagated Equalities Original rule: l4 -> l5 : 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 /\ -i^post22+i^0 == 0 /\ edgecount^0-edgecount^post22 == 0 /\ j^0-j^post22 == 0), cost: 1 New rule: l4 -> l5 : 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 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 -> l5 : 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: l4 -> l5 : 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: l4 -> l5 : 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: l4 -> l5 : T, 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 -> l13 : 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 /\ -x^post24+x^post25 == 0 /\ -15+edgecount^post24 == 0 /\ x^0-x^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ -i^post25+i^0 == 0), cost: 1 New rule: l17 -> l13 : edgecount^0'=15, 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 x^post24 = x^post25 propagated equality edgecount^post24 = 15 Propagated Equalities Original rule: l17 -> l13 : edgecount^0'=15, 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 -> l13 : edgecount^0'=15, 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 -> l13 : edgecount^0'=15, 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 -> l13 : edgecount^0'=15, 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 -> l13 : edgecount^0'=15, 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 -> l13 : edgecount^0'=15, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1 Propagated Equalities Original rule: l8 -> l7 : 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 /\ -x^post7+x^post9 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ y^post9-y^post7 == 0 /\ source^0-source^post9 == 0 /\ i^post9-i^post7 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -nodecount^post7+nodecount^post9 == 0 /\ edgecount^post9-edgecount^post7 == 0 /\ source^post9-source^post7 == 0 /\ -i^post9+i^0 == 0 /\ j^0-j^post9 == 0 /\ -1+j^post7-j^post9 == 0), cost: 1 New rule: l8 -> l7 : edgecount^0'=edgecount^post9, i^0'=i^post9, j^0'=1+j^post9, nodecount^0'=nodecount^post9, source^0'=source^post9, x^0'=x^post9, y^0'=y^post9, (0 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^post9+i^0 == 0 /\ j^0-j^post9 == 0), cost: 1 propagated equality x^post7 = x^post9 propagated equality y^post7 = y^post9 propagated equality i^post7 = i^post9 propagated equality nodecount^post7 = nodecount^post9 propagated equality edgecount^post7 = edgecount^post9 propagated equality source^post7 = source^post9 propagated equality j^post7 = 1+j^post9 Propagated Equalities Original rule: l8 -> l7 : edgecount^0'=edgecount^post9, i^0'=i^post9, j^0'=1+j^post9, nodecount^0'=nodecount^post9, source^0'=source^post9, x^0'=x^post9, y^0'=y^post9, (0 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ source^0-source^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^post9+i^0 == 0 /\ j^0-j^post9 == 0), cost: 1 New rule: l8 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post9, y^0'=y^post9, (0 == 0 /\ 1+j^0-edgecount^0 <= 0), cost: 1 propagated equality nodecount^post9 = nodecount^0 propagated equality source^post9 = source^0 propagated equality edgecount^post9 = edgecount^0 propagated equality i^post9 = i^0 propagated equality j^post9 = j^0 Simplified Guard Original rule: l8 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post9, y^0'=y^post9, (0 == 0 /\ 1+j^0-edgecount^0 <= 0), cost: 1 New rule: l8 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : edgecount^0'=edgecount^0, i^0'=i^0, j^0'=1+j^0, nodecount^0'=nodecount^0, source^0'=source^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 New rule: l8 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 Step with 48 Trace 48[T] Blocked [{}, {}] Step with 37 Trace 48[T], 37[T] Blocked [{}, {}, {}] Step with 43 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}] Step with 41 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}] Step with 38 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 37 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 43 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 39 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {}, {}, {41[T]}, {}] Step with 36 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)], 36[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {}, {}, {41[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 : i^0'=1+i^0, T, cost: 1 30: l3 -> l1 : T, cost: 1 46: l4 -> l5 : T, cost: 1 31: l5 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1 32: l5 -> l3 : x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 45: l7 -> l8 : T, cost: 1 33: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 49: l8 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 44: l9 -> l10 : T, cost: 1 34: l10 -> l4 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 35: l10 -> l7 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1 36: l11 -> l12 : T, cost: 1 38: l12 -> l13 : i^0'=1+i^0, T, cost: 1 50: l12 -> l12 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1 37: l13 -> l14 : T, cost: 1 42: l14 -> l9 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 43: l14 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1 39: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 40: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 41: l15 -> l12 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 48: l17 -> l13 : edgecount^0'=15, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1 Loop Acceleration Original rule: l12 -> l12 : i^0'=1+i^0, (source^0-i^0 <= 0 /\ 2-nodecount^0+i^0 <= 0), cost: 1 New rule: l12 -> l12 : 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], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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 [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}] Step with 38 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 37 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 43 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 39 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {}, {}, {}] Step with 36 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)], 36[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {}, {}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {}, {}, {36[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {}, {39[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}] Step with 42 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}] Step with 44 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {}] Step with 35 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {33[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 : i^0'=1+i^0, T, cost: 1 30: l3 -> l1 : T, cost: 1 46: l4 -> l5 : T, cost: 1 31: l5 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1 32: l5 -> l3 : x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 45: l7 -> l8 : T, cost: 1 51: l7 -> l7 : j^0'=j^0+n2, x^0'=x^post9, y^0'=y^post9, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1 33: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 49: l8 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 44: l9 -> l10 : T, cost: 1 34: l10 -> l4 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 35: l10 -> l7 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1 36: l11 -> l12 : T, cost: 1 38: l12 -> l13 : i^0'=1+i^0, T, cost: 1 50: l12 -> l12 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1 37: l13 -> l14 : T, cost: 1 42: l14 -> l9 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 43: l14 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1 39: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 40: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 41: l15 -> l12 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 48: l17 -> l13 : edgecount^0'=15, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1 Loop Acceleration Original rule: l7 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 New rule: l7 -> l7 : j^0'=j^0+n2, x^0'=x^post9, y^0'=y^post9, (-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], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {51[T]}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {51[T]}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {51[T]}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {51[T]}, {49[T]}] Step with 33 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 33[(-j^0+edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {34[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 : i^0'=1+i^0, T, cost: 1 30: l3 -> l1 : T, cost: 1 46: l4 -> l5 : T, cost: 1 31: l5 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1 32: l5 -> l3 : x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 45: l7 -> l8 : T, cost: 1 51: l7 -> l7 : j^0'=j^0+n2, x^0'=x^post9, y^0'=y^post9, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1 33: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 49: l8 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 44: l9 -> l10 : T, cost: 1 52: l9 -> l9 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post92, y^0'=y^post92, (-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 1 34: l10 -> l4 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 35: l10 -> l7 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1 36: l11 -> l12 : T, cost: 1 38: l12 -> l13 : i^0'=1+i^0, T, cost: 1 50: l12 -> l12 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1 37: l13 -> l14 : T, cost: 1 42: l14 -> l9 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 43: l14 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1 39: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 40: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 41: l15 -> l12 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 48: l17 -> l13 : edgecount^0'=15, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1 Loop Acceleration Original rule: l9 -> l9 : i^0'=1+i^0, j^0'=edgecount^0, x^0'=x^post92, y^0'=y^post92, (1-nodecount^0+i^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 1 New rule: l9 -> l9 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post92, y^0'=y^post92, (-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], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}] Step with 44 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}] Step with 35 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {}, {33[T]}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {}, {33[T], 49[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}] Step with 51 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}, {51[T]}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}, {51[T]}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}, {51[T]}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}, {51[T]}, {49[T]}] Step with 33 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 33[(-j^0+edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}, {51[T]}, {49[T]}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}, {51[T]}, {33[T], 49[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T]}, {45[T], 51[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {}, {45[T], 51[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}] Step with 34 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}, {}] Step with 46 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}, {}, {}] Step with 32 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}, {}, {31[T]}, {}] Step with 30 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)], 30[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}, {}, {31[T]}, {}, {}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}, {}, {31[T]}, {30[T]}] Step with 29 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)], 29[T] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}, {}, {31[T]}, {30[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 : i^0'=1+i^0, T, cost: 1 30: l3 -> l1 : T, cost: 1 46: l4 -> l5 : T, cost: 1 53: l4 -> l4 : i^0'=n4+i^0, x^0'=x^post61, y^0'=y^post61, (-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0), cost: 1 31: l5 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1 32: l5 -> l3 : x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 45: l7 -> l8 : T, cost: 1 51: l7 -> l7 : j^0'=j^0+n2, x^0'=x^post9, y^0'=y^post9, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1 33: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 49: l8 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 44: l9 -> l10 : T, cost: 1 52: l9 -> l9 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post92, y^0'=y^post92, (-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 1 34: l10 -> l4 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 35: l10 -> l7 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1 36: l11 -> l12 : T, cost: 1 38: l12 -> l13 : i^0'=1+i^0, T, cost: 1 50: l12 -> l12 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1 37: l13 -> l14 : T, cost: 1 42: l14 -> l9 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 43: l14 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1 39: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 40: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 41: l15 -> l12 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 48: l17 -> l13 : edgecount^0'=15, i^0'=0, nodecount^0'=5, source^0'=0, T, cost: 1 Loop Acceleration Original rule: l4 -> l4 : i^0'=1+i^0, x^0'=x^post61, y^0'=y^post61, 1-edgecount^0+i^0 <= 0, cost: 1 New rule: l4 -> l4 : i^0'=n4+i^0, x^0'=x^post61, y^0'=y^post61, (-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], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)] Blocked [{}, {}, {42[T]}, {39[T], 40[T]}, {}, {50[T]}, {}, {43[T]}, {}, {52[T]}, {35[T]}, {}, {53[T]}] Restart Step with 48 Trace 48[T] Blocked [{}, {}] Step with 37 Trace 48[T], 37[T] Blocked [{}, {}, {}] Step with 43 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}] Step with 41 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {}] Step with 38 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T] Blocked [{}, {}, {42[T]}, {}, {}, {}] Step with 37 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {}, {}, {}, {}] Step with 43 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {}, {}, {}, {}] Step with 39 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {}, {}, {}, {41[T]}, {}] Step with 36 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)], 36[T] Blocked [{}, {}, {42[T]}, {}, {}, {}, {}, {41[T]}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {}, {}, {}, {41[T]}, {36[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {}, {}, {}, {39[T], 41[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {}, {}, {}, {43[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)], 38[T] Blocked [{}, {}, {42[T]}, {}, {}, {37[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}] Step with 50 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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 [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}] Step with 38 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}] Step with 37 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {}] Step with 43 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {}, {}] Step with 39 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {}, {}, {}] Step with 36 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)], 36[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {}, {}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 39[(1+source^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {}, {}, {36[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {}, {39[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}] Step with 42 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}] Step with 44 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {}] Step with 35 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {}, {49[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}] Step with 51 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}, {51[T]}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}, {51[T]}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}, {51[T]}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}, {51[T]}, {49[T]}] Step with 33 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 33[(-j^0+edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}, {51[T]}, {49[T]}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}, {51[T]}, {33[T], 49[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T]}, {45[T], 51[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T]}, {45[T], 51[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 44[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {}, {34[T], 35[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}] Step with 52 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}] Step with 44 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}] Step with 35 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {}, {33[T]}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {}, {33[T], 49[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}] Step with 51 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}, {51[T]}] Step with 45 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}, {51[T]}, {}] Step with 49 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 49[(1+j^0-edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}, {51[T]}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}, {51[T]}, {49[T]}] Step with 33 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T], 33[(-j^0+edgecount^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}, {51[T]}, {49[T]}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)], 45[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}, {51[T]}, {33[T], 49[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)], 51[(-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T]}, {45[T], 51[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 35[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {}, {45[T], 51[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}] Step with 34 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}] Step with 46 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}, {}] Step with 32 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}, {31[T]}, {}] Step with 30 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)], 30[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}, {31[T]}, {}, {}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}, {31[T]}, {30[T]}] Step with 29 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)], 29[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}, {31[T]}, {30[T]}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}, {31[T]}, {29[T], 30[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 46[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {}, {31[T], 32[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}] Step with 53 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}] Step with 46 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {}] Step with 32 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {}, {}] Step with 29 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)], 29[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {}, {29[T]}] Step with 30 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)], 30[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {}, {29[T]}, {}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 32[(1-edgecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {}, {29[T], 30[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}] Step with 31 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}] Step with 47 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 47[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {}] Step with 28 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 47[T], 28[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[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 : i^0'=1+i^0, T, cost: 1 30: l3 -> l1 : T, cost: 1 46: l4 -> l5 : T, cost: 1 53: l4 -> l4 : i^0'=n4+i^0, x^0'=x^post61, y^0'=y^post61, (-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0), cost: 1 31: l5 -> l2 : i^0'=0, edgecount^0-i^0 <= 0, cost: 1 32: l5 -> l3 : x^0'=x^post6, y^0'=y^post6, 1-edgecount^0+i^0 <= 0, cost: 1 45: l7 -> l8 : T, cost: 1 51: l7 -> l7 : j^0'=j^0+n2, x^0'=x^post9, y^0'=y^post9, (-1+n2 >= 0 /\ -j^0-n2+edgecount^0 >= 0), cost: 1 33: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 49: l8 -> l7 : j^0'=1+j^0, x^0'=x^post9, y^0'=y^post9, 1+j^0-edgecount^0 <= 0, cost: 1 44: l9 -> l10 : T, cost: 1 52: l9 -> l9 : i^0'=n3+i^0, j^0'=edgecount^0, x^0'=x^post92, y^0'=y^post92, (-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 1 34: l10 -> l4 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 35: l10 -> l7 : j^0'=0, 1-nodecount^0+i^0 <= 0, cost: 1 36: l11 -> l12 : T, cost: 1 38: l12 -> l13 : i^0'=1+i^0, T, cost: 1 50: l12 -> l12 : i^0'=n+i^0, (-source^0+i^0 >= 0 /\ -1-n+nodecount^0-i^0 >= 0 /\ -1+n >= 0), cost: 1 37: l13 -> l14 : T, cost: 1 42: l14 -> l9 : i^0'=0, nodecount^0-i^0 <= 0, cost: 1 43: l14 -> l15 : 1-nodecount^0+i^0 <= 0, cost: 1 39: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 40: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 41: l15 -> l12 : (source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0), cost: 1 48: l17 -> l13 : edgecount^0'=15, 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], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {54[T]}] Step with 47 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {54[T]}, {}] Step with 28 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(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 [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {54[T]}, {}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {54[T]}, {28[T]}] Step with 27 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T], 27[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {54[T]}, {28[T]}, {}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)], 47[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {54[T]}, {27[T], 28[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 54[(nodecount^0-n6-i^0 >= 0 /\ -1+n6 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {}, {47[T], 54[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {54[T]}] Step with 47 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 47[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {54[T]}, {}] Step with 28 Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 47[T], 28[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {54[T]}, {27[T]}, {}] Covered Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)], 47[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {54[T]}, {27[T], 28[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T], 31[(edgecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {32[T]}, {47[T], 54[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)], 46[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {53[T]}, {31[T], 32[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)], 53[(-1+n4 >= 0 /\ -n4+edgecount^0-i^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T]}, {46[T], 53[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T], 34[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {35[T]}, {46[T], 53[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)], 44[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {52[T]}, {34[T], 35[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)], 52[(-1+n3 >= 0 /\ nodecount^0-n3-i^0 >= 0 /\ -1+edgecount^0 >= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T]}, {44[T], 52[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T], 42[(nodecount^0-i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {43[T]}, {44[T], 52[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T], 37[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {}, {42[T], 43[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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)], 38[T] Blocked [{}, {}, {42[T]}, {}, {38[T]}, {50[T]}, {37[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(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 [{}, {}, {42[T]}, {}, {38[T]}, {38[T], 50[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)], 41[(source^0-i^0 <= 0 /\ source^0-i^0 == 0 /\ -source^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {}, {38[T], 50[T]}] Backtrack Trace 48[T], 37[T], 43[(1-nodecount^0+i^0 <= 0)] Blocked [{}, {}, {42[T]}, {41[T]}] Backtrack Trace 48[T], 37[T] Blocked [{}, {}, {42[T], 43[T]}] Backtrack Trace 48[T] Blocked [{}, {37[T]}] Backtrack Trace Blocked [{48[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b