NO Initial ITS Start location: l28 Program variables: __lengthofvisited^0 destflag^0 edgecount^0 h^0 i^0 j^0 k^0 k_1^0 min^0 nodecount^0 sourceflag^0 0: l0 -> l1 : __lengthofvisited^0'=__lengthofvisited^post1, destflag^0'=destflag^post1, edgecount^0'=edgecount^post1, h^0'=h^post1, i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, k_1^0'=k_1^post1, min^0'=min^post1, nodecount^0'=nodecount^post1, sourceflag^0'=sourceflag^post1, (__lengthofvisited^0-__lengthofvisited^post1 == 0 /\ nodecount^0-nodecount^post1 == 0 /\ -j^post1+j^0 == 0 /\ -min^post1+min^0 == 0 /\ -destflag^post1+destflag^0 == 0 /\ k^0-k^post1 == 0 /\ -sourceflag^post1+sourceflag^0 == 0 /\ h^0-h^post1 == 0 /\ k_1^0-k_1^post1 == 0 /\ -i^post1+i^0 == 0 /\ -edgecount^post1+edgecount^0 == 0), cost: 1 42: l1 -> l2 : __lengthofvisited^0'=__lengthofvisited^post43, destflag^0'=destflag^post43, edgecount^0'=edgecount^post43, h^0'=h^post43, i^0'=i^post43, j^0'=j^post43, k^0'=k^post43, k_1^0'=k_1^post43, min^0'=min^post43, nodecount^0'=nodecount^post43, sourceflag^0'=sourceflag^post43, (-i^0+nodecount^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post43 == 0 /\ -j^post43+j^0 == 0 /\ i^post43 == 0 /\ -k_1^post43+k_1^0 == 0 /\ -destflag^post43+destflag^0 == 0 /\ nodecount^0-nodecount^post43 == 0 /\ -min^post43+min^0 == 0 /\ k^0-k^post43 == 0 /\ -sourceflag^post43+sourceflag^0 == 0 /\ h^0-h^post43 == 0 /\ -edgecount^post43+edgecount^0 == 0), cost: 1 43: l1 -> l0 : __lengthofvisited^0'=__lengthofvisited^post44, destflag^0'=destflag^post44, edgecount^0'=edgecount^post44, h^0'=h^post44, i^0'=i^post44, j^0'=j^post44, k^0'=k^post44, k_1^0'=k_1^post44, min^0'=min^post44, nodecount^0'=nodecount^post44, sourceflag^0'=sourceflag^post44, (k_1^0-k_1^post44 == 0 /\ -k^post44+k^0 == 0 /\ -1-i^0+i^post44 == 0 /\ -nodecount^post44+nodecount^0 == 0 /\ -sourceflag^post44+sourceflag^0 == 0 /\ destflag^0-destflag^post44 == 0 /\ min^0-min^post44 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ -h^post44+h^0 == 0 /\ j^0-j^post44 == 0 /\ -__lengthofvisited^post44+__lengthofvisited^0 == 0 /\ -edgecount^post44+edgecount^0 == 0), cost: 1 1: l2 -> l3 : __lengthofvisited^0'=__lengthofvisited^post2, destflag^0'=destflag^post2, edgecount^0'=edgecount^post2, h^0'=h^post2, i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, k_1^0'=k_1^post2, min^0'=min^post2, nodecount^0'=nodecount^post2, sourceflag^0'=sourceflag^post2, (i^0-i^post2 == 0 /\ -h^post2+h^0 == 0 /\ -j^post2+j^0 == 0 /\ k_1^0-k_1^post2 == 0 /\ destflag^0-destflag^post2 == 0 /\ -k^post2+k^0 == 0 /\ -__lengthofvisited^post2+__lengthofvisited^0 == 0 /\ -min^post2+min^0 == 0 /\ -sourceflag^post2+sourceflag^0 == 0 /\ -edgecount^post2+edgecount^0 == 0 /\ nodecount^0-nodecount^post2 == 0), cost: 1 39: l3 -> l4 : __lengthofvisited^0'=__lengthofvisited^post40, destflag^0'=destflag^post40, edgecount^0'=edgecount^post40, h^0'=h^post40, i^0'=i^post40, j^0'=j^post40, k^0'=k^post40, k_1^0'=k_1^post40, min^0'=min^post40, nodecount^0'=nodecount^post40, sourceflag^0'=sourceflag^post40, (nodecount^0-nodecount^post40 == 0 /\ i^0-i^post40 == 0 /\ -sourceflag^post40+sourceflag^0 == 0 /\ h^0-h^post40 == 0 /\ -j^post40+j^0 == 0 /\ k^post40 == 0 /\ __lengthofvisited^0-__lengthofvisited^post40 == 0 /\ destflag^0-destflag^post40 == 0 /\ k_1^0-k_1^post40 == 0 /\ -edgecount^post40+edgecount^0 == 0 /\ -1-i^0+nodecount^0 <= 0 /\ -min^post40+min^0 == 0), cost: 1 40: l3 -> l2 : __lengthofvisited^0'=__lengthofvisited^post41, destflag^0'=destflag^post41, edgecount^0'=edgecount^post41, h^0'=h^post41, i^0'=i^post41, j^0'=j^post41, k^0'=k^post41, k_1^0'=k_1^post41, min^0'=min^post41, nodecount^0'=nodecount^post41, sourceflag^0'=sourceflag^post41, (2+i^0-nodecount^0 <= 0 /\ destflag^0-destflag^post41 == 0 /\ -j^post41+j^0 == 0 /\ -h^post41+h^0 == 0 /\ -edgecount^post41+edgecount^0 == 0 /\ -__lengthofvisited^post41+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post41 == 0 /\ -1-i^0+i^post41 == 0 /\ -k^post41+k^0 == 0 /\ -sourceflag^post41+sourceflag^0 == 0 /\ nodecount^0-nodecount^post41 == 0 /\ -min^post41+min^0 == 0), cost: 1 2: l4 -> l5 : __lengthofvisited^0'=__lengthofvisited^post3, destflag^0'=destflag^post3, edgecount^0'=edgecount^post3, h^0'=h^post3, i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, k_1^0'=k_1^post3, min^0'=min^post3, nodecount^0'=nodecount^post3, sourceflag^0'=sourceflag^post3, (i^0-i^post3 == 0 /\ h^0-h^post3 == 0 /\ -j^post3+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post3 == 0 /\ destflag^0-destflag^post3 == 0 /\ k_1^0-k_1^post3 == 0 /\ -edgecount^post3+edgecount^0 == 0 /\ -sourceflag^post3+sourceflag^0 == 0 /\ -min^post3+min^0 == 0 /\ nodecount^0-nodecount^post3 == 0 /\ k^0-k^post3 == 0), cost: 1 36: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^post37, destflag^0'=destflag^post37, edgecount^0'=edgecount^post37, h^0'=h^post37, i^0'=i^post37, j^0'=j^post37, k^0'=k^post37, k_1^0'=k_1^post37, min^0'=min^post37, nodecount^0'=nodecount^post37, sourceflag^0'=sourceflag^post37, (-1+nodecount^0-k^0 <= 0 /\ k^0-k^post37 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ -min^post37+min^0 == 0 /\ k_1^0-k_1^post37 == 0 /\ i^0-i^post37 == 0 /\ 1-nodecount^0+k^0 <= 0 /\ h^0-h^post37 == 0 /\ nodecount^0-nodecount^post37 == 0 /\ -j^post37+j^0 == 0 /\ destflag^0-destflag^post37 == 0), cost: 1 37: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^post38, destflag^0'=destflag^post38, edgecount^0'=edgecount^post38, h^0'=h^post38, i^0'=i^post38, j^0'=j^post38, k^0'=k^post38, k_1^0'=k_1^post38, min^0'=min^post38, nodecount^0'=nodecount^post38, sourceflag^0'=sourceflag^post38, (k^0-k^post38 == 0 /\ -__lengthofvisited^post38+__lengthofvisited^0 == 0 /\ -min^post38+min^0 == 0 /\ -edgecount^post38+edgecount^0 == 0 /\ -sourceflag^post38+sourceflag^0 == 0 /\ i^0-i^post38 == 0 /\ k_1^0-k_1^post38 == 0 /\ -j^post38+j^0 == 0 /\ -h^post38+h^0 == 0 /\ -nodecount^post38+nodecount^0 == 0 /\ nodecount^0-k^0 <= 0 /\ destflag^0-destflag^post38 == 0), cost: 1 38: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^post39, destflag^0'=destflag^post39, edgecount^0'=edgecount^post39, h^0'=h^post39, i^0'=i^post39, j^0'=j^post39, k^0'=k^post39, k_1^0'=k_1^post39, min^0'=min^post39, nodecount^0'=nodecount^post39, sourceflag^0'=sourceflag^post39, (min^0-min^post39 == 0 /\ __lengthofvisited^0-__lengthofvisited^post39 == 0 /\ -sourceflag^post39+sourceflag^0 == 0 /\ -k^post39+k^0 == 0 /\ -edgecount^post39+edgecount^0 == 0 /\ -destflag^post39+destflag^0 == 0 /\ h^0-h^post39 == 0 /\ j^0-j^post39 == 0 /\ -nodecount^post39+nodecount^0 == 0 /\ 2-nodecount^0+k^0 <= 0 /\ k_1^0-k_1^post39 == 0 /\ i^0-i^post39 == 0), cost: 1 3: l6 -> l7 : __lengthofvisited^0'=__lengthofvisited^post4, destflag^0'=destflag^post4, edgecount^0'=edgecount^post4, h^0'=h^post4, i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, k_1^0'=k_1^post4, min^0'=min^post4, nodecount^0'=nodecount^post4, sourceflag^0'=sourceflag^post4, (-edgecount^post4+edgecount^0 == 0 /\ -h^post4+h^0 == 0 /\ -__lengthofvisited^post4+__lengthofvisited^0 == 0 /\ -nodecount^post4+nodecount^0 == 0 /\ min^0-min^post4 == 0 /\ i^0-i^post4 == 0 /\ j^0-j^post4 == 0 /\ destflag^0-destflag^post4 == 0 /\ -1-k_1^0+k_1^post4 == 0 /\ -sourceflag^post4+sourceflag^0 == 0 /\ -k^post4+k^0 == 0), cost: 1 18: l7 -> l18 : __lengthofvisited^0'=__lengthofvisited^post19, destflag^0'=destflag^post19, edgecount^0'=edgecount^post19, h^0'=h^post19, i^0'=i^post19, j^0'=j^post19, k^0'=k^post19, k_1^0'=k_1^post19, min^0'=min^post19, nodecount^0'=nodecount^post19, sourceflag^0'=sourceflag^post19, (min^0-min^post19 == 0 /\ edgecount^0-edgecount^post19 == 0 /\ -__lengthofvisited^post19+__lengthofvisited^0 == 0 /\ -sourceflag^post19+sourceflag^0 == 0 /\ destflag^0-destflag^post19 == 0 /\ -k^post19+k^0 == 0 /\ -h^post19+h^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ j^0-j^post19 == 0 /\ i^0-i^post19 == 0 /\ k_1^0-k_1^post19 == 0), cost: 1 4: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post5, destflag^0'=destflag^post5, edgecount^0'=edgecount^post5, h^0'=h^post5, i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, k_1^0'=k_1^post5, min^0'=min^post5, nodecount^0'=nodecount^post5, sourceflag^0'=sourceflag^post5, (h^0-h^post5 == 0 /\ nodecount^0-nodecount^post5 == 0 /\ -edgecount^post5+edgecount^0 == 0 /\ -destflag^post5+destflag^0 == 0 /\ -i^post5+i^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post5 == 0 /\ -min^post5+min^0 == 0 /\ 1-destflag^0 <= 0 /\ k^0-k^post5 == 0 /\ -j^post5+j^0 == 0 /\ -sourceflag^post5+sourceflag^0 == 0 /\ k_1^0-k_1^post5 == 0), cost: 1 5: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post6, destflag^0'=destflag^post6, edgecount^0'=edgecount^post6, h^0'=h^post6, i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, k_1^0'=k_1^post6, min^0'=min^post6, nodecount^0'=nodecount^post6, sourceflag^0'=sourceflag^post6, (destflag^0-destflag^post6 == 0 /\ min^0-min^post6 == 0 /\ edgecount^0-edgecount^post6 == 0 /\ -h^post6+h^0 == 0 /\ -__lengthofvisited^post6+__lengthofvisited^0 == 0 /\ 1+destflag^0 <= 0 /\ -k^post6+k^0 == 0 /\ -sourceflag^post6+sourceflag^0 == 0 /\ j^0-j^post6 == 0 /\ i^0-i^post6 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ k_1^0-k_1^post6 == 0), cost: 1 6: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post7, destflag^0'=destflag^post7, edgecount^0'=edgecount^post7, h^0'=h^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, k_1^0'=k_1^post7, min^0'=min^post7, nodecount^0'=nodecount^post7, sourceflag^0'=sourceflag^post7, (-j^post7+j^0 == 0 /\ -min^post7+min^0 == 0 /\ k^0-k^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ h^0-h^post7 == 0 /\ i^0-i^post7 == 0 /\ destflag^0 <= 0 /\ -edgecount^post7+edgecount^0 == 0 /\ k_1^0-k_1^post7 == 0 /\ -destflag^post7+destflag^0 == 0 /\ -destflag^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post7 == 0 /\ nodecount^0-nodecount^post7 == 0), cost: 1 7: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^post8, destflag^0'=destflag^post8, edgecount^0'=edgecount^post8, h^0'=h^post8, i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, k_1^0'=k_1^post8, min^0'=min^post8, nodecount^0'=nodecount^post8, sourceflag^0'=sourceflag^post8, (-sourceflag^post8+sourceflag^0 == 0 /\ k_1^0-k_1^post8 == 0 /\ k^0-k^post8 == 0 /\ -__lengthofvisited^post8+__lengthofvisited^0 == 0 /\ i^0-i^post8 == 0 /\ -edgecount^post8+edgecount^0 == 0 /\ h^0-h^post8 == 0 /\ -min^post8+min^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ -j^post8+j^0 == 0 /\ 1-sourceflag^0 <= 0 /\ destflag^0-destflag^post8 == 0), cost: 1 8: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^post9, destflag^0'=destflag^post9, edgecount^0'=edgecount^post9, h^0'=h^post9, i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, k_1^0'=k_1^post9, min^0'=min^post9, nodecount^0'=nodecount^post9, sourceflag^0'=sourceflag^post9, (1+sourceflag^0 <= 0 /\ k^0-k^post9 == 0 /\ -min^post9+min^0 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ k_1^0-k_1^post9 == 0 /\ -__lengthofvisited^post9+__lengthofvisited^0 == 0 /\ i^0-i^post9 == 0 /\ -nodecount^post9+nodecount^0 == 0 /\ -sourceflag^post9+sourceflag^0 == 0 /\ destflag^0-destflag^post9 == 0 /\ -j^post9+j^0 == 0 /\ -h^post9+h^0 == 0), cost: 1 9: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^post10, destflag^0'=destflag^post10, edgecount^0'=edgecount^post10, h^0'=h^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, k_1^0'=k_1^post10, min^0'=min^post10, nodecount^0'=nodecount^post10, sourceflag^0'=sourceflag^post10, (i^0-i^post10 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -destflag^post10+destflag^0 == 0 /\ -k^post10+k^0 == 0 /\ -sourceflag^post10+sourceflag^0 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ k_1^0-k_1^post10 == 0 /\ -sourceflag^0 <= 0 /\ -h^post10+h^0 == 0 /\ j^0-j^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0 <= 0), cost: 1 10: l10 -> l11 : __lengthofvisited^0'=__lengthofvisited^post11, destflag^0'=destflag^post11, edgecount^0'=edgecount^post11, h^0'=h^post11, i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, k_1^0'=k_1^post11, min^0'=min^post11, nodecount^0'=nodecount^post11, sourceflag^0'=sourceflag^post11, (nodecount^0-nodecount^post11 == 0 /\ i^0-i^post11 == 0 /\ h^0-h^post11 == 0 /\ -j^post11+j^0 == 0 /\ -min^post11+min^0 == 0 /\ k_1^0-k_1^post11 == 0 /\ destflag^0-destflag^post11 == 0 /\ -sourceflag^post11+sourceflag^0 == 0 /\ -__lengthofvisited^post11+__lengthofvisited^0 == 0 /\ -edgecount^post11+edgecount^0 == 0 /\ k^0-k^post11 == 0), cost: 1 32: l11 -> l7 : __lengthofvisited^0'=__lengthofvisited^post33, destflag^0'=destflag^post33, edgecount^0'=edgecount^post33, h^0'=h^post33, i^0'=i^post33, j^0'=j^post33, k^0'=k^post33, k_1^0'=k_1^post33, min^0'=min^post33, nodecount^0'=nodecount^post33, sourceflag^0'=sourceflag^post33, (-__lengthofvisited^post33+__lengthofvisited^0 == 0 /\ -h^post33+h^0 == 0 /\ -edgecount^post33+edgecount^0 == 0 /\ -j^post33+j^0 == 0 /\ i^0-i^post33 == 0 /\ min^0-min^post33 == 0 /\ -i^0+edgecount^0 <= 0 /\ -nodecount^post33+nodecount^0 == 0 /\ destflag^0-destflag^post33 == 0 /\ k_1^post33 == 0 /\ -k^post33+k^0 == 0 /\ -sourceflag^post33+sourceflag^0 == 0), cost: 1 33: l11 -> l10 : __lengthofvisited^0'=__lengthofvisited^post34, destflag^0'=destflag^post34, edgecount^0'=edgecount^post34, h^0'=h^post34, i^0'=i^post34, j^0'=j^post34, k^0'=k^post34, k_1^0'=k_1^post34, min^0'=min^post34, nodecount^0'=nodecount^post34, sourceflag^0'=sourceflag^post34, (-min^post34+min^0 == 0 /\ -k_1^post34+k_1^0 == 0 /\ -j^post34+j^0 == 0 /\ -destflag^post34+destflag^0 == 0 /\ -edgecount^post34+edgecount^0 == 0 /\ 1+i^0-edgecount^0 <= 0 /\ nodecount^0-nodecount^post34 == 0 /\ __lengthofvisited^0-__lengthofvisited^post34 == 0 /\ -sourceflag^post34+sourceflag^0 == 0 /\ k^0-k^post34 == 0 /\ -1+i^post34-i^0 == 0 /\ h^0-h^post34 == 0), cost: 1 11: l12 -> l13 : __lengthofvisited^0'=__lengthofvisited^post12, destflag^0'=destflag^post12, edgecount^0'=edgecount^post12, h^0'=h^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, k_1^0'=k_1^post12, min^0'=min^post12, nodecount^0'=nodecount^post12, sourceflag^0'=sourceflag^post12, (i^0-i^post12 == 0 /\ -h^post12+h^0 == 0 /\ k_1^0-k_1^post12 == 0 /\ destflag^0-destflag^post12 == 0 /\ -__lengthofvisited^post12+__lengthofvisited^0 == 0 /\ -min^post12+min^0 == 0 /\ -sourceflag^post12+sourceflag^0 == 0 /\ -edgecount^post12+edgecount^0 == 0 /\ -1+j^post12-j^0 == 0 /\ nodecount^0-nodecount^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 41: l13 -> l15 : __lengthofvisited^0'=__lengthofvisited^post42, destflag^0'=destflag^post42, edgecount^0'=edgecount^post42, h^0'=h^post42, i^0'=i^post42, j^0'=j^post42, k^0'=k^post42, k_1^0'=k_1^post42, min^0'=min^post42, nodecount^0'=nodecount^post42, sourceflag^0'=sourceflag^post42, (-__lengthofvisited^post42+__lengthofvisited^0 == 0 /\ -edgecount^post42+edgecount^0 == 0 /\ k_1^0-k_1^post42 == 0 /\ min^0-min^post42 == 0 /\ destflag^0-destflag^post42 == 0 /\ -sourceflag^post42+sourceflag^0 == 0 /\ i^0-i^post42 == 0 /\ -h^post42+h^0 == 0 /\ -nodecount^post42+nodecount^0 == 0 /\ -k^post42+k^0 == 0 /\ -j^post42+j^0 == 0), cost: 1 12: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post13, destflag^0'=destflag^post13, edgecount^0'=edgecount^post13, h^0'=h^post13, i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, k_1^0'=k_1^post13, min^0'=min^post13, nodecount^0'=nodecount^post13, sourceflag^0'=sourceflag^post13, (k_1^0-k_1^post13 == 0 /\ -__lengthofvisited^post13+__lengthofvisited^0 == 0 /\ min^0-min^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0 /\ destflag^0-destflag^post13 == 0 /\ i^0-i^post13 == 0 /\ -j^post13+j^0 == 0 /\ -edgecount^post13+edgecount^0 == 0 /\ -k^post13+k^0 == 0 /\ -h^post13+h^0 == 0 /\ -sourceflag^post13+sourceflag^0 == 0), cost: 1 13: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post14, destflag^0'=destflag^post14, edgecount^0'=edgecount^post14, h^0'=h^post14, i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, k_1^0'=k_1^post14, min^0'=min^post14, nodecount^0'=nodecount^post14, sourceflag^0'=sourceflag^post14, (-i^post14+i^0 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ destflag^post14 == 0 /\ -j^post14+j^0 == 0 /\ k_1^0-k_1^post14 == 0 /\ __lengthofvisited^0-__lengthofvisited^post14 == 0 /\ nodecount^0-nodecount^post14 == 0 /\ k^0-k^post14 == 0 /\ -min^post14+min^0 == 0 /\ h^0-h^post14 == 0 /\ -sourceflag^post14+sourceflag^0 == 0), cost: 1 14: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post15, destflag^0'=destflag^post15, edgecount^0'=edgecount^post15, h^0'=h^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, k_1^0'=k_1^post15, min^0'=min^post15, nodecount^0'=nodecount^post15, sourceflag^0'=sourceflag^post15, (-k^post15+k^0 == 0 /\ -__lengthofvisited^post15+__lengthofvisited^0 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ destflag^0-destflag^post15 == 0 /\ k_1^0-k_1^post15 == 0 /\ -h^post15+h^0 == 0 /\ -sourceflag^post15+sourceflag^0 == 0 /\ min^0-min^post15 == 0 /\ edgecount^0-edgecount^post15 == 0 /\ j^0-j^post15 == 0 /\ i^0-i^post15 == 0), cost: 1 15: l15 -> l9 : __lengthofvisited^0'=__lengthofvisited^post16, destflag^0'=destflag^post16, edgecount^0'=edgecount^post16, h^0'=h^post16, i^0'=i^post16, j^0'=j^post16, k^0'=k^post16, k_1^0'=k_1^post16, min^0'=min^post16, nodecount^0'=nodecount^post16, sourceflag^0'=sourceflag^post16, (k^0-k^post16 == 0 /\ -sourceflag^post16+sourceflag^0 == 0 /\ -edgecount^post16+edgecount^0 == 0 /\ -min^post16+min^0 == 0 /\ -h^post16+h^0 == 0 /\ -j^post16+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post16 == 0 /\ i^0-i^post16 == 0 /\ k_1^0-k_1^post16 == 0 /\ nodecount^0-j^0 <= 0 /\ destflag^0-destflag^post16 == 0 /\ nodecount^0-nodecount^post16 == 0), cost: 1 16: l15 -> l14 : __lengthofvisited^0'=__lengthofvisited^post17, destflag^0'=destflag^post17, edgecount^0'=edgecount^post17, h^0'=h^post17, i^0'=i^post17, j^0'=j^post17, k^0'=k^post17, k_1^0'=k_1^post17, min^0'=min^post17, nodecount^0'=nodecount^post17, sourceflag^0'=sourceflag^post17, (-min^post17+min^0 == 0 /\ k^0-k^post17 == 0 /\ -sourceflag^post17+sourceflag^0 == 0 /\ -__lengthofvisited^post17+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0 /\ i^0-i^post17 == 0 /\ -j^post17+j^0 == 0 /\ -h^post17+h^0 == 0 /\ nodecount^0-nodecount^post17 == 0 /\ destflag^0-destflag^post17 == 0 /\ 1-nodecount^0+j^0 <= 0), cost: 1 17: l16 -> l17 : __lengthofvisited^0'=__lengthofvisited^post18, destflag^0'=destflag^post18, edgecount^0'=edgecount^post18, h^0'=h^post18, i^0'=i^post18, j^0'=j^post18, k^0'=k^post18, k_1^0'=k_1^post18, min^0'=min^post18, nodecount^0'=nodecount^post18, sourceflag^0'=sourceflag^post18, (-1+j^post18-j^0 == 0 /\ k_1^0-k_1^post18 == 0 /\ k^0-k^post18 == 0 /\ -edgecount^post18+edgecount^0 == 0 /\ i^0-i^post18 == 0 /\ -__lengthofvisited^post18+__lengthofvisited^0 == 0 /\ nodecount^0-nodecount^post18 == 0 /\ h^0-h^post18 == 0 /\ -sourceflag^post18+sourceflag^0 == 0 /\ -min^post18+min^0 == 0 /\ destflag^0-destflag^post18 == 0), cost: 1 34: l17 -> l20 : __lengthofvisited^0'=__lengthofvisited^post35, destflag^0'=destflag^post35, edgecount^0'=edgecount^post35, h^0'=h^post35, i^0'=i^post35, j^0'=j^post35, k^0'=k^post35, k_1^0'=k_1^post35, min^0'=min^post35, nodecount^0'=nodecount^post35, sourceflag^0'=sourceflag^post35, (k_1^0-k_1^post35 == 0 /\ -h^post35+h^0 == 0 /\ -sourceflag^post35+sourceflag^0 == 0 /\ -__lengthofvisited^post35+__lengthofvisited^0 == 0 /\ -nodecount^post35+nodecount^0 == 0 /\ destflag^0-destflag^post35 == 0 /\ min^0-min^post35 == 0 /\ -k^post35+k^0 == 0 /\ edgecount^0-edgecount^post35 == 0 /\ j^0-j^post35 == 0 /\ i^0-i^post35 == 0), cost: 1 30: l18 -> l4 : __lengthofvisited^0'=__lengthofvisited^post31, destflag^0'=destflag^post31, edgecount^0'=edgecount^post31, h^0'=h^post31, i^0'=i^post31, j^0'=j^post31, k^0'=k^post31, k_1^0'=k_1^post31, min^0'=min^post31, nodecount^0'=nodecount^post31, sourceflag^0'=sourceflag^post31, (i^0-i^post31 == 0 /\ -1+k^post31-k^0 == 0 /\ destflag^0-destflag^post31 == 0 /\ -j^post31+j^0 == 0 /\ -k_1^0+edgecount^0 <= 0 /\ -h^post31+h^0 == 0 /\ -edgecount^post31+edgecount^0 == 0 /\ k_1^0-k_1^post31 == 0 /\ -__lengthofvisited^post31+__lengthofvisited^0 == 0 /\ -sourceflag^post31+sourceflag^0 == 0 /\ -min^post31+min^0 == 0 /\ nodecount^0-nodecount^post31 == 0), cost: 1 31: l18 -> l22 : __lengthofvisited^0'=__lengthofvisited^post32, destflag^0'=destflag^post32, edgecount^0'=edgecount^post32, h^0'=h^post32, i^0'=i^post32, j^0'=j^post32, k^0'=k^post32, k_1^0'=k_1^post32, min^0'=min^post32, nodecount^0'=nodecount^post32, sourceflag^0'=sourceflag^post32, (i^0-i^post32 == 0 /\ -__lengthofvisited^post32+__lengthofvisited^0 == 0 /\ h^post32 == 0 /\ -j^post32+j^0 == 0 /\ -destflag^post32+destflag^0 == 0 /\ -edgecount^post32+edgecount^0 == 0 /\ k_1^0-k_1^post32 == 0 /\ k^0-k^post32 == 0 /\ 1+k_1^0-edgecount^0 <= 0 /\ -min^post32+min^0 == 0 /\ nodecount^0-nodecount^post32 == 0 /\ -sourceflag^post32+sourceflag^0 == 0), cost: 1 19: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post20, destflag^0'=destflag^post20, edgecount^0'=edgecount^post20, h^0'=h^post20, i^0'=i^post20, j^0'=j^post20, k^0'=k^post20, k_1^0'=k_1^post20, min^0'=min^post20, nodecount^0'=nodecount^post20, sourceflag^0'=sourceflag^post20, (nodecount^0-nodecount^post20 == 0 /\ i^0-i^post20 == 0 /\ h^0-h^post20 == 0 /\ -sourceflag^post20+sourceflag^0 == 0 /\ -min^post20+min^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post20 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ k^0-k^post20 == 0 /\ -destflag^post20+destflag^0 == 0 /\ -j^post20+j^0 == 0 /\ k_1^0-k_1^post20 == 0), cost: 1 20: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post21, destflag^0'=destflag^post21, edgecount^0'=edgecount^post21, h^0'=h^post21, i^0'=i^post21, j^0'=j^post21, k^0'=k^post21, k_1^0'=k_1^post21, min^0'=min^post21, nodecount^0'=nodecount^post21, sourceflag^0'=sourceflag^post21, (i^0-i^post21 == 0 /\ destflag^0-destflag^post21 == 0 /\ -j^post21+j^0 == 0 /\ -h^post21+h^0 == 0 /\ -k^post21+k^0 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ -__lengthofvisited^post21+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post21 == 0 /\ -1+sourceflag^post21 == 0 /\ -min^post21+min^0 == 0 /\ nodecount^0-nodecount^post21 == 0), cost: 1 21: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post22, destflag^0'=destflag^post22, edgecount^0'=edgecount^post22, h^0'=h^post22, i^0'=i^post22, j^0'=j^post22, k^0'=k^post22, k_1^0'=k_1^post22, min^0'=min^post22, nodecount^0'=nodecount^post22, sourceflag^0'=sourceflag^post22, (i^0-i^post22 == 0 /\ -h^post22+h^0 == 0 /\ -j^post22+j^0 == 0 /\ k_1^0-k_1^post22 == 0 /\ destflag^0-destflag^post22 == 0 /\ -sourceflag^post22+sourceflag^0 == 0 /\ -__lengthofvisited^post22+__lengthofvisited^0 == 0 /\ -min^post22+min^0 == 0 /\ nodecount^0-nodecount^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0 /\ -k^post22+k^0 == 0), cost: 1 22: l20 -> l13 : __lengthofvisited^0'=__lengthofvisited^post23, destflag^0'=destflag^post23, edgecount^0'=edgecount^post23, h^0'=h^post23, i^0'=i^post23, j^0'=j^post23, k^0'=k^post23, k_1^0'=k_1^post23, min^0'=min^post23, nodecount^0'=nodecount^post23, sourceflag^0'=sourceflag^post23, (i^0-i^post23 == 0 /\ j^post23 == 0 /\ -edgecount^post23+edgecount^0 == 0 /\ -__lengthofvisited^post23+__lengthofvisited^0 == 0 /\ nodecount^0-j^0 <= 0 /\ k_1^0-k_1^post23 == 0 /\ -1+destflag^post23 == 0 /\ -min^post23+min^0 == 0 /\ -sourceflag^post23+sourceflag^0 == 0 /\ -h^post23+h^0 == 0 /\ k^0-k^post23 == 0 /\ nodecount^0-nodecount^post23 == 0), cost: 1 23: l20 -> l19 : __lengthofvisited^0'=__lengthofvisited^post24, destflag^0'=destflag^post24, edgecount^0'=edgecount^post24, h^0'=h^post24, i^0'=i^post24, j^0'=j^post24, k^0'=k^post24, k_1^0'=k_1^post24, min^0'=min^post24, nodecount^0'=nodecount^post24, sourceflag^0'=sourceflag^post24, (-edgecount^post24+edgecount^0 == 0 /\ -__lengthofvisited^post24+__lengthofvisited^0 == 0 /\ k^0-k^post24 == 0 /\ i^0-i^post24 == 0 /\ k_1^0-k_1^post24 == 0 /\ nodecount^0-nodecount^post24 == 0 /\ -min^post24+min^0 == 0 /\ h^0-h^post24 == 0 /\ destflag^0-destflag^post24 == 0 /\ -j^post24+j^0 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ -sourceflag^post24+sourceflag^0 == 0), cost: 1 24: l21 -> l22 : __lengthofvisited^0'=__lengthofvisited^post25, destflag^0'=destflag^post25, edgecount^0'=edgecount^post25, h^0'=h^post25, i^0'=i^post25, j^0'=j^post25, k^0'=k^post25, k_1^0'=k_1^post25, min^0'=min^post25, nodecount^0'=nodecount^post25, sourceflag^0'=sourceflag^post25, (-__lengthofvisited^post25+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post25 == 0 /\ -sourceflag^post25+sourceflag^0 == 0 /\ destflag^0-destflag^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ min^0-min^post25 == 0 /\ edgecount^0-edgecount^post25 == 0 /\ -k^post25+k^0 == 0 /\ -1+h^post25-h^0 == 0 /\ j^0-j^post25 == 0 /\ i^0-i^post25 == 0), cost: 1 27: l22 -> l24 : __lengthofvisited^0'=__lengthofvisited^post28, destflag^0'=destflag^post28, edgecount^0'=edgecount^post28, h^0'=h^post28, i^0'=i^post28, j^0'=j^post28, k^0'=k^post28, k_1^0'=k_1^post28, min^0'=min^post28, nodecount^0'=nodecount^post28, sourceflag^0'=sourceflag^post28, (k^0-k^post28 == 0 /\ k_1^0-k_1^post28 == 0 /\ -__lengthofvisited^post28+__lengthofvisited^0 == 0 /\ -edgecount^post28+edgecount^0 == 0 /\ i^0-i^post28 == 0 /\ -j^post28+j^0 == 0 /\ -sourceflag^post28+sourceflag^0 == 0 /\ nodecount^0-nodecount^post28 == 0 /\ h^0-h^post28 == 0 /\ -min^post28+min^0 == 0 /\ destflag^0-destflag^post28 == 0), cost: 1 25: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^post26, destflag^0'=destflag^post26, edgecount^0'=edgecount^post26, h^0'=h^post26, i^0'=i^post26, j^0'=j^post26, k^0'=k^post26, k_1^0'=k_1^post26, min^0'=min^post26, nodecount^0'=nodecount^post26, sourceflag^0'=sourceflag^post26, (-i^post26+i^0 == 0 /\ -j^post26+j^0 == 0 /\ -sourceflag^post26+sourceflag^0 == 0 /\ -k_1^post26+k_1^0 == 0 /\ min^post26-h^0 == 0 /\ nodecount^0-nodecount^post26 == 0 /\ __lengthofvisited^0-__lengthofvisited^post26 == 0 /\ -edgecount^post26+edgecount^0 == 0 /\ k^0-k^post26 == 0 /\ h^0-h^post26 == 0 /\ -destflag^post26+destflag^0 == 0), cost: 1 26: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^post27, destflag^0'=destflag^post27, edgecount^0'=edgecount^post27, h^0'=h^post27, i^0'=i^post27, j^0'=j^post27, k^0'=k^post27, k_1^0'=k_1^post27, min^0'=min^post27, nodecount^0'=nodecount^post27, sourceflag^0'=sourceflag^post27, (-sourceflag^post27+sourceflag^0 == 0 /\ -min^post27+min^0 == 0 /\ -__lengthofvisited^post27+__lengthofvisited^0 == 0 /\ destflag^0-destflag^post27 == 0 /\ -edgecount^post27+edgecount^0 == 0 /\ -k^post27+k^0 == 0 /\ nodecount^0-nodecount^post27 == 0 /\ j^0-j^post27 == 0 /\ k_1^0-k_1^post27 == 0 /\ -h^post27+h^0 == 0 /\ i^0-i^post27 == 0), cost: 1 28: l24 -> l17 : __lengthofvisited^0'=__lengthofvisited^post29, destflag^0'=destflag^post29, edgecount^0'=edgecount^post29, h^0'=h^post29, i^0'=i^post29, j^0'=j^post29, k^0'=k^post29, k_1^0'=k_1^post29, min^0'=min^post29, nodecount^0'=nodecount^post29, sourceflag^0'=sourceflag^post29, (j^post29 == 0 /\ destflag^0-destflag^post29 == 0 /\ k_1^0-k_1^post29 == 0 /\ -edgecount^post29+edgecount^0 == 0 /\ min^0-min^post29 == 0 /\ i^0-i^post29 == 0 /\ sourceflag^post29 == 0 /\ -k^post29+k^0 == 0 /\ -nodecount^post29+nodecount^0 == 0 /\ -h^post29+h^0 == 0 /\ -__lengthofvisited^post29+__lengthofvisited^0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1 29: l24 -> l23 : __lengthofvisited^0'=__lengthofvisited^post30, destflag^0'=destflag^post30, edgecount^0'=edgecount^post30, h^0'=h^post30, i^0'=i^post30, j^0'=j^post30, k^0'=k^post30, k_1^0'=k_1^post30, min^0'=min^post30, nodecount^0'=nodecount^post30, sourceflag^0'=sourceflag^post30, (__lengthofvisited^0-__lengthofvisited^post30 == 0 /\ nodecount^0-nodecount^post30 == 0 /\ -min^post30+min^0 == 0 /\ -destflag^post30+destflag^0 == 0 /\ -sourceflag^post30+sourceflag^0 == 0 /\ k^0-k^post30 == 0 /\ -j^post30+j^0 == 0 /\ i^0-i^post30 == 0 /\ 1+h^0-edgecount^0 <= 0 /\ h^0-h^post30 == 0 /\ k_1^0-k_1^post30 == 0 /\ -edgecount^post30+edgecount^0 == 0), cost: 1 35: l25 -> l10 : __lengthofvisited^0'=__lengthofvisited^post36, destflag^0'=destflag^post36, edgecount^0'=edgecount^post36, h^0'=h^post36, i^0'=i^post36, j^0'=j^post36, k^0'=k^post36, k_1^0'=k_1^post36, min^0'=min^post36, nodecount^0'=nodecount^post36, sourceflag^0'=sourceflag^post36, (-j^post36+j^0 == 0 /\ k^0-k^post36 == 0 /\ min^post36 == 0 /\ h^0-h^post36 == 0 /\ -sourceflag^post36+sourceflag^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post36 == 0 /\ -edgecount^post36+edgecount^0 == 0 /\ k_1^0-k_1^post36 == 0 /\ nodecount^0-nodecount^post36 == 0 /\ -destflag^post36+destflag^0 == 0 /\ i^post36 == 0), cost: 1 44: l27 -> l0 : __lengthofvisited^0'=__lengthofvisited^post45, destflag^0'=destflag^post45, edgecount^0'=edgecount^post45, h^0'=h^post45, i^0'=i^post45, j^0'=j^post45, k^0'=k^post45, k_1^0'=k_1^post45, min^0'=min^post45, nodecount^0'=nodecount^post45, sourceflag^0'=sourceflag^post45, (sourceflag^0-sourceflag^post45 == 0 /\ -1+i^post45 == 0 /\ -k_1^post45+k_1^0 == 0 /\ k^0-k^post45 == 0 /\ nodecount^0-nodecount^post45 == 0 /\ -j^post45+j^0 == 0 /\ __lengthofvisited^post45-edgecount^0 == 0 /\ h^0-h^post45 == 0 /\ -min^post45+min^0 == 0 /\ -destflag^post45+destflag^0 == 0 /\ -edgecount^post45+edgecount^0 == 0), cost: 1 45: l28 -> l27 : __lengthofvisited^0'=__lengthofvisited^post46, destflag^0'=destflag^post46, edgecount^0'=edgecount^post46, h^0'=h^post46, i^0'=i^post46, j^0'=j^post46, k^0'=k^post46, k_1^0'=k_1^post46, min^0'=min^post46, nodecount^0'=nodecount^post46, sourceflag^0'=sourceflag^post46, (edgecount^0-edgecount^post46 == 0 /\ k_1^0-k_1^post46 == 0 /\ -k^post46+k^0 == 0 /\ min^0-min^post46 == 0 /\ -__lengthofvisited^post46+__lengthofvisited^0 == 0 /\ -nodecount^post46+nodecount^0 == 0 /\ destflag^0-destflag^post46 == 0 /\ -sourceflag^post46+sourceflag^0 == 0 /\ j^0-j^post46 == 0 /\ -h^post46+h^0 == 0 /\ i^0-i^post46 == 0), cost: 1 Chained Linear Paths Start location: l28 Program variables: __lengthofvisited^0 destflag^0 edgecount^0 h^0 i^0 j^0 k^0 k_1^0 min^0 nodecount^0 sourceflag^0 0: l0 -> l1 : __lengthofvisited^0'=__lengthofvisited^post1, destflag^0'=destflag^post1, edgecount^0'=edgecount^post1, h^0'=h^post1, i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, k_1^0'=k_1^post1, min^0'=min^post1, nodecount^0'=nodecount^post1, sourceflag^0'=sourceflag^post1, (__lengthofvisited^0-__lengthofvisited^post1 == 0 /\ nodecount^0-nodecount^post1 == 0 /\ -j^post1+j^0 == 0 /\ -min^post1+min^0 == 0 /\ -destflag^post1+destflag^0 == 0 /\ k^0-k^post1 == 0 /\ -sourceflag^post1+sourceflag^0 == 0 /\ h^0-h^post1 == 0 /\ k_1^0-k_1^post1 == 0 /\ -i^post1+i^0 == 0 /\ -edgecount^post1+edgecount^0 == 0), cost: 1 42: l1 -> l2 : __lengthofvisited^0'=__lengthofvisited^post43, destflag^0'=destflag^post43, edgecount^0'=edgecount^post43, h^0'=h^post43, i^0'=i^post43, j^0'=j^post43, k^0'=k^post43, k_1^0'=k_1^post43, min^0'=min^post43, nodecount^0'=nodecount^post43, sourceflag^0'=sourceflag^post43, (-i^0+nodecount^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post43 == 0 /\ -j^post43+j^0 == 0 /\ i^post43 == 0 /\ -k_1^post43+k_1^0 == 0 /\ -destflag^post43+destflag^0 == 0 /\ nodecount^0-nodecount^post43 == 0 /\ -min^post43+min^0 == 0 /\ k^0-k^post43 == 0 /\ -sourceflag^post43+sourceflag^0 == 0 /\ h^0-h^post43 == 0 /\ -edgecount^post43+edgecount^0 == 0), cost: 1 43: l1 -> l0 : __lengthofvisited^0'=__lengthofvisited^post44, destflag^0'=destflag^post44, edgecount^0'=edgecount^post44, h^0'=h^post44, i^0'=i^post44, j^0'=j^post44, k^0'=k^post44, k_1^0'=k_1^post44, min^0'=min^post44, nodecount^0'=nodecount^post44, sourceflag^0'=sourceflag^post44, (k_1^0-k_1^post44 == 0 /\ -k^post44+k^0 == 0 /\ -1-i^0+i^post44 == 0 /\ -nodecount^post44+nodecount^0 == 0 /\ -sourceflag^post44+sourceflag^0 == 0 /\ destflag^0-destflag^post44 == 0 /\ min^0-min^post44 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ -h^post44+h^0 == 0 /\ j^0-j^post44 == 0 /\ -__lengthofvisited^post44+__lengthofvisited^0 == 0 /\ -edgecount^post44+edgecount^0 == 0), cost: 1 1: l2 -> l3 : __lengthofvisited^0'=__lengthofvisited^post2, destflag^0'=destflag^post2, edgecount^0'=edgecount^post2, h^0'=h^post2, i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, k_1^0'=k_1^post2, min^0'=min^post2, nodecount^0'=nodecount^post2, sourceflag^0'=sourceflag^post2, (i^0-i^post2 == 0 /\ -h^post2+h^0 == 0 /\ -j^post2+j^0 == 0 /\ k_1^0-k_1^post2 == 0 /\ destflag^0-destflag^post2 == 0 /\ -k^post2+k^0 == 0 /\ -__lengthofvisited^post2+__lengthofvisited^0 == 0 /\ -min^post2+min^0 == 0 /\ -sourceflag^post2+sourceflag^0 == 0 /\ -edgecount^post2+edgecount^0 == 0 /\ nodecount^0-nodecount^post2 == 0), cost: 1 39: l3 -> l4 : __lengthofvisited^0'=__lengthofvisited^post40, destflag^0'=destflag^post40, edgecount^0'=edgecount^post40, h^0'=h^post40, i^0'=i^post40, j^0'=j^post40, k^0'=k^post40, k_1^0'=k_1^post40, min^0'=min^post40, nodecount^0'=nodecount^post40, sourceflag^0'=sourceflag^post40, (nodecount^0-nodecount^post40 == 0 /\ i^0-i^post40 == 0 /\ -sourceflag^post40+sourceflag^0 == 0 /\ h^0-h^post40 == 0 /\ -j^post40+j^0 == 0 /\ k^post40 == 0 /\ __lengthofvisited^0-__lengthofvisited^post40 == 0 /\ destflag^0-destflag^post40 == 0 /\ k_1^0-k_1^post40 == 0 /\ -edgecount^post40+edgecount^0 == 0 /\ -1-i^0+nodecount^0 <= 0 /\ -min^post40+min^0 == 0), cost: 1 40: l3 -> l2 : __lengthofvisited^0'=__lengthofvisited^post41, destflag^0'=destflag^post41, edgecount^0'=edgecount^post41, h^0'=h^post41, i^0'=i^post41, j^0'=j^post41, k^0'=k^post41, k_1^0'=k_1^post41, min^0'=min^post41, nodecount^0'=nodecount^post41, sourceflag^0'=sourceflag^post41, (2+i^0-nodecount^0 <= 0 /\ destflag^0-destflag^post41 == 0 /\ -j^post41+j^0 == 0 /\ -h^post41+h^0 == 0 /\ -edgecount^post41+edgecount^0 == 0 /\ -__lengthofvisited^post41+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post41 == 0 /\ -1-i^0+i^post41 == 0 /\ -k^post41+k^0 == 0 /\ -sourceflag^post41+sourceflag^0 == 0 /\ nodecount^0-nodecount^post41 == 0 /\ -min^post41+min^0 == 0), cost: 1 2: l4 -> l5 : __lengthofvisited^0'=__lengthofvisited^post3, destflag^0'=destflag^post3, edgecount^0'=edgecount^post3, h^0'=h^post3, i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, k_1^0'=k_1^post3, min^0'=min^post3, nodecount^0'=nodecount^post3, sourceflag^0'=sourceflag^post3, (i^0-i^post3 == 0 /\ h^0-h^post3 == 0 /\ -j^post3+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post3 == 0 /\ destflag^0-destflag^post3 == 0 /\ k_1^0-k_1^post3 == 0 /\ -edgecount^post3+edgecount^0 == 0 /\ -sourceflag^post3+sourceflag^0 == 0 /\ -min^post3+min^0 == 0 /\ nodecount^0-nodecount^post3 == 0 /\ k^0-k^post3 == 0), cost: 1 36: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^post37, destflag^0'=destflag^post37, edgecount^0'=edgecount^post37, h^0'=h^post37, i^0'=i^post37, j^0'=j^post37, k^0'=k^post37, k_1^0'=k_1^post37, min^0'=min^post37, nodecount^0'=nodecount^post37, sourceflag^0'=sourceflag^post37, (-1+nodecount^0-k^0 <= 0 /\ k^0-k^post37 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ -min^post37+min^0 == 0 /\ k_1^0-k_1^post37 == 0 /\ i^0-i^post37 == 0 /\ 1-nodecount^0+k^0 <= 0 /\ h^0-h^post37 == 0 /\ nodecount^0-nodecount^post37 == 0 /\ -j^post37+j^0 == 0 /\ destflag^0-destflag^post37 == 0), cost: 1 37: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^post38, destflag^0'=destflag^post38, edgecount^0'=edgecount^post38, h^0'=h^post38, i^0'=i^post38, j^0'=j^post38, k^0'=k^post38, k_1^0'=k_1^post38, min^0'=min^post38, nodecount^0'=nodecount^post38, sourceflag^0'=sourceflag^post38, (k^0-k^post38 == 0 /\ -__lengthofvisited^post38+__lengthofvisited^0 == 0 /\ -min^post38+min^0 == 0 /\ -edgecount^post38+edgecount^0 == 0 /\ -sourceflag^post38+sourceflag^0 == 0 /\ i^0-i^post38 == 0 /\ k_1^0-k_1^post38 == 0 /\ -j^post38+j^0 == 0 /\ -h^post38+h^0 == 0 /\ -nodecount^post38+nodecount^0 == 0 /\ nodecount^0-k^0 <= 0 /\ destflag^0-destflag^post38 == 0), cost: 1 38: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^post39, destflag^0'=destflag^post39, edgecount^0'=edgecount^post39, h^0'=h^post39, i^0'=i^post39, j^0'=j^post39, k^0'=k^post39, k_1^0'=k_1^post39, min^0'=min^post39, nodecount^0'=nodecount^post39, sourceflag^0'=sourceflag^post39, (min^0-min^post39 == 0 /\ __lengthofvisited^0-__lengthofvisited^post39 == 0 /\ -sourceflag^post39+sourceflag^0 == 0 /\ -k^post39+k^0 == 0 /\ -edgecount^post39+edgecount^0 == 0 /\ -destflag^post39+destflag^0 == 0 /\ h^0-h^post39 == 0 /\ j^0-j^post39 == 0 /\ -nodecount^post39+nodecount^0 == 0 /\ 2-nodecount^0+k^0 <= 0 /\ k_1^0-k_1^post39 == 0 /\ i^0-i^post39 == 0), cost: 1 3: l6 -> l7 : __lengthofvisited^0'=__lengthofvisited^post4, destflag^0'=destflag^post4, edgecount^0'=edgecount^post4, h^0'=h^post4, i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, k_1^0'=k_1^post4, min^0'=min^post4, nodecount^0'=nodecount^post4, sourceflag^0'=sourceflag^post4, (-edgecount^post4+edgecount^0 == 0 /\ -h^post4+h^0 == 0 /\ -__lengthofvisited^post4+__lengthofvisited^0 == 0 /\ -nodecount^post4+nodecount^0 == 0 /\ min^0-min^post4 == 0 /\ i^0-i^post4 == 0 /\ j^0-j^post4 == 0 /\ destflag^0-destflag^post4 == 0 /\ -1-k_1^0+k_1^post4 == 0 /\ -sourceflag^post4+sourceflag^0 == 0 /\ -k^post4+k^0 == 0), cost: 1 18: l7 -> l18 : __lengthofvisited^0'=__lengthofvisited^post19, destflag^0'=destflag^post19, edgecount^0'=edgecount^post19, h^0'=h^post19, i^0'=i^post19, j^0'=j^post19, k^0'=k^post19, k_1^0'=k_1^post19, min^0'=min^post19, nodecount^0'=nodecount^post19, sourceflag^0'=sourceflag^post19, (min^0-min^post19 == 0 /\ edgecount^0-edgecount^post19 == 0 /\ -__lengthofvisited^post19+__lengthofvisited^0 == 0 /\ -sourceflag^post19+sourceflag^0 == 0 /\ destflag^0-destflag^post19 == 0 /\ -k^post19+k^0 == 0 /\ -h^post19+h^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ j^0-j^post19 == 0 /\ i^0-i^post19 == 0 /\ k_1^0-k_1^post19 == 0), cost: 1 4: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post5, destflag^0'=destflag^post5, edgecount^0'=edgecount^post5, h^0'=h^post5, i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, k_1^0'=k_1^post5, min^0'=min^post5, nodecount^0'=nodecount^post5, sourceflag^0'=sourceflag^post5, (h^0-h^post5 == 0 /\ nodecount^0-nodecount^post5 == 0 /\ -edgecount^post5+edgecount^0 == 0 /\ -destflag^post5+destflag^0 == 0 /\ -i^post5+i^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post5 == 0 /\ -min^post5+min^0 == 0 /\ 1-destflag^0 <= 0 /\ k^0-k^post5 == 0 /\ -j^post5+j^0 == 0 /\ -sourceflag^post5+sourceflag^0 == 0 /\ k_1^0-k_1^post5 == 0), cost: 1 5: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post6, destflag^0'=destflag^post6, edgecount^0'=edgecount^post6, h^0'=h^post6, i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, k_1^0'=k_1^post6, min^0'=min^post6, nodecount^0'=nodecount^post6, sourceflag^0'=sourceflag^post6, (destflag^0-destflag^post6 == 0 /\ min^0-min^post6 == 0 /\ edgecount^0-edgecount^post6 == 0 /\ -h^post6+h^0 == 0 /\ -__lengthofvisited^post6+__lengthofvisited^0 == 0 /\ 1+destflag^0 <= 0 /\ -k^post6+k^0 == 0 /\ -sourceflag^post6+sourceflag^0 == 0 /\ j^0-j^post6 == 0 /\ i^0-i^post6 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ k_1^0-k_1^post6 == 0), cost: 1 6: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post7, destflag^0'=destflag^post7, edgecount^0'=edgecount^post7, h^0'=h^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, k_1^0'=k_1^post7, min^0'=min^post7, nodecount^0'=nodecount^post7, sourceflag^0'=sourceflag^post7, (-j^post7+j^0 == 0 /\ -min^post7+min^0 == 0 /\ k^0-k^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ h^0-h^post7 == 0 /\ i^0-i^post7 == 0 /\ destflag^0 <= 0 /\ -edgecount^post7+edgecount^0 == 0 /\ k_1^0-k_1^post7 == 0 /\ -destflag^post7+destflag^0 == 0 /\ -destflag^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post7 == 0 /\ nodecount^0-nodecount^post7 == 0), cost: 1 7: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^post8, destflag^0'=destflag^post8, edgecount^0'=edgecount^post8, h^0'=h^post8, i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, k_1^0'=k_1^post8, min^0'=min^post8, nodecount^0'=nodecount^post8, sourceflag^0'=sourceflag^post8, (-sourceflag^post8+sourceflag^0 == 0 /\ k_1^0-k_1^post8 == 0 /\ k^0-k^post8 == 0 /\ -__lengthofvisited^post8+__lengthofvisited^0 == 0 /\ i^0-i^post8 == 0 /\ -edgecount^post8+edgecount^0 == 0 /\ h^0-h^post8 == 0 /\ -min^post8+min^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ -j^post8+j^0 == 0 /\ 1-sourceflag^0 <= 0 /\ destflag^0-destflag^post8 == 0), cost: 1 8: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^post9, destflag^0'=destflag^post9, edgecount^0'=edgecount^post9, h^0'=h^post9, i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, k_1^0'=k_1^post9, min^0'=min^post9, nodecount^0'=nodecount^post9, sourceflag^0'=sourceflag^post9, (1+sourceflag^0 <= 0 /\ k^0-k^post9 == 0 /\ -min^post9+min^0 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ k_1^0-k_1^post9 == 0 /\ -__lengthofvisited^post9+__lengthofvisited^0 == 0 /\ i^0-i^post9 == 0 /\ -nodecount^post9+nodecount^0 == 0 /\ -sourceflag^post9+sourceflag^0 == 0 /\ destflag^0-destflag^post9 == 0 /\ -j^post9+j^0 == 0 /\ -h^post9+h^0 == 0), cost: 1 9: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^post10, destflag^0'=destflag^post10, edgecount^0'=edgecount^post10, h^0'=h^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, k_1^0'=k_1^post10, min^0'=min^post10, nodecount^0'=nodecount^post10, sourceflag^0'=sourceflag^post10, (i^0-i^post10 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -destflag^post10+destflag^0 == 0 /\ -k^post10+k^0 == 0 /\ -sourceflag^post10+sourceflag^0 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ k_1^0-k_1^post10 == 0 /\ -sourceflag^0 <= 0 /\ -h^post10+h^0 == 0 /\ j^0-j^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0 <= 0), cost: 1 10: l10 -> l11 : __lengthofvisited^0'=__lengthofvisited^post11, destflag^0'=destflag^post11, edgecount^0'=edgecount^post11, h^0'=h^post11, i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, k_1^0'=k_1^post11, min^0'=min^post11, nodecount^0'=nodecount^post11, sourceflag^0'=sourceflag^post11, (nodecount^0-nodecount^post11 == 0 /\ i^0-i^post11 == 0 /\ h^0-h^post11 == 0 /\ -j^post11+j^0 == 0 /\ -min^post11+min^0 == 0 /\ k_1^0-k_1^post11 == 0 /\ destflag^0-destflag^post11 == 0 /\ -sourceflag^post11+sourceflag^0 == 0 /\ -__lengthofvisited^post11+__lengthofvisited^0 == 0 /\ -edgecount^post11+edgecount^0 == 0 /\ k^0-k^post11 == 0), cost: 1 32: l11 -> l7 : __lengthofvisited^0'=__lengthofvisited^post33, destflag^0'=destflag^post33, edgecount^0'=edgecount^post33, h^0'=h^post33, i^0'=i^post33, j^0'=j^post33, k^0'=k^post33, k_1^0'=k_1^post33, min^0'=min^post33, nodecount^0'=nodecount^post33, sourceflag^0'=sourceflag^post33, (-__lengthofvisited^post33+__lengthofvisited^0 == 0 /\ -h^post33+h^0 == 0 /\ -edgecount^post33+edgecount^0 == 0 /\ -j^post33+j^0 == 0 /\ i^0-i^post33 == 0 /\ min^0-min^post33 == 0 /\ -i^0+edgecount^0 <= 0 /\ -nodecount^post33+nodecount^0 == 0 /\ destflag^0-destflag^post33 == 0 /\ k_1^post33 == 0 /\ -k^post33+k^0 == 0 /\ -sourceflag^post33+sourceflag^0 == 0), cost: 1 33: l11 -> l10 : __lengthofvisited^0'=__lengthofvisited^post34, destflag^0'=destflag^post34, edgecount^0'=edgecount^post34, h^0'=h^post34, i^0'=i^post34, j^0'=j^post34, k^0'=k^post34, k_1^0'=k_1^post34, min^0'=min^post34, nodecount^0'=nodecount^post34, sourceflag^0'=sourceflag^post34, (-min^post34+min^0 == 0 /\ -k_1^post34+k_1^0 == 0 /\ -j^post34+j^0 == 0 /\ -destflag^post34+destflag^0 == 0 /\ -edgecount^post34+edgecount^0 == 0 /\ 1+i^0-edgecount^0 <= 0 /\ nodecount^0-nodecount^post34 == 0 /\ __lengthofvisited^0-__lengthofvisited^post34 == 0 /\ -sourceflag^post34+sourceflag^0 == 0 /\ k^0-k^post34 == 0 /\ -1+i^post34-i^0 == 0 /\ h^0-h^post34 == 0), cost: 1 11: l12 -> l13 : __lengthofvisited^0'=__lengthofvisited^post12, destflag^0'=destflag^post12, edgecount^0'=edgecount^post12, h^0'=h^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, k_1^0'=k_1^post12, min^0'=min^post12, nodecount^0'=nodecount^post12, sourceflag^0'=sourceflag^post12, (i^0-i^post12 == 0 /\ -h^post12+h^0 == 0 /\ k_1^0-k_1^post12 == 0 /\ destflag^0-destflag^post12 == 0 /\ -__lengthofvisited^post12+__lengthofvisited^0 == 0 /\ -min^post12+min^0 == 0 /\ -sourceflag^post12+sourceflag^0 == 0 /\ -edgecount^post12+edgecount^0 == 0 /\ -1+j^post12-j^0 == 0 /\ nodecount^0-nodecount^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 41: l13 -> l15 : __lengthofvisited^0'=__lengthofvisited^post42, destflag^0'=destflag^post42, edgecount^0'=edgecount^post42, h^0'=h^post42, i^0'=i^post42, j^0'=j^post42, k^0'=k^post42, k_1^0'=k_1^post42, min^0'=min^post42, nodecount^0'=nodecount^post42, sourceflag^0'=sourceflag^post42, (-__lengthofvisited^post42+__lengthofvisited^0 == 0 /\ -edgecount^post42+edgecount^0 == 0 /\ k_1^0-k_1^post42 == 0 /\ min^0-min^post42 == 0 /\ destflag^0-destflag^post42 == 0 /\ -sourceflag^post42+sourceflag^0 == 0 /\ i^0-i^post42 == 0 /\ -h^post42+h^0 == 0 /\ -nodecount^post42+nodecount^0 == 0 /\ -k^post42+k^0 == 0 /\ -j^post42+j^0 == 0), cost: 1 12: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post13, destflag^0'=destflag^post13, edgecount^0'=edgecount^post13, h^0'=h^post13, i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, k_1^0'=k_1^post13, min^0'=min^post13, nodecount^0'=nodecount^post13, sourceflag^0'=sourceflag^post13, (k_1^0-k_1^post13 == 0 /\ -__lengthofvisited^post13+__lengthofvisited^0 == 0 /\ min^0-min^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0 /\ destflag^0-destflag^post13 == 0 /\ i^0-i^post13 == 0 /\ -j^post13+j^0 == 0 /\ -edgecount^post13+edgecount^0 == 0 /\ -k^post13+k^0 == 0 /\ -h^post13+h^0 == 0 /\ -sourceflag^post13+sourceflag^0 == 0), cost: 1 13: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post14, destflag^0'=destflag^post14, edgecount^0'=edgecount^post14, h^0'=h^post14, i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, k_1^0'=k_1^post14, min^0'=min^post14, nodecount^0'=nodecount^post14, sourceflag^0'=sourceflag^post14, (-i^post14+i^0 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ destflag^post14 == 0 /\ -j^post14+j^0 == 0 /\ k_1^0-k_1^post14 == 0 /\ __lengthofvisited^0-__lengthofvisited^post14 == 0 /\ nodecount^0-nodecount^post14 == 0 /\ k^0-k^post14 == 0 /\ -min^post14+min^0 == 0 /\ h^0-h^post14 == 0 /\ -sourceflag^post14+sourceflag^0 == 0), cost: 1 14: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post15, destflag^0'=destflag^post15, edgecount^0'=edgecount^post15, h^0'=h^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, k_1^0'=k_1^post15, min^0'=min^post15, nodecount^0'=nodecount^post15, sourceflag^0'=sourceflag^post15, (-k^post15+k^0 == 0 /\ -__lengthofvisited^post15+__lengthofvisited^0 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ destflag^0-destflag^post15 == 0 /\ k_1^0-k_1^post15 == 0 /\ -h^post15+h^0 == 0 /\ -sourceflag^post15+sourceflag^0 == 0 /\ min^0-min^post15 == 0 /\ edgecount^0-edgecount^post15 == 0 /\ j^0-j^post15 == 0 /\ i^0-i^post15 == 0), cost: 1 15: l15 -> l9 : __lengthofvisited^0'=__lengthofvisited^post16, destflag^0'=destflag^post16, edgecount^0'=edgecount^post16, h^0'=h^post16, i^0'=i^post16, j^0'=j^post16, k^0'=k^post16, k_1^0'=k_1^post16, min^0'=min^post16, nodecount^0'=nodecount^post16, sourceflag^0'=sourceflag^post16, (k^0-k^post16 == 0 /\ -sourceflag^post16+sourceflag^0 == 0 /\ -edgecount^post16+edgecount^0 == 0 /\ -min^post16+min^0 == 0 /\ -h^post16+h^0 == 0 /\ -j^post16+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post16 == 0 /\ i^0-i^post16 == 0 /\ k_1^0-k_1^post16 == 0 /\ nodecount^0-j^0 <= 0 /\ destflag^0-destflag^post16 == 0 /\ nodecount^0-nodecount^post16 == 0), cost: 1 16: l15 -> l14 : __lengthofvisited^0'=__lengthofvisited^post17, destflag^0'=destflag^post17, edgecount^0'=edgecount^post17, h^0'=h^post17, i^0'=i^post17, j^0'=j^post17, k^0'=k^post17, k_1^0'=k_1^post17, min^0'=min^post17, nodecount^0'=nodecount^post17, sourceflag^0'=sourceflag^post17, (-min^post17+min^0 == 0 /\ k^0-k^post17 == 0 /\ -sourceflag^post17+sourceflag^0 == 0 /\ -__lengthofvisited^post17+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0 /\ i^0-i^post17 == 0 /\ -j^post17+j^0 == 0 /\ -h^post17+h^0 == 0 /\ nodecount^0-nodecount^post17 == 0 /\ destflag^0-destflag^post17 == 0 /\ 1-nodecount^0+j^0 <= 0), cost: 1 17: l16 -> l17 : __lengthofvisited^0'=__lengthofvisited^post18, destflag^0'=destflag^post18, edgecount^0'=edgecount^post18, h^0'=h^post18, i^0'=i^post18, j^0'=j^post18, k^0'=k^post18, k_1^0'=k_1^post18, min^0'=min^post18, nodecount^0'=nodecount^post18, sourceflag^0'=sourceflag^post18, (-1+j^post18-j^0 == 0 /\ k_1^0-k_1^post18 == 0 /\ k^0-k^post18 == 0 /\ -edgecount^post18+edgecount^0 == 0 /\ i^0-i^post18 == 0 /\ -__lengthofvisited^post18+__lengthofvisited^0 == 0 /\ nodecount^0-nodecount^post18 == 0 /\ h^0-h^post18 == 0 /\ -sourceflag^post18+sourceflag^0 == 0 /\ -min^post18+min^0 == 0 /\ destflag^0-destflag^post18 == 0), cost: 1 34: l17 -> l20 : __lengthofvisited^0'=__lengthofvisited^post35, destflag^0'=destflag^post35, edgecount^0'=edgecount^post35, h^0'=h^post35, i^0'=i^post35, j^0'=j^post35, k^0'=k^post35, k_1^0'=k_1^post35, min^0'=min^post35, nodecount^0'=nodecount^post35, sourceflag^0'=sourceflag^post35, (k_1^0-k_1^post35 == 0 /\ -h^post35+h^0 == 0 /\ -sourceflag^post35+sourceflag^0 == 0 /\ -__lengthofvisited^post35+__lengthofvisited^0 == 0 /\ -nodecount^post35+nodecount^0 == 0 /\ destflag^0-destflag^post35 == 0 /\ min^0-min^post35 == 0 /\ -k^post35+k^0 == 0 /\ edgecount^0-edgecount^post35 == 0 /\ j^0-j^post35 == 0 /\ i^0-i^post35 == 0), cost: 1 30: l18 -> l4 : __lengthofvisited^0'=__lengthofvisited^post31, destflag^0'=destflag^post31, edgecount^0'=edgecount^post31, h^0'=h^post31, i^0'=i^post31, j^0'=j^post31, k^0'=k^post31, k_1^0'=k_1^post31, min^0'=min^post31, nodecount^0'=nodecount^post31, sourceflag^0'=sourceflag^post31, (i^0-i^post31 == 0 /\ -1+k^post31-k^0 == 0 /\ destflag^0-destflag^post31 == 0 /\ -j^post31+j^0 == 0 /\ -k_1^0+edgecount^0 <= 0 /\ -h^post31+h^0 == 0 /\ -edgecount^post31+edgecount^0 == 0 /\ k_1^0-k_1^post31 == 0 /\ -__lengthofvisited^post31+__lengthofvisited^0 == 0 /\ -sourceflag^post31+sourceflag^0 == 0 /\ -min^post31+min^0 == 0 /\ nodecount^0-nodecount^post31 == 0), cost: 1 31: l18 -> l22 : __lengthofvisited^0'=__lengthofvisited^post32, destflag^0'=destflag^post32, edgecount^0'=edgecount^post32, h^0'=h^post32, i^0'=i^post32, j^0'=j^post32, k^0'=k^post32, k_1^0'=k_1^post32, min^0'=min^post32, nodecount^0'=nodecount^post32, sourceflag^0'=sourceflag^post32, (i^0-i^post32 == 0 /\ -__lengthofvisited^post32+__lengthofvisited^0 == 0 /\ h^post32 == 0 /\ -j^post32+j^0 == 0 /\ -destflag^post32+destflag^0 == 0 /\ -edgecount^post32+edgecount^0 == 0 /\ k_1^0-k_1^post32 == 0 /\ k^0-k^post32 == 0 /\ 1+k_1^0-edgecount^0 <= 0 /\ -min^post32+min^0 == 0 /\ nodecount^0-nodecount^post32 == 0 /\ -sourceflag^post32+sourceflag^0 == 0), cost: 1 19: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post20, destflag^0'=destflag^post20, edgecount^0'=edgecount^post20, h^0'=h^post20, i^0'=i^post20, j^0'=j^post20, k^0'=k^post20, k_1^0'=k_1^post20, min^0'=min^post20, nodecount^0'=nodecount^post20, sourceflag^0'=sourceflag^post20, (nodecount^0-nodecount^post20 == 0 /\ i^0-i^post20 == 0 /\ h^0-h^post20 == 0 /\ -sourceflag^post20+sourceflag^0 == 0 /\ -min^post20+min^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post20 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ k^0-k^post20 == 0 /\ -destflag^post20+destflag^0 == 0 /\ -j^post20+j^0 == 0 /\ k_1^0-k_1^post20 == 0), cost: 1 20: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post21, destflag^0'=destflag^post21, edgecount^0'=edgecount^post21, h^0'=h^post21, i^0'=i^post21, j^0'=j^post21, k^0'=k^post21, k_1^0'=k_1^post21, min^0'=min^post21, nodecount^0'=nodecount^post21, sourceflag^0'=sourceflag^post21, (i^0-i^post21 == 0 /\ destflag^0-destflag^post21 == 0 /\ -j^post21+j^0 == 0 /\ -h^post21+h^0 == 0 /\ -k^post21+k^0 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ -__lengthofvisited^post21+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post21 == 0 /\ -1+sourceflag^post21 == 0 /\ -min^post21+min^0 == 0 /\ nodecount^0-nodecount^post21 == 0), cost: 1 21: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post22, destflag^0'=destflag^post22, edgecount^0'=edgecount^post22, h^0'=h^post22, i^0'=i^post22, j^0'=j^post22, k^0'=k^post22, k_1^0'=k_1^post22, min^0'=min^post22, nodecount^0'=nodecount^post22, sourceflag^0'=sourceflag^post22, (i^0-i^post22 == 0 /\ -h^post22+h^0 == 0 /\ -j^post22+j^0 == 0 /\ k_1^0-k_1^post22 == 0 /\ destflag^0-destflag^post22 == 0 /\ -sourceflag^post22+sourceflag^0 == 0 /\ -__lengthofvisited^post22+__lengthofvisited^0 == 0 /\ -min^post22+min^0 == 0 /\ nodecount^0-nodecount^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0 /\ -k^post22+k^0 == 0), cost: 1 22: l20 -> l13 : __lengthofvisited^0'=__lengthofvisited^post23, destflag^0'=destflag^post23, edgecount^0'=edgecount^post23, h^0'=h^post23, i^0'=i^post23, j^0'=j^post23, k^0'=k^post23, k_1^0'=k_1^post23, min^0'=min^post23, nodecount^0'=nodecount^post23, sourceflag^0'=sourceflag^post23, (i^0-i^post23 == 0 /\ j^post23 == 0 /\ -edgecount^post23+edgecount^0 == 0 /\ -__lengthofvisited^post23+__lengthofvisited^0 == 0 /\ nodecount^0-j^0 <= 0 /\ k_1^0-k_1^post23 == 0 /\ -1+destflag^post23 == 0 /\ -min^post23+min^0 == 0 /\ -sourceflag^post23+sourceflag^0 == 0 /\ -h^post23+h^0 == 0 /\ k^0-k^post23 == 0 /\ nodecount^0-nodecount^post23 == 0), cost: 1 23: l20 -> l19 : __lengthofvisited^0'=__lengthofvisited^post24, destflag^0'=destflag^post24, edgecount^0'=edgecount^post24, h^0'=h^post24, i^0'=i^post24, j^0'=j^post24, k^0'=k^post24, k_1^0'=k_1^post24, min^0'=min^post24, nodecount^0'=nodecount^post24, sourceflag^0'=sourceflag^post24, (-edgecount^post24+edgecount^0 == 0 /\ -__lengthofvisited^post24+__lengthofvisited^0 == 0 /\ k^0-k^post24 == 0 /\ i^0-i^post24 == 0 /\ k_1^0-k_1^post24 == 0 /\ nodecount^0-nodecount^post24 == 0 /\ -min^post24+min^0 == 0 /\ h^0-h^post24 == 0 /\ destflag^0-destflag^post24 == 0 /\ -j^post24+j^0 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ -sourceflag^post24+sourceflag^0 == 0), cost: 1 24: l21 -> l22 : __lengthofvisited^0'=__lengthofvisited^post25, destflag^0'=destflag^post25, edgecount^0'=edgecount^post25, h^0'=h^post25, i^0'=i^post25, j^0'=j^post25, k^0'=k^post25, k_1^0'=k_1^post25, min^0'=min^post25, nodecount^0'=nodecount^post25, sourceflag^0'=sourceflag^post25, (-__lengthofvisited^post25+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post25 == 0 /\ -sourceflag^post25+sourceflag^0 == 0 /\ destflag^0-destflag^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ min^0-min^post25 == 0 /\ edgecount^0-edgecount^post25 == 0 /\ -k^post25+k^0 == 0 /\ -1+h^post25-h^0 == 0 /\ j^0-j^post25 == 0 /\ i^0-i^post25 == 0), cost: 1 27: l22 -> l24 : __lengthofvisited^0'=__lengthofvisited^post28, destflag^0'=destflag^post28, edgecount^0'=edgecount^post28, h^0'=h^post28, i^0'=i^post28, j^0'=j^post28, k^0'=k^post28, k_1^0'=k_1^post28, min^0'=min^post28, nodecount^0'=nodecount^post28, sourceflag^0'=sourceflag^post28, (k^0-k^post28 == 0 /\ k_1^0-k_1^post28 == 0 /\ -__lengthofvisited^post28+__lengthofvisited^0 == 0 /\ -edgecount^post28+edgecount^0 == 0 /\ i^0-i^post28 == 0 /\ -j^post28+j^0 == 0 /\ -sourceflag^post28+sourceflag^0 == 0 /\ nodecount^0-nodecount^post28 == 0 /\ h^0-h^post28 == 0 /\ -min^post28+min^0 == 0 /\ destflag^0-destflag^post28 == 0), cost: 1 25: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^post26, destflag^0'=destflag^post26, edgecount^0'=edgecount^post26, h^0'=h^post26, i^0'=i^post26, j^0'=j^post26, k^0'=k^post26, k_1^0'=k_1^post26, min^0'=min^post26, nodecount^0'=nodecount^post26, sourceflag^0'=sourceflag^post26, (-i^post26+i^0 == 0 /\ -j^post26+j^0 == 0 /\ -sourceflag^post26+sourceflag^0 == 0 /\ -k_1^post26+k_1^0 == 0 /\ min^post26-h^0 == 0 /\ nodecount^0-nodecount^post26 == 0 /\ __lengthofvisited^0-__lengthofvisited^post26 == 0 /\ -edgecount^post26+edgecount^0 == 0 /\ k^0-k^post26 == 0 /\ h^0-h^post26 == 0 /\ -destflag^post26+destflag^0 == 0), cost: 1 26: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^post27, destflag^0'=destflag^post27, edgecount^0'=edgecount^post27, h^0'=h^post27, i^0'=i^post27, j^0'=j^post27, k^0'=k^post27, k_1^0'=k_1^post27, min^0'=min^post27, nodecount^0'=nodecount^post27, sourceflag^0'=sourceflag^post27, (-sourceflag^post27+sourceflag^0 == 0 /\ -min^post27+min^0 == 0 /\ -__lengthofvisited^post27+__lengthofvisited^0 == 0 /\ destflag^0-destflag^post27 == 0 /\ -edgecount^post27+edgecount^0 == 0 /\ -k^post27+k^0 == 0 /\ nodecount^0-nodecount^post27 == 0 /\ j^0-j^post27 == 0 /\ k_1^0-k_1^post27 == 0 /\ -h^post27+h^0 == 0 /\ i^0-i^post27 == 0), cost: 1 28: l24 -> l17 : __lengthofvisited^0'=__lengthofvisited^post29, destflag^0'=destflag^post29, edgecount^0'=edgecount^post29, h^0'=h^post29, i^0'=i^post29, j^0'=j^post29, k^0'=k^post29, k_1^0'=k_1^post29, min^0'=min^post29, nodecount^0'=nodecount^post29, sourceflag^0'=sourceflag^post29, (j^post29 == 0 /\ destflag^0-destflag^post29 == 0 /\ k_1^0-k_1^post29 == 0 /\ -edgecount^post29+edgecount^0 == 0 /\ min^0-min^post29 == 0 /\ i^0-i^post29 == 0 /\ sourceflag^post29 == 0 /\ -k^post29+k^0 == 0 /\ -nodecount^post29+nodecount^0 == 0 /\ -h^post29+h^0 == 0 /\ -__lengthofvisited^post29+__lengthofvisited^0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1 29: l24 -> l23 : __lengthofvisited^0'=__lengthofvisited^post30, destflag^0'=destflag^post30, edgecount^0'=edgecount^post30, h^0'=h^post30, i^0'=i^post30, j^0'=j^post30, k^0'=k^post30, k_1^0'=k_1^post30, min^0'=min^post30, nodecount^0'=nodecount^post30, sourceflag^0'=sourceflag^post30, (__lengthofvisited^0-__lengthofvisited^post30 == 0 /\ nodecount^0-nodecount^post30 == 0 /\ -min^post30+min^0 == 0 /\ -destflag^post30+destflag^0 == 0 /\ -sourceflag^post30+sourceflag^0 == 0 /\ k^0-k^post30 == 0 /\ -j^post30+j^0 == 0 /\ i^0-i^post30 == 0 /\ 1+h^0-edgecount^0 <= 0 /\ h^0-h^post30 == 0 /\ k_1^0-k_1^post30 == 0 /\ -edgecount^post30+edgecount^0 == 0), cost: 1 35: l25 -> l10 : __lengthofvisited^0'=__lengthofvisited^post36, destflag^0'=destflag^post36, edgecount^0'=edgecount^post36, h^0'=h^post36, i^0'=i^post36, j^0'=j^post36, k^0'=k^post36, k_1^0'=k_1^post36, min^0'=min^post36, nodecount^0'=nodecount^post36, sourceflag^0'=sourceflag^post36, (-j^post36+j^0 == 0 /\ k^0-k^post36 == 0 /\ min^post36 == 0 /\ h^0-h^post36 == 0 /\ -sourceflag^post36+sourceflag^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post36 == 0 /\ -edgecount^post36+edgecount^0 == 0 /\ k_1^0-k_1^post36 == 0 /\ nodecount^0-nodecount^post36 == 0 /\ -destflag^post36+destflag^0 == 0 /\ i^post36 == 0), cost: 1 46: l28 -> l0 : __lengthofvisited^0'=__lengthofvisited^post45, destflag^0'=destflag^post45, edgecount^0'=edgecount^post45, h^0'=h^post45, i^0'=i^post45, j^0'=j^post45, k^0'=k^post45, k_1^0'=k_1^post45, min^0'=min^post45, nodecount^0'=nodecount^post45, sourceflag^0'=sourceflag^post45, (edgecount^0-edgecount^post46 == 0 /\ k_1^0-k_1^post46 == 0 /\ h^post46-h^post45 == 0 /\ -j^post45+j^post46 == 0 /\ -k^post46+k^0 == 0 /\ -1+i^post45 == 0 /\ min^0-min^post46 == 0 /\ -k_1^post45+k_1^post46 == 0 /\ k^post46-k^post45 == 0 /\ -__lengthofvisited^post46+__lengthofvisited^0 == 0 /\ -nodecount^post46+nodecount^0 == 0 /\ -min^post45+min^post46 == 0 /\ destflag^0-destflag^post46 == 0 /\ -destflag^post45+destflag^post46 == 0 /\ sourceflag^post46-sourceflag^post45 == 0 /\ __lengthofvisited^post45-edgecount^post46 == 0 /\ -sourceflag^post46+sourceflag^0 == 0 /\ nodecount^post46-nodecount^post45 == 0 /\ j^0-j^post46 == 0 /\ -h^post46+h^0 == 0 /\ -edgecount^post45+edgecount^post46 == 0 /\ i^0-i^post46 == 0), cost: 1 Eliminating location l27 by chaining: Applied chaining First rule: l28 -> l27 : __lengthofvisited^0'=__lengthofvisited^post46, destflag^0'=destflag^post46, edgecount^0'=edgecount^post46, h^0'=h^post46, i^0'=i^post46, j^0'=j^post46, k^0'=k^post46, k_1^0'=k_1^post46, min^0'=min^post46, nodecount^0'=nodecount^post46, sourceflag^0'=sourceflag^post46, (edgecount^0-edgecount^post46 == 0 /\ k_1^0-k_1^post46 == 0 /\ -k^post46+k^0 == 0 /\ min^0-min^post46 == 0 /\ -__lengthofvisited^post46+__lengthofvisited^0 == 0 /\ -nodecount^post46+nodecount^0 == 0 /\ destflag^0-destflag^post46 == 0 /\ -sourceflag^post46+sourceflag^0 == 0 /\ j^0-j^post46 == 0 /\ -h^post46+h^0 == 0 /\ i^0-i^post46 == 0), cost: 1 Second rule: l27 -> l0 : __lengthofvisited^0'=__lengthofvisited^post45, destflag^0'=destflag^post45, edgecount^0'=edgecount^post45, h^0'=h^post45, i^0'=i^post45, j^0'=j^post45, k^0'=k^post45, k_1^0'=k_1^post45, min^0'=min^post45, nodecount^0'=nodecount^post45, sourceflag^0'=sourceflag^post45, (sourceflag^0-sourceflag^post45 == 0 /\ -1+i^post45 == 0 /\ -k_1^post45+k_1^0 == 0 /\ k^0-k^post45 == 0 /\ nodecount^0-nodecount^post45 == 0 /\ -j^post45+j^0 == 0 /\ __lengthofvisited^post45-edgecount^0 == 0 /\ h^0-h^post45 == 0 /\ -min^post45+min^0 == 0 /\ -destflag^post45+destflag^0 == 0 /\ -edgecount^post45+edgecount^0 == 0), cost: 1 New rule: l28 -> l0 : __lengthofvisited^0'=__lengthofvisited^post45, destflag^0'=destflag^post45, edgecount^0'=edgecount^post45, h^0'=h^post45, i^0'=i^post45, j^0'=j^post45, k^0'=k^post45, k_1^0'=k_1^post45, min^0'=min^post45, nodecount^0'=nodecount^post45, sourceflag^0'=sourceflag^post45, (edgecount^0-edgecount^post46 == 0 /\ k_1^0-k_1^post46 == 0 /\ h^post46-h^post45 == 0 /\ -j^post45+j^post46 == 0 /\ -k^post46+k^0 == 0 /\ -1+i^post45 == 0 /\ min^0-min^post46 == 0 /\ -k_1^post45+k_1^post46 == 0 /\ k^post46-k^post45 == 0 /\ -__lengthofvisited^post46+__lengthofvisited^0 == 0 /\ -nodecount^post46+nodecount^0 == 0 /\ -min^post45+min^post46 == 0 /\ destflag^0-destflag^post46 == 0 /\ -destflag^post45+destflag^post46 == 0 /\ sourceflag^post46-sourceflag^post45 == 0 /\ __lengthofvisited^post45-edgecount^post46 == 0 /\ -sourceflag^post46+sourceflag^0 == 0 /\ nodecount^post46-nodecount^post45 == 0 /\ j^0-j^post46 == 0 /\ -h^post46+h^0 == 0 /\ -edgecount^post45+edgecount^post46 == 0 /\ i^0-i^post46 == 0), cost: 1 Applied deletion Removed the following rules: 44 45 Simplified Transitions Start location: l28 Program variables: __lengthofvisited^0 destflag^0 edgecount^0 h^0 i^0 j^0 k^0 k_1^0 min^0 nodecount^0 sourceflag^0 47: l0 -> l1 : T, cost: 1 89: l1 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 90: l1 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1 48: l2 -> l3 : T, cost: 1 86: l3 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 1 87: l3 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 1 49: l4 -> l5 : T, cost: 1 83: l5 -> l26 : (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 84: l5 -> l25 : nodecount^0-k^0 <= 0, cost: 1 85: l5 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 1 50: l6 -> l7 : k_1^0'=1+k_1^0, T, cost: 1 65: l7 -> l18 : T, cost: 1 51: l8 -> l6 : 1-destflag^0 <= 0, cost: 1 52: l8 -> l6 : 1+destflag^0 <= 0, cost: 1 53: l8 -> l6 : (destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 54: l9 -> l6 : 1-sourceflag^0 <= 0, cost: 1 55: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1 56: l9 -> l8 : (-sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 57: l10 -> l11 : T, cost: 1 79: l11 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 1 80: l11 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 1 58: l12 -> l13 : j^0'=1+j^0, T, cost: 1 88: l13 -> l15 : T, cost: 1 59: l14 -> l12 : T, cost: 1 60: l14 -> l12 : destflag^0'=0, T, cost: 1 61: l14 -> l12 : T, cost: 1 62: l15 -> l9 : nodecount^0-j^0 <= 0, cost: 1 63: l15 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 1 64: l16 -> l17 : j^0'=1+j^0, T, cost: 1 81: l17 -> l20 : T, cost: 1 77: l18 -> l4 : k^0'=1+k^0, -k_1^0+edgecount^0 <= 0, cost: 1 78: l18 -> l22 : h^0'=0, 1+k_1^0-edgecount^0 <= 0, cost: 1 66: l19 -> l16 : T, cost: 1 67: l19 -> l16 : sourceflag^0'=1, T, cost: 1 68: l19 -> l16 : T, cost: 1 69: l20 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 1 70: l20 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 1 71: l21 -> l22 : h^0'=1+h^0, T, cost: 1 74: l22 -> l24 : T, cost: 1 72: l23 -> l21 : min^0'=h^0, T, cost: 1 73: l23 -> l21 : T, cost: 1 75: l24 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1 76: l24 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 1 82: l25 -> l10 : i^0'=0, min^0'=0, T, cost: 1 91: l28 -> l0 : __lengthofvisited^0'=edgecount^0, i^0'=1, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __lengthofvisited^0'=__lengthofvisited^post1, destflag^0'=destflag^post1, edgecount^0'=edgecount^post1, h^0'=h^post1, i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, k_1^0'=k_1^post1, min^0'=min^post1, nodecount^0'=nodecount^post1, sourceflag^0'=sourceflag^post1, (__lengthofvisited^0-__lengthofvisited^post1 == 0 /\ nodecount^0-nodecount^post1 == 0 /\ -j^post1+j^0 == 0 /\ -min^post1+min^0 == 0 /\ -destflag^post1+destflag^0 == 0 /\ k^0-k^post1 == 0 /\ -sourceflag^post1+sourceflag^0 == 0 /\ h^0-h^post1 == 0 /\ k_1^0-k_1^post1 == 0 /\ -i^post1+i^0 == 0 /\ -edgecount^post1+edgecount^0 == 0), cost: 1 New rule: l0 -> l1 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality __lengthofvisited^post1 = __lengthofvisited^0 propagated equality nodecount^post1 = nodecount^0 propagated equality j^post1 = j^0 propagated equality min^post1 = min^0 propagated equality destflag^post1 = destflag^0 propagated equality k^post1 = k^0 propagated equality sourceflag^post1 = sourceflag^0 propagated equality h^post1 = h^0 propagated equality k_1^post1 = k_1^0 propagated equality i^post1 = i^0 propagated equality edgecount^post1 = edgecount^0 Simplified Guard Original rule: l0 -> l1 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l0 -> l1 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : __lengthofvisited^0'=__lengthofvisited^post2, destflag^0'=destflag^post2, edgecount^0'=edgecount^post2, h^0'=h^post2, i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, k_1^0'=k_1^post2, min^0'=min^post2, nodecount^0'=nodecount^post2, sourceflag^0'=sourceflag^post2, (i^0-i^post2 == 0 /\ -h^post2+h^0 == 0 /\ -j^post2+j^0 == 0 /\ k_1^0-k_1^post2 == 0 /\ destflag^0-destflag^post2 == 0 /\ -k^post2+k^0 == 0 /\ -__lengthofvisited^post2+__lengthofvisited^0 == 0 /\ -min^post2+min^0 == 0 /\ -sourceflag^post2+sourceflag^0 == 0 /\ -edgecount^post2+edgecount^0 == 0 /\ nodecount^0-nodecount^post2 == 0), cost: 1 New rule: l2 -> l3 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality i^post2 = i^0 propagated equality h^post2 = h^0 propagated equality j^post2 = j^0 propagated equality k_1^post2 = k_1^0 propagated equality destflag^post2 = destflag^0 propagated equality k^post2 = k^0 propagated equality __lengthofvisited^post2 = __lengthofvisited^0 propagated equality min^post2 = min^0 propagated equality sourceflag^post2 = sourceflag^0 propagated equality edgecount^post2 = edgecount^0 propagated equality nodecount^post2 = nodecount^0 Simplified Guard Original rule: l2 -> l3 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l2 -> l3 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l2 -> l3 : T, cost: 1 Propagated Equalities Original rule: l4 -> l5 : __lengthofvisited^0'=__lengthofvisited^post3, destflag^0'=destflag^post3, edgecount^0'=edgecount^post3, h^0'=h^post3, i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, k_1^0'=k_1^post3, min^0'=min^post3, nodecount^0'=nodecount^post3, sourceflag^0'=sourceflag^post3, (i^0-i^post3 == 0 /\ h^0-h^post3 == 0 /\ -j^post3+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post3 == 0 /\ destflag^0-destflag^post3 == 0 /\ k_1^0-k_1^post3 == 0 /\ -edgecount^post3+edgecount^0 == 0 /\ -sourceflag^post3+sourceflag^0 == 0 /\ -min^post3+min^0 == 0 /\ nodecount^0-nodecount^post3 == 0 /\ k^0-k^post3 == 0), cost: 1 New rule: l4 -> l5 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality i^post3 = i^0 propagated equality h^post3 = h^0 propagated equality j^post3 = j^0 propagated equality __lengthofvisited^post3 = __lengthofvisited^0 propagated equality destflag^post3 = destflag^0 propagated equality k_1^post3 = k_1^0 propagated equality edgecount^post3 = edgecount^0 propagated equality sourceflag^post3 = sourceflag^0 propagated equality min^post3 = min^0 propagated equality nodecount^post3 = nodecount^0 propagated equality k^post3 = k^0 Simplified Guard Original rule: l4 -> l5 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l4 -> l5 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l5 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l4 -> l5 : T, cost: 1 Propagated Equalities Original rule: l6 -> l7 : __lengthofvisited^0'=__lengthofvisited^post4, destflag^0'=destflag^post4, edgecount^0'=edgecount^post4, h^0'=h^post4, i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, k_1^0'=k_1^post4, min^0'=min^post4, nodecount^0'=nodecount^post4, sourceflag^0'=sourceflag^post4, (-edgecount^post4+edgecount^0 == 0 /\ -h^post4+h^0 == 0 /\ -__lengthofvisited^post4+__lengthofvisited^0 == 0 /\ -nodecount^post4+nodecount^0 == 0 /\ min^0-min^post4 == 0 /\ i^0-i^post4 == 0 /\ j^0-j^post4 == 0 /\ destflag^0-destflag^post4 == 0 /\ -1-k_1^0+k_1^post4 == 0 /\ -sourceflag^post4+sourceflag^0 == 0 /\ -k^post4+k^0 == 0), cost: 1 New rule: l6 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=1+k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality edgecount^post4 = edgecount^0 propagated equality h^post4 = h^0 propagated equality __lengthofvisited^post4 = __lengthofvisited^0 propagated equality nodecount^post4 = nodecount^0 propagated equality min^post4 = min^0 propagated equality i^post4 = i^0 propagated equality j^post4 = j^0 propagated equality destflag^post4 = destflag^0 propagated equality k_1^post4 = 1+k_1^0 propagated equality sourceflag^post4 = sourceflag^0 propagated equality k^post4 = k^0 Simplified Guard Original rule: l6 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=1+k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l6 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=1+k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=1+k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l6 -> l7 : k_1^0'=1+k_1^0, T, cost: 1 Propagated Equalities Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post5, destflag^0'=destflag^post5, edgecount^0'=edgecount^post5, h^0'=h^post5, i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, k_1^0'=k_1^post5, min^0'=min^post5, nodecount^0'=nodecount^post5, sourceflag^0'=sourceflag^post5, (h^0-h^post5 == 0 /\ nodecount^0-nodecount^post5 == 0 /\ -edgecount^post5+edgecount^0 == 0 /\ -destflag^post5+destflag^0 == 0 /\ -i^post5+i^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post5 == 0 /\ -min^post5+min^0 == 0 /\ 1-destflag^0 <= 0 /\ k^0-k^post5 == 0 /\ -j^post5+j^0 == 0 /\ -sourceflag^post5+sourceflag^0 == 0 /\ k_1^0-k_1^post5 == 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-destflag^0 <= 0), cost: 1 propagated equality h^post5 = h^0 propagated equality nodecount^post5 = nodecount^0 propagated equality edgecount^post5 = edgecount^0 propagated equality destflag^post5 = destflag^0 propagated equality i^post5 = i^0 propagated equality __lengthofvisited^post5 = __lengthofvisited^0 propagated equality min^post5 = min^0 propagated equality k^post5 = k^0 propagated equality j^post5 = j^0 propagated equality sourceflag^post5 = sourceflag^0 propagated equality k_1^post5 = k_1^0 Simplified Guard Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-destflag^0 <= 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-destflag^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-destflag^0 <= 0, cost: 1 New rule: l8 -> l6 : 1-destflag^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post6, destflag^0'=destflag^post6, edgecount^0'=edgecount^post6, h^0'=h^post6, i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, k_1^0'=k_1^post6, min^0'=min^post6, nodecount^0'=nodecount^post6, sourceflag^0'=sourceflag^post6, (destflag^0-destflag^post6 == 0 /\ min^0-min^post6 == 0 /\ edgecount^0-edgecount^post6 == 0 /\ -h^post6+h^0 == 0 /\ -__lengthofvisited^post6+__lengthofvisited^0 == 0 /\ 1+destflag^0 <= 0 /\ -k^post6+k^0 == 0 /\ -sourceflag^post6+sourceflag^0 == 0 /\ j^0-j^post6 == 0 /\ i^0-i^post6 == 0 /\ -nodecount^post6+nodecount^0 == 0 /\ k_1^0-k_1^post6 == 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+destflag^0 <= 0), cost: 1 propagated equality destflag^post6 = destflag^0 propagated equality min^post6 = min^0 propagated equality edgecount^post6 = edgecount^0 propagated equality h^post6 = h^0 propagated equality __lengthofvisited^post6 = __lengthofvisited^0 propagated equality k^post6 = k^0 propagated equality sourceflag^post6 = sourceflag^0 propagated equality j^post6 = j^0 propagated equality i^post6 = i^0 propagated equality nodecount^post6 = nodecount^0 propagated equality k_1^post6 = k_1^0 Simplified Guard Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+destflag^0 <= 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+destflag^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+destflag^0 <= 0, cost: 1 New rule: l8 -> l6 : 1+destflag^0 <= 0, cost: 1 made implied equalities explicit Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post7, destflag^0'=destflag^post7, edgecount^0'=edgecount^post7, h^0'=h^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, k_1^0'=k_1^post7, min^0'=min^post7, nodecount^0'=nodecount^post7, sourceflag^0'=sourceflag^post7, (-j^post7+j^0 == 0 /\ -min^post7+min^0 == 0 /\ k^0-k^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ h^0-h^post7 == 0 /\ i^0-i^post7 == 0 /\ destflag^0 <= 0 /\ -edgecount^post7+edgecount^0 == 0 /\ k_1^0-k_1^post7 == 0 /\ -destflag^post7+destflag^0 == 0 /\ -destflag^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post7 == 0 /\ nodecount^0-nodecount^post7 == 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post7, destflag^0'=destflag^post7, edgecount^0'=edgecount^post7, h^0'=h^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, k_1^0'=k_1^post7, min^0'=min^post7, nodecount^0'=nodecount^post7, sourceflag^0'=sourceflag^post7, (-j^post7+j^0 == 0 /\ -min^post7+min^0 == 0 /\ k^0-k^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ h^0-h^post7 == 0 /\ i^0-i^post7 == 0 /\ destflag^0 <= 0 /\ destflag^0 == 0 /\ -edgecount^post7+edgecount^0 == 0 /\ k_1^0-k_1^post7 == 0 /\ -destflag^post7+destflag^0 == 0 /\ -destflag^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post7 == 0 /\ nodecount^0-nodecount^post7 == 0), cost: 1 Propagated Equalities Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^post7, destflag^0'=destflag^post7, edgecount^0'=edgecount^post7, h^0'=h^post7, i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, k_1^0'=k_1^post7, min^0'=min^post7, nodecount^0'=nodecount^post7, sourceflag^0'=sourceflag^post7, (-j^post7+j^0 == 0 /\ -min^post7+min^0 == 0 /\ k^0-k^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ h^0-h^post7 == 0 /\ i^0-i^post7 == 0 /\ destflag^0 <= 0 /\ destflag^0 == 0 /\ -edgecount^post7+edgecount^0 == 0 /\ k_1^0-k_1^post7 == 0 /\ -destflag^post7+destflag^0 == 0 /\ -destflag^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post7 == 0 /\ nodecount^0-nodecount^post7 == 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 propagated equality j^post7 = j^0 propagated equality min^post7 = min^0 propagated equality k^post7 = k^0 propagated equality sourceflag^post7 = sourceflag^0 propagated equality h^post7 = h^0 propagated equality i^post7 = i^0 propagated equality edgecount^post7 = edgecount^0 propagated equality k_1^post7 = k_1^0 propagated equality destflag^post7 = destflag^0 propagated equality __lengthofvisited^post7 = __lengthofvisited^0 propagated equality nodecount^post7 = nodecount^0 Simplified Guard Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 made implied equalities explicit Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 New rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l8 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 New rule: l8 -> l6 : (destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 Propagated Equalities Original rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^post8, destflag^0'=destflag^post8, edgecount^0'=edgecount^post8, h^0'=h^post8, i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, k_1^0'=k_1^post8, min^0'=min^post8, nodecount^0'=nodecount^post8, sourceflag^0'=sourceflag^post8, (-sourceflag^post8+sourceflag^0 == 0 /\ k_1^0-k_1^post8 == 0 /\ k^0-k^post8 == 0 /\ -__lengthofvisited^post8+__lengthofvisited^0 == 0 /\ i^0-i^post8 == 0 /\ -edgecount^post8+edgecount^0 == 0 /\ h^0-h^post8 == 0 /\ -min^post8+min^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ -j^post8+j^0 == 0 /\ 1-sourceflag^0 <= 0 /\ destflag^0-destflag^post8 == 0), cost: 1 New rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-sourceflag^0 <= 0), cost: 1 propagated equality sourceflag^post8 = sourceflag^0 propagated equality k_1^post8 = k_1^0 propagated equality k^post8 = k^0 propagated equality __lengthofvisited^post8 = __lengthofvisited^0 propagated equality i^post8 = i^0 propagated equality edgecount^post8 = edgecount^0 propagated equality h^post8 = h^0 propagated equality min^post8 = min^0 propagated equality nodecount^post8 = nodecount^0 propagated equality j^post8 = j^0 propagated equality destflag^post8 = destflag^0 Simplified Guard Original rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-sourceflag^0 <= 0), cost: 1 New rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-sourceflag^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-sourceflag^0 <= 0, cost: 1 New rule: l9 -> l6 : 1-sourceflag^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^post9, destflag^0'=destflag^post9, edgecount^0'=edgecount^post9, h^0'=h^post9, i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, k_1^0'=k_1^post9, min^0'=min^post9, nodecount^0'=nodecount^post9, sourceflag^0'=sourceflag^post9, (1+sourceflag^0 <= 0 /\ k^0-k^post9 == 0 /\ -min^post9+min^0 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ k_1^0-k_1^post9 == 0 /\ -__lengthofvisited^post9+__lengthofvisited^0 == 0 /\ i^0-i^post9 == 0 /\ -nodecount^post9+nodecount^0 == 0 /\ -sourceflag^post9+sourceflag^0 == 0 /\ destflag^0-destflag^post9 == 0 /\ -j^post9+j^0 == 0 /\ -h^post9+h^0 == 0), cost: 1 New rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+sourceflag^0 <= 0), cost: 1 propagated equality k^post9 = k^0 propagated equality min^post9 = min^0 propagated equality edgecount^post9 = edgecount^0 propagated equality k_1^post9 = k_1^0 propagated equality __lengthofvisited^post9 = __lengthofvisited^0 propagated equality i^post9 = i^0 propagated equality nodecount^post9 = nodecount^0 propagated equality sourceflag^post9 = sourceflag^0 propagated equality destflag^post9 = destflag^0 propagated equality j^post9 = j^0 propagated equality h^post9 = h^0 Simplified Guard Original rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+sourceflag^0 <= 0), cost: 1 New rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+sourceflag^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l6 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+sourceflag^0 <= 0, cost: 1 New rule: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1 made implied equalities explicit Original rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^post10, destflag^0'=destflag^post10, edgecount^0'=edgecount^post10, h^0'=h^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, k_1^0'=k_1^post10, min^0'=min^post10, nodecount^0'=nodecount^post10, sourceflag^0'=sourceflag^post10, (i^0-i^post10 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -destflag^post10+destflag^0 == 0 /\ -k^post10+k^0 == 0 /\ -sourceflag^post10+sourceflag^0 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ k_1^0-k_1^post10 == 0 /\ -sourceflag^0 <= 0 /\ -h^post10+h^0 == 0 /\ j^0-j^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0 <= 0), cost: 1 New rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^post10, destflag^0'=destflag^post10, edgecount^0'=edgecount^post10, h^0'=h^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, k_1^0'=k_1^post10, min^0'=min^post10, nodecount^0'=nodecount^post10, sourceflag^0'=sourceflag^post10, (i^0-i^post10 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -destflag^post10+destflag^0 == 0 /\ -k^post10+k^0 == 0 /\ -sourceflag^post10+sourceflag^0 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ k_1^0-k_1^post10 == 0 /\ -sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ -h^post10+h^0 == 0 /\ j^0-j^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0 <= 0), cost: 1 Propagated Equalities Original rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^post10, destflag^0'=destflag^post10, edgecount^0'=edgecount^post10, h^0'=h^post10, i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, k_1^0'=k_1^post10, min^0'=min^post10, nodecount^0'=nodecount^post10, sourceflag^0'=sourceflag^post10, (i^0-i^post10 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -destflag^post10+destflag^0 == 0 /\ -k^post10+k^0 == 0 /\ -sourceflag^post10+sourceflag^0 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ k_1^0-k_1^post10 == 0 /\ -sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ -h^post10+h^0 == 0 /\ j^0-j^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0 <= 0), cost: 1 New rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 propagated equality i^post10 = i^0 propagated equality __lengthofvisited^post10 = __lengthofvisited^0 propagated equality destflag^post10 = destflag^0 propagated equality k^post10 = k^0 propagated equality sourceflag^post10 = sourceflag^0 propagated equality nodecount^post10 = nodecount^0 propagated equality edgecount^post10 = edgecount^0 propagated equality k_1^post10 = k_1^0 propagated equality h^post10 = h^0 propagated equality j^post10 = j^0 propagated equality min^post10 = min^0 Simplified Guard Original rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 New rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 made implied equalities explicit Original rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 New rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l9 -> l8 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 New rule: l9 -> l8 : (-sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 Propagated Equalities Original rule: l10 -> l11 : __lengthofvisited^0'=__lengthofvisited^post11, destflag^0'=destflag^post11, edgecount^0'=edgecount^post11, h^0'=h^post11, i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, k_1^0'=k_1^post11, min^0'=min^post11, nodecount^0'=nodecount^post11, sourceflag^0'=sourceflag^post11, (nodecount^0-nodecount^post11 == 0 /\ i^0-i^post11 == 0 /\ h^0-h^post11 == 0 /\ -j^post11+j^0 == 0 /\ -min^post11+min^0 == 0 /\ k_1^0-k_1^post11 == 0 /\ destflag^0-destflag^post11 == 0 /\ -sourceflag^post11+sourceflag^0 == 0 /\ -__lengthofvisited^post11+__lengthofvisited^0 == 0 /\ -edgecount^post11+edgecount^0 == 0 /\ k^0-k^post11 == 0), cost: 1 New rule: l10 -> l11 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality nodecount^post11 = nodecount^0 propagated equality i^post11 = i^0 propagated equality h^post11 = h^0 propagated equality j^post11 = j^0 propagated equality min^post11 = min^0 propagated equality k_1^post11 = k_1^0 propagated equality destflag^post11 = destflag^0 propagated equality sourceflag^post11 = sourceflag^0 propagated equality __lengthofvisited^post11 = __lengthofvisited^0 propagated equality edgecount^post11 = edgecount^0 propagated equality k^post11 = k^0 Simplified Guard Original rule: l10 -> l11 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l10 -> l11 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l10 -> l11 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l10 -> l11 : T, cost: 1 Propagated Equalities Original rule: l12 -> l13 : __lengthofvisited^0'=__lengthofvisited^post12, destflag^0'=destflag^post12, edgecount^0'=edgecount^post12, h^0'=h^post12, i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, k_1^0'=k_1^post12, min^0'=min^post12, nodecount^0'=nodecount^post12, sourceflag^0'=sourceflag^post12, (i^0-i^post12 == 0 /\ -h^post12+h^0 == 0 /\ k_1^0-k_1^post12 == 0 /\ destflag^0-destflag^post12 == 0 /\ -__lengthofvisited^post12+__lengthofvisited^0 == 0 /\ -min^post12+min^0 == 0 /\ -sourceflag^post12+sourceflag^0 == 0 /\ -edgecount^post12+edgecount^0 == 0 /\ -1+j^post12-j^0 == 0 /\ nodecount^0-nodecount^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 New rule: l12 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality i^post12 = i^0 propagated equality h^post12 = h^0 propagated equality k_1^post12 = k_1^0 propagated equality destflag^post12 = destflag^0 propagated equality __lengthofvisited^post12 = __lengthofvisited^0 propagated equality min^post12 = min^0 propagated equality sourceflag^post12 = sourceflag^0 propagated equality edgecount^post12 = edgecount^0 propagated equality j^post12 = 1+j^0 propagated equality nodecount^post12 = nodecount^0 propagated equality k^post12 = k^0 Simplified Guard Original rule: l12 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l12 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l12 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l12 -> l13 : j^0'=1+j^0, T, cost: 1 Propagated Equalities Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post13, destflag^0'=destflag^post13, edgecount^0'=edgecount^post13, h^0'=h^post13, i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, k_1^0'=k_1^post13, min^0'=min^post13, nodecount^0'=nodecount^post13, sourceflag^0'=sourceflag^post13, (k_1^0-k_1^post13 == 0 /\ -__lengthofvisited^post13+__lengthofvisited^0 == 0 /\ min^0-min^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0 /\ destflag^0-destflag^post13 == 0 /\ i^0-i^post13 == 0 /\ -j^post13+j^0 == 0 /\ -edgecount^post13+edgecount^0 == 0 /\ -k^post13+k^0 == 0 /\ -h^post13+h^0 == 0 /\ -sourceflag^post13+sourceflag^0 == 0), cost: 1 New rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality k_1^post13 = k_1^0 propagated equality __lengthofvisited^post13 = __lengthofvisited^0 propagated equality min^post13 = min^0 propagated equality nodecount^post13 = nodecount^0 propagated equality destflag^post13 = destflag^0 propagated equality i^post13 = i^0 propagated equality j^post13 = j^0 propagated equality edgecount^post13 = edgecount^0 propagated equality k^post13 = k^0 propagated equality h^post13 = h^0 propagated equality sourceflag^post13 = sourceflag^0 Simplified Guard Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l14 -> l12 : T, cost: 1 Propagated Equalities Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post14, destflag^0'=destflag^post14, edgecount^0'=edgecount^post14, h^0'=h^post14, i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, k_1^0'=k_1^post14, min^0'=min^post14, nodecount^0'=nodecount^post14, sourceflag^0'=sourceflag^post14, (-i^post14+i^0 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ destflag^post14 == 0 /\ -j^post14+j^0 == 0 /\ k_1^0-k_1^post14 == 0 /\ __lengthofvisited^0-__lengthofvisited^post14 == 0 /\ nodecount^0-nodecount^post14 == 0 /\ k^0-k^post14 == 0 /\ -min^post14+min^0 == 0 /\ h^0-h^post14 == 0 /\ -sourceflag^post14+sourceflag^0 == 0), cost: 1 New rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality i^post14 = i^0 propagated equality edgecount^post14 = edgecount^0 propagated equality destflag^post14 = 0 propagated equality j^post14 = j^0 propagated equality k_1^post14 = k_1^0 propagated equality __lengthofvisited^post14 = __lengthofvisited^0 propagated equality nodecount^post14 = nodecount^0 propagated equality k^post14 = k^0 propagated equality min^post14 = min^0 propagated equality h^post14 = h^0 propagated equality sourceflag^post14 = sourceflag^0 Simplified Guard Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l14 -> l12 : destflag^0'=0, T, cost: 1 Propagated Equalities Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^post15, destflag^0'=destflag^post15, edgecount^0'=edgecount^post15, h^0'=h^post15, i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, k_1^0'=k_1^post15, min^0'=min^post15, nodecount^0'=nodecount^post15, sourceflag^0'=sourceflag^post15, (-k^post15+k^0 == 0 /\ -__lengthofvisited^post15+__lengthofvisited^0 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ destflag^0-destflag^post15 == 0 /\ k_1^0-k_1^post15 == 0 /\ -h^post15+h^0 == 0 /\ -sourceflag^post15+sourceflag^0 == 0 /\ min^0-min^post15 == 0 /\ edgecount^0-edgecount^post15 == 0 /\ j^0-j^post15 == 0 /\ i^0-i^post15 == 0), cost: 1 New rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality k^post15 = k^0 propagated equality __lengthofvisited^post15 = __lengthofvisited^0 propagated equality nodecount^post15 = nodecount^0 propagated equality destflag^post15 = destflag^0 propagated equality k_1^post15 = k_1^0 propagated equality h^post15 = h^0 propagated equality sourceflag^post15 = sourceflag^0 propagated equality min^post15 = min^0 propagated equality edgecount^post15 = edgecount^0 propagated equality j^post15 = j^0 propagated equality i^post15 = i^0 Simplified Guard Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l14 -> l12 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l14 -> l12 : T, cost: 1 Propagated Equalities Original rule: l15 -> l9 : __lengthofvisited^0'=__lengthofvisited^post16, destflag^0'=destflag^post16, edgecount^0'=edgecount^post16, h^0'=h^post16, i^0'=i^post16, j^0'=j^post16, k^0'=k^post16, k_1^0'=k_1^post16, min^0'=min^post16, nodecount^0'=nodecount^post16, sourceflag^0'=sourceflag^post16, (k^0-k^post16 == 0 /\ -sourceflag^post16+sourceflag^0 == 0 /\ -edgecount^post16+edgecount^0 == 0 /\ -min^post16+min^0 == 0 /\ -h^post16+h^0 == 0 /\ -j^post16+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post16 == 0 /\ i^0-i^post16 == 0 /\ k_1^0-k_1^post16 == 0 /\ nodecount^0-j^0 <= 0 /\ destflag^0-destflag^post16 == 0 /\ nodecount^0-nodecount^post16 == 0), cost: 1 New rule: l15 -> l9 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ nodecount^0-j^0 <= 0), cost: 1 propagated equality k^post16 = k^0 propagated equality sourceflag^post16 = sourceflag^0 propagated equality edgecount^post16 = edgecount^0 propagated equality min^post16 = min^0 propagated equality h^post16 = h^0 propagated equality j^post16 = j^0 propagated equality __lengthofvisited^post16 = __lengthofvisited^0 propagated equality i^post16 = i^0 propagated equality k_1^post16 = k_1^0 propagated equality destflag^post16 = destflag^0 propagated equality nodecount^post16 = nodecount^0 Simplified Guard Original rule: l15 -> l9 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ nodecount^0-j^0 <= 0), cost: 1 New rule: l15 -> l9 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, nodecount^0-j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l15 -> l9 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, nodecount^0-j^0 <= 0, cost: 1 New rule: l15 -> l9 : nodecount^0-j^0 <= 0, cost: 1 Propagated Equalities Original rule: l15 -> l14 : __lengthofvisited^0'=__lengthofvisited^post17, destflag^0'=destflag^post17, edgecount^0'=edgecount^post17, h^0'=h^post17, i^0'=i^post17, j^0'=j^post17, k^0'=k^post17, k_1^0'=k_1^post17, min^0'=min^post17, nodecount^0'=nodecount^post17, sourceflag^0'=sourceflag^post17, (-min^post17+min^0 == 0 /\ k^0-k^post17 == 0 /\ -sourceflag^post17+sourceflag^0 == 0 /\ -__lengthofvisited^post17+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0 /\ i^0-i^post17 == 0 /\ -j^post17+j^0 == 0 /\ -h^post17+h^0 == 0 /\ nodecount^0-nodecount^post17 == 0 /\ destflag^0-destflag^post17 == 0 /\ 1-nodecount^0+j^0 <= 0), cost: 1 New rule: l15 -> l14 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-nodecount^0+j^0 <= 0), cost: 1 propagated equality min^post17 = min^0 propagated equality k^post17 = k^0 propagated equality sourceflag^post17 = sourceflag^0 propagated equality __lengthofvisited^post17 = __lengthofvisited^0 propagated equality k_1^post17 = k_1^0 propagated equality edgecount^post17 = edgecount^0 propagated equality i^post17 = i^0 propagated equality j^post17 = j^0 propagated equality h^post17 = h^0 propagated equality nodecount^post17 = nodecount^0 propagated equality destflag^post17 = destflag^0 Simplified Guard Original rule: l15 -> l14 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-nodecount^0+j^0 <= 0), cost: 1 New rule: l15 -> l14 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-nodecount^0+j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l15 -> l14 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-nodecount^0+j^0 <= 0, cost: 1 New rule: l15 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 1 Propagated Equalities Original rule: l16 -> l17 : __lengthofvisited^0'=__lengthofvisited^post18, destflag^0'=destflag^post18, edgecount^0'=edgecount^post18, h^0'=h^post18, i^0'=i^post18, j^0'=j^post18, k^0'=k^post18, k_1^0'=k_1^post18, min^0'=min^post18, nodecount^0'=nodecount^post18, sourceflag^0'=sourceflag^post18, (-1+j^post18-j^0 == 0 /\ k_1^0-k_1^post18 == 0 /\ k^0-k^post18 == 0 /\ -edgecount^post18+edgecount^0 == 0 /\ i^0-i^post18 == 0 /\ -__lengthofvisited^post18+__lengthofvisited^0 == 0 /\ nodecount^0-nodecount^post18 == 0 /\ h^0-h^post18 == 0 /\ -sourceflag^post18+sourceflag^0 == 0 /\ -min^post18+min^0 == 0 /\ destflag^0-destflag^post18 == 0), cost: 1 New rule: l16 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality j^post18 = 1+j^0 propagated equality k_1^post18 = k_1^0 propagated equality k^post18 = k^0 propagated equality edgecount^post18 = edgecount^0 propagated equality i^post18 = i^0 propagated equality __lengthofvisited^post18 = __lengthofvisited^0 propagated equality nodecount^post18 = nodecount^0 propagated equality h^post18 = h^0 propagated equality sourceflag^post18 = sourceflag^0 propagated equality min^post18 = min^0 propagated equality destflag^post18 = destflag^0 Simplified Guard Original rule: l16 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l16 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l16 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=1+j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l16 -> l17 : j^0'=1+j^0, T, cost: 1 Propagated Equalities Original rule: l7 -> l18 : __lengthofvisited^0'=__lengthofvisited^post19, destflag^0'=destflag^post19, edgecount^0'=edgecount^post19, h^0'=h^post19, i^0'=i^post19, j^0'=j^post19, k^0'=k^post19, k_1^0'=k_1^post19, min^0'=min^post19, nodecount^0'=nodecount^post19, sourceflag^0'=sourceflag^post19, (min^0-min^post19 == 0 /\ edgecount^0-edgecount^post19 == 0 /\ -__lengthofvisited^post19+__lengthofvisited^0 == 0 /\ -sourceflag^post19+sourceflag^0 == 0 /\ destflag^0-destflag^post19 == 0 /\ -k^post19+k^0 == 0 /\ -h^post19+h^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ j^0-j^post19 == 0 /\ i^0-i^post19 == 0 /\ k_1^0-k_1^post19 == 0), cost: 1 New rule: l7 -> l18 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality min^post19 = min^0 propagated equality edgecount^post19 = edgecount^0 propagated equality __lengthofvisited^post19 = __lengthofvisited^0 propagated equality sourceflag^post19 = sourceflag^0 propagated equality destflag^post19 = destflag^0 propagated equality k^post19 = k^0 propagated equality h^post19 = h^0 propagated equality nodecount^post19 = nodecount^0 propagated equality j^post19 = j^0 propagated equality i^post19 = i^0 propagated equality k_1^post19 = k_1^0 Simplified Guard Original rule: l7 -> l18 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l7 -> l18 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l18 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l7 -> l18 : T, cost: 1 Propagated Equalities Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post20, destflag^0'=destflag^post20, edgecount^0'=edgecount^post20, h^0'=h^post20, i^0'=i^post20, j^0'=j^post20, k^0'=k^post20, k_1^0'=k_1^post20, min^0'=min^post20, nodecount^0'=nodecount^post20, sourceflag^0'=sourceflag^post20, (nodecount^0-nodecount^post20 == 0 /\ i^0-i^post20 == 0 /\ h^0-h^post20 == 0 /\ -sourceflag^post20+sourceflag^0 == 0 /\ -min^post20+min^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post20 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ k^0-k^post20 == 0 /\ -destflag^post20+destflag^0 == 0 /\ -j^post20+j^0 == 0 /\ k_1^0-k_1^post20 == 0), cost: 1 New rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality nodecount^post20 = nodecount^0 propagated equality i^post20 = i^0 propagated equality h^post20 = h^0 propagated equality sourceflag^post20 = sourceflag^0 propagated equality min^post20 = min^0 propagated equality __lengthofvisited^post20 = __lengthofvisited^0 propagated equality edgecount^post20 = edgecount^0 propagated equality k^post20 = k^0 propagated equality destflag^post20 = destflag^0 propagated equality j^post20 = j^0 propagated equality k_1^post20 = k_1^0 Simplified Guard Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l19 -> l16 : T, cost: 1 Propagated Equalities Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post21, destflag^0'=destflag^post21, edgecount^0'=edgecount^post21, h^0'=h^post21, i^0'=i^post21, j^0'=j^post21, k^0'=k^post21, k_1^0'=k_1^post21, min^0'=min^post21, nodecount^0'=nodecount^post21, sourceflag^0'=sourceflag^post21, (i^0-i^post21 == 0 /\ destflag^0-destflag^post21 == 0 /\ -j^post21+j^0 == 0 /\ -h^post21+h^0 == 0 /\ -k^post21+k^0 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ -__lengthofvisited^post21+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post21 == 0 /\ -1+sourceflag^post21 == 0 /\ -min^post21+min^0 == 0 /\ nodecount^0-nodecount^post21 == 0), cost: 1 New rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=1, 0 == 0, cost: 1 propagated equality i^post21 = i^0 propagated equality destflag^post21 = destflag^0 propagated equality j^post21 = j^0 propagated equality h^post21 = h^0 propagated equality k^post21 = k^0 propagated equality edgecount^post21 = edgecount^0 propagated equality __lengthofvisited^post21 = __lengthofvisited^0 propagated equality k_1^post21 = k_1^0 propagated equality sourceflag^post21 = 1 propagated equality min^post21 = min^0 propagated equality nodecount^post21 = nodecount^0 Simplified Guard Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=1, 0 == 0, cost: 1 New rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=1, T, cost: 1 New rule: l19 -> l16 : sourceflag^0'=1, T, cost: 1 Propagated Equalities Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^post22, destflag^0'=destflag^post22, edgecount^0'=edgecount^post22, h^0'=h^post22, i^0'=i^post22, j^0'=j^post22, k^0'=k^post22, k_1^0'=k_1^post22, min^0'=min^post22, nodecount^0'=nodecount^post22, sourceflag^0'=sourceflag^post22, (i^0-i^post22 == 0 /\ -h^post22+h^0 == 0 /\ -j^post22+j^0 == 0 /\ k_1^0-k_1^post22 == 0 /\ destflag^0-destflag^post22 == 0 /\ -sourceflag^post22+sourceflag^0 == 0 /\ -__lengthofvisited^post22+__lengthofvisited^0 == 0 /\ -min^post22+min^0 == 0 /\ nodecount^0-nodecount^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0 /\ -k^post22+k^0 == 0), cost: 1 New rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality i^post22 = i^0 propagated equality h^post22 = h^0 propagated equality j^post22 = j^0 propagated equality k_1^post22 = k_1^0 propagated equality destflag^post22 = destflag^0 propagated equality sourceflag^post22 = sourceflag^0 propagated equality __lengthofvisited^post22 = __lengthofvisited^0 propagated equality min^post22 = min^0 propagated equality nodecount^post22 = nodecount^0 propagated equality edgecount^post22 = edgecount^0 propagated equality k^post22 = k^0 Simplified Guard Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l19 -> l16 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l19 -> l16 : T, cost: 1 Propagated Equalities Original rule: l20 -> l13 : __lengthofvisited^0'=__lengthofvisited^post23, destflag^0'=destflag^post23, edgecount^0'=edgecount^post23, h^0'=h^post23, i^0'=i^post23, j^0'=j^post23, k^0'=k^post23, k_1^0'=k_1^post23, min^0'=min^post23, nodecount^0'=nodecount^post23, sourceflag^0'=sourceflag^post23, (i^0-i^post23 == 0 /\ j^post23 == 0 /\ -edgecount^post23+edgecount^0 == 0 /\ -__lengthofvisited^post23+__lengthofvisited^0 == 0 /\ nodecount^0-j^0 <= 0 /\ k_1^0-k_1^post23 == 0 /\ -1+destflag^post23 == 0 /\ -min^post23+min^0 == 0 /\ -sourceflag^post23+sourceflag^0 == 0 /\ -h^post23+h^0 == 0 /\ k^0-k^post23 == 0 /\ nodecount^0-nodecount^post23 == 0), cost: 1 New rule: l20 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=1, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ nodecount^0-j^0 <= 0), cost: 1 propagated equality i^post23 = i^0 propagated equality j^post23 = 0 propagated equality edgecount^post23 = edgecount^0 propagated equality __lengthofvisited^post23 = __lengthofvisited^0 propagated equality k_1^post23 = k_1^0 propagated equality destflag^post23 = 1 propagated equality min^post23 = min^0 propagated equality sourceflag^post23 = sourceflag^0 propagated equality h^post23 = h^0 propagated equality k^post23 = k^0 propagated equality nodecount^post23 = nodecount^0 Simplified Guard Original rule: l20 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=1, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ nodecount^0-j^0 <= 0), cost: 1 New rule: l20 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=1, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, nodecount^0-j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l20 -> l13 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=1, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, nodecount^0-j^0 <= 0, cost: 1 New rule: l20 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 1 Propagated Equalities Original rule: l20 -> l19 : __lengthofvisited^0'=__lengthofvisited^post24, destflag^0'=destflag^post24, edgecount^0'=edgecount^post24, h^0'=h^post24, i^0'=i^post24, j^0'=j^post24, k^0'=k^post24, k_1^0'=k_1^post24, min^0'=min^post24, nodecount^0'=nodecount^post24, sourceflag^0'=sourceflag^post24, (-edgecount^post24+edgecount^0 == 0 /\ -__lengthofvisited^post24+__lengthofvisited^0 == 0 /\ k^0-k^post24 == 0 /\ i^0-i^post24 == 0 /\ k_1^0-k_1^post24 == 0 /\ nodecount^0-nodecount^post24 == 0 /\ -min^post24+min^0 == 0 /\ h^0-h^post24 == 0 /\ destflag^0-destflag^post24 == 0 /\ -j^post24+j^0 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ -sourceflag^post24+sourceflag^0 == 0), cost: 1 New rule: l20 -> l19 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-nodecount^0+j^0 <= 0), cost: 1 propagated equality edgecount^post24 = edgecount^0 propagated equality __lengthofvisited^post24 = __lengthofvisited^0 propagated equality k^post24 = k^0 propagated equality i^post24 = i^0 propagated equality k_1^post24 = k_1^0 propagated equality nodecount^post24 = nodecount^0 propagated equality min^post24 = min^0 propagated equality h^post24 = h^0 propagated equality destflag^post24 = destflag^0 propagated equality j^post24 = j^0 propagated equality sourceflag^post24 = sourceflag^0 Simplified Guard Original rule: l20 -> l19 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1-nodecount^0+j^0 <= 0), cost: 1 New rule: l20 -> l19 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-nodecount^0+j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l20 -> l19 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1-nodecount^0+j^0 <= 0, cost: 1 New rule: l20 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 1 Propagated Equalities Original rule: l21 -> l22 : __lengthofvisited^0'=__lengthofvisited^post25, destflag^0'=destflag^post25, edgecount^0'=edgecount^post25, h^0'=h^post25, i^0'=i^post25, j^0'=j^post25, k^0'=k^post25, k_1^0'=k_1^post25, min^0'=min^post25, nodecount^0'=nodecount^post25, sourceflag^0'=sourceflag^post25, (-__lengthofvisited^post25+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post25 == 0 /\ -sourceflag^post25+sourceflag^0 == 0 /\ destflag^0-destflag^post25 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ min^0-min^post25 == 0 /\ edgecount^0-edgecount^post25 == 0 /\ -k^post25+k^0 == 0 /\ -1+h^post25-h^0 == 0 /\ j^0-j^post25 == 0 /\ i^0-i^post25 == 0), cost: 1 New rule: l21 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=1+h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality __lengthofvisited^post25 = __lengthofvisited^0 propagated equality k_1^post25 = k_1^0 propagated equality sourceflag^post25 = sourceflag^0 propagated equality destflag^post25 = destflag^0 propagated equality nodecount^post25 = nodecount^0 propagated equality min^post25 = min^0 propagated equality edgecount^post25 = edgecount^0 propagated equality k^post25 = k^0 propagated equality h^post25 = 1+h^0 propagated equality j^post25 = j^0 propagated equality i^post25 = i^0 Simplified Guard Original rule: l21 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=1+h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l21 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=1+h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l21 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=1+h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l21 -> l22 : h^0'=1+h^0, T, cost: 1 Propagated Equalities Original rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^post26, destflag^0'=destflag^post26, edgecount^0'=edgecount^post26, h^0'=h^post26, i^0'=i^post26, j^0'=j^post26, k^0'=k^post26, k_1^0'=k_1^post26, min^0'=min^post26, nodecount^0'=nodecount^post26, sourceflag^0'=sourceflag^post26, (-i^post26+i^0 == 0 /\ -j^post26+j^0 == 0 /\ -sourceflag^post26+sourceflag^0 == 0 /\ -k_1^post26+k_1^0 == 0 /\ min^post26-h^0 == 0 /\ nodecount^0-nodecount^post26 == 0 /\ __lengthofvisited^0-__lengthofvisited^post26 == 0 /\ -edgecount^post26+edgecount^0 == 0 /\ k^0-k^post26 == 0 /\ h^0-h^post26 == 0 /\ -destflag^post26+destflag^0 == 0), cost: 1 New rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=h^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality i^post26 = i^0 propagated equality j^post26 = j^0 propagated equality sourceflag^post26 = sourceflag^0 propagated equality k_1^post26 = k_1^0 propagated equality min^post26 = h^0 propagated equality nodecount^post26 = nodecount^0 propagated equality __lengthofvisited^post26 = __lengthofvisited^0 propagated equality edgecount^post26 = edgecount^0 propagated equality k^post26 = k^0 propagated equality h^post26 = h^0 propagated equality destflag^post26 = destflag^0 Simplified Guard Original rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=h^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=h^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=h^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l23 -> l21 : min^0'=h^0, T, cost: 1 Propagated Equalities Original rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^post27, destflag^0'=destflag^post27, edgecount^0'=edgecount^post27, h^0'=h^post27, i^0'=i^post27, j^0'=j^post27, k^0'=k^post27, k_1^0'=k_1^post27, min^0'=min^post27, nodecount^0'=nodecount^post27, sourceflag^0'=sourceflag^post27, (-sourceflag^post27+sourceflag^0 == 0 /\ -min^post27+min^0 == 0 /\ -__lengthofvisited^post27+__lengthofvisited^0 == 0 /\ destflag^0-destflag^post27 == 0 /\ -edgecount^post27+edgecount^0 == 0 /\ -k^post27+k^0 == 0 /\ nodecount^0-nodecount^post27 == 0 /\ j^0-j^post27 == 0 /\ k_1^0-k_1^post27 == 0 /\ -h^post27+h^0 == 0 /\ i^0-i^post27 == 0), cost: 1 New rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality sourceflag^post27 = sourceflag^0 propagated equality min^post27 = min^0 propagated equality __lengthofvisited^post27 = __lengthofvisited^0 propagated equality destflag^post27 = destflag^0 propagated equality edgecount^post27 = edgecount^0 propagated equality k^post27 = k^0 propagated equality nodecount^post27 = nodecount^0 propagated equality j^post27 = j^0 propagated equality k_1^post27 = k_1^0 propagated equality h^post27 = h^0 propagated equality i^post27 = i^0 Simplified Guard Original rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l23 -> l21 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l23 -> l21 : T, cost: 1 Propagated Equalities Original rule: l22 -> l24 : __lengthofvisited^0'=__lengthofvisited^post28, destflag^0'=destflag^post28, edgecount^0'=edgecount^post28, h^0'=h^post28, i^0'=i^post28, j^0'=j^post28, k^0'=k^post28, k_1^0'=k_1^post28, min^0'=min^post28, nodecount^0'=nodecount^post28, sourceflag^0'=sourceflag^post28, (k^0-k^post28 == 0 /\ k_1^0-k_1^post28 == 0 /\ -__lengthofvisited^post28+__lengthofvisited^0 == 0 /\ -edgecount^post28+edgecount^0 == 0 /\ i^0-i^post28 == 0 /\ -j^post28+j^0 == 0 /\ -sourceflag^post28+sourceflag^0 == 0 /\ nodecount^0-nodecount^post28 == 0 /\ h^0-h^post28 == 0 /\ -min^post28+min^0 == 0 /\ destflag^0-destflag^post28 == 0), cost: 1 New rule: l22 -> l24 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality k^post28 = k^0 propagated equality k_1^post28 = k_1^0 propagated equality __lengthofvisited^post28 = __lengthofvisited^0 propagated equality edgecount^post28 = edgecount^0 propagated equality i^post28 = i^0 propagated equality j^post28 = j^0 propagated equality sourceflag^post28 = sourceflag^0 propagated equality nodecount^post28 = nodecount^0 propagated equality h^post28 = h^0 propagated equality min^post28 = min^0 propagated equality destflag^post28 = destflag^0 Simplified Guard Original rule: l22 -> l24 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l22 -> l24 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l22 -> l24 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l22 -> l24 : T, cost: 1 Propagated Equalities Original rule: l24 -> l17 : __lengthofvisited^0'=__lengthofvisited^post29, destflag^0'=destflag^post29, edgecount^0'=edgecount^post29, h^0'=h^post29, i^0'=i^post29, j^0'=j^post29, k^0'=k^post29, k_1^0'=k_1^post29, min^0'=min^post29, nodecount^0'=nodecount^post29, sourceflag^0'=sourceflag^post29, (j^post29 == 0 /\ destflag^0-destflag^post29 == 0 /\ k_1^0-k_1^post29 == 0 /\ -edgecount^post29+edgecount^0 == 0 /\ min^0-min^post29 == 0 /\ i^0-i^post29 == 0 /\ sourceflag^post29 == 0 /\ -k^post29+k^0 == 0 /\ -nodecount^post29+nodecount^0 == 0 /\ -h^post29+h^0 == 0 /\ -__lengthofvisited^post29+__lengthofvisited^0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1 New rule: l24 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=0, (0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1 propagated equality j^post29 = 0 propagated equality destflag^post29 = destflag^0 propagated equality k_1^post29 = k_1^0 propagated equality edgecount^post29 = edgecount^0 propagated equality min^post29 = min^0 propagated equality i^post29 = i^0 propagated equality sourceflag^post29 = 0 propagated equality k^post29 = k^0 propagated equality nodecount^post29 = nodecount^0 propagated equality h^post29 = h^0 propagated equality __lengthofvisited^post29 = __lengthofvisited^0 Simplified Guard Original rule: l24 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=0, (0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1 New rule: l24 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l24 -> l17 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1 New rule: l24 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l24 -> l23 : __lengthofvisited^0'=__lengthofvisited^post30, destflag^0'=destflag^post30, edgecount^0'=edgecount^post30, h^0'=h^post30, i^0'=i^post30, j^0'=j^post30, k^0'=k^post30, k_1^0'=k_1^post30, min^0'=min^post30, nodecount^0'=nodecount^post30, sourceflag^0'=sourceflag^post30, (__lengthofvisited^0-__lengthofvisited^post30 == 0 /\ nodecount^0-nodecount^post30 == 0 /\ -min^post30+min^0 == 0 /\ -destflag^post30+destflag^0 == 0 /\ -sourceflag^post30+sourceflag^0 == 0 /\ k^0-k^post30 == 0 /\ -j^post30+j^0 == 0 /\ i^0-i^post30 == 0 /\ 1+h^0-edgecount^0 <= 0 /\ h^0-h^post30 == 0 /\ k_1^0-k_1^post30 == 0 /\ -edgecount^post30+edgecount^0 == 0), cost: 1 New rule: l24 -> l23 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+h^0-edgecount^0 <= 0), cost: 1 propagated equality __lengthofvisited^post30 = __lengthofvisited^0 propagated equality nodecount^post30 = nodecount^0 propagated equality min^post30 = min^0 propagated equality destflag^post30 = destflag^0 propagated equality sourceflag^post30 = sourceflag^0 propagated equality k^post30 = k^0 propagated equality j^post30 = j^0 propagated equality i^post30 = i^0 propagated equality h^post30 = h^0 propagated equality k_1^post30 = k_1^0 propagated equality edgecount^post30 = edgecount^0 Simplified Guard Original rule: l24 -> l23 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+h^0-edgecount^0 <= 0), cost: 1 New rule: l24 -> l23 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+h^0-edgecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l24 -> l23 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+h^0-edgecount^0 <= 0, cost: 1 New rule: l24 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l18 -> l4 : __lengthofvisited^0'=__lengthofvisited^post31, destflag^0'=destflag^post31, edgecount^0'=edgecount^post31, h^0'=h^post31, i^0'=i^post31, j^0'=j^post31, k^0'=k^post31, k_1^0'=k_1^post31, min^0'=min^post31, nodecount^0'=nodecount^post31, sourceflag^0'=sourceflag^post31, (i^0-i^post31 == 0 /\ -1+k^post31-k^0 == 0 /\ destflag^0-destflag^post31 == 0 /\ -j^post31+j^0 == 0 /\ -k_1^0+edgecount^0 <= 0 /\ -h^post31+h^0 == 0 /\ -edgecount^post31+edgecount^0 == 0 /\ k_1^0-k_1^post31 == 0 /\ -__lengthofvisited^post31+__lengthofvisited^0 == 0 /\ -sourceflag^post31+sourceflag^0 == 0 /\ -min^post31+min^0 == 0 /\ nodecount^0-nodecount^post31 == 0), cost: 1 New rule: l18 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=1+k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -k_1^0+edgecount^0 <= 0), cost: 1 propagated equality i^post31 = i^0 propagated equality k^post31 = 1+k^0 propagated equality destflag^post31 = destflag^0 propagated equality j^post31 = j^0 propagated equality h^post31 = h^0 propagated equality edgecount^post31 = edgecount^0 propagated equality k_1^post31 = k_1^0 propagated equality __lengthofvisited^post31 = __lengthofvisited^0 propagated equality sourceflag^post31 = sourceflag^0 propagated equality min^post31 = min^0 propagated equality nodecount^post31 = nodecount^0 Simplified Guard Original rule: l18 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=1+k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -k_1^0+edgecount^0 <= 0), cost: 1 New rule: l18 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=1+k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -k_1^0+edgecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l18 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=1+k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -k_1^0+edgecount^0 <= 0, cost: 1 New rule: l18 -> l4 : k^0'=1+k^0, -k_1^0+edgecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l18 -> l22 : __lengthofvisited^0'=__lengthofvisited^post32, destflag^0'=destflag^post32, edgecount^0'=edgecount^post32, h^0'=h^post32, i^0'=i^post32, j^0'=j^post32, k^0'=k^post32, k_1^0'=k_1^post32, min^0'=min^post32, nodecount^0'=nodecount^post32, sourceflag^0'=sourceflag^post32, (i^0-i^post32 == 0 /\ -__lengthofvisited^post32+__lengthofvisited^0 == 0 /\ h^post32 == 0 /\ -j^post32+j^0 == 0 /\ -destflag^post32+destflag^0 == 0 /\ -edgecount^post32+edgecount^0 == 0 /\ k_1^0-k_1^post32 == 0 /\ k^0-k^post32 == 0 /\ 1+k_1^0-edgecount^0 <= 0 /\ -min^post32+min^0 == 0 /\ nodecount^0-nodecount^post32 == 0 /\ -sourceflag^post32+sourceflag^0 == 0), cost: 1 New rule: l18 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+k_1^0-edgecount^0 <= 0), cost: 1 propagated equality i^post32 = i^0 propagated equality __lengthofvisited^post32 = __lengthofvisited^0 propagated equality h^post32 = 0 propagated equality j^post32 = j^0 propagated equality destflag^post32 = destflag^0 propagated equality edgecount^post32 = edgecount^0 propagated equality k_1^post32 = k_1^0 propagated equality k^post32 = k^0 propagated equality min^post32 = min^0 propagated equality nodecount^post32 = nodecount^0 propagated equality sourceflag^post32 = sourceflag^0 Simplified Guard Original rule: l18 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+k_1^0-edgecount^0 <= 0), cost: 1 New rule: l18 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+k_1^0-edgecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l18 -> l22 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+k_1^0-edgecount^0 <= 0, cost: 1 New rule: l18 -> l22 : h^0'=0, 1+k_1^0-edgecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l7 : __lengthofvisited^0'=__lengthofvisited^post33, destflag^0'=destflag^post33, edgecount^0'=edgecount^post33, h^0'=h^post33, i^0'=i^post33, j^0'=j^post33, k^0'=k^post33, k_1^0'=k_1^post33, min^0'=min^post33, nodecount^0'=nodecount^post33, sourceflag^0'=sourceflag^post33, (-__lengthofvisited^post33+__lengthofvisited^0 == 0 /\ -h^post33+h^0 == 0 /\ -edgecount^post33+edgecount^0 == 0 /\ -j^post33+j^0 == 0 /\ i^0-i^post33 == 0 /\ min^0-min^post33 == 0 /\ -i^0+edgecount^0 <= 0 /\ -nodecount^post33+nodecount^0 == 0 /\ destflag^0-destflag^post33 == 0 /\ k_1^post33 == 0 /\ -k^post33+k^0 == 0 /\ -sourceflag^post33+sourceflag^0 == 0), cost: 1 New rule: l11 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -i^0+edgecount^0 <= 0), cost: 1 propagated equality __lengthofvisited^post33 = __lengthofvisited^0 propagated equality h^post33 = h^0 propagated equality edgecount^post33 = edgecount^0 propagated equality j^post33 = j^0 propagated equality i^post33 = i^0 propagated equality min^post33 = min^0 propagated equality nodecount^post33 = nodecount^0 propagated equality destflag^post33 = destflag^0 propagated equality k_1^post33 = 0 propagated equality k^post33 = k^0 propagated equality sourceflag^post33 = sourceflag^0 Simplified Guard Original rule: l11 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -i^0+edgecount^0 <= 0), cost: 1 New rule: l11 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -i^0+edgecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l7 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -i^0+edgecount^0 <= 0, cost: 1 New rule: l11 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l10 : __lengthofvisited^0'=__lengthofvisited^post34, destflag^0'=destflag^post34, edgecount^0'=edgecount^post34, h^0'=h^post34, i^0'=i^post34, j^0'=j^post34, k^0'=k^post34, k_1^0'=k_1^post34, min^0'=min^post34, nodecount^0'=nodecount^post34, sourceflag^0'=sourceflag^post34, (-min^post34+min^0 == 0 /\ -k_1^post34+k_1^0 == 0 /\ -j^post34+j^0 == 0 /\ -destflag^post34+destflag^0 == 0 /\ -edgecount^post34+edgecount^0 == 0 /\ 1+i^0-edgecount^0 <= 0 /\ nodecount^0-nodecount^post34 == 0 /\ __lengthofvisited^0-__lengthofvisited^post34 == 0 /\ -sourceflag^post34+sourceflag^0 == 0 /\ k^0-k^post34 == 0 /\ -1+i^post34-i^0 == 0 /\ h^0-h^post34 == 0), cost: 1 New rule: l11 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+i^0-edgecount^0 <= 0), cost: 1 propagated equality min^post34 = min^0 propagated equality k_1^post34 = k_1^0 propagated equality j^post34 = j^0 propagated equality destflag^post34 = destflag^0 propagated equality edgecount^post34 = edgecount^0 propagated equality nodecount^post34 = nodecount^0 propagated equality __lengthofvisited^post34 = __lengthofvisited^0 propagated equality sourceflag^post34 = sourceflag^0 propagated equality k^post34 = k^0 propagated equality i^post34 = 1+i^0 propagated equality h^post34 = h^0 Simplified Guard Original rule: l11 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+i^0-edgecount^0 <= 0), cost: 1 New rule: l11 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+i^0-edgecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+i^0-edgecount^0 <= 0, cost: 1 New rule: l11 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l17 -> l20 : __lengthofvisited^0'=__lengthofvisited^post35, destflag^0'=destflag^post35, edgecount^0'=edgecount^post35, h^0'=h^post35, i^0'=i^post35, j^0'=j^post35, k^0'=k^post35, k_1^0'=k_1^post35, min^0'=min^post35, nodecount^0'=nodecount^post35, sourceflag^0'=sourceflag^post35, (k_1^0-k_1^post35 == 0 /\ -h^post35+h^0 == 0 /\ -sourceflag^post35+sourceflag^0 == 0 /\ -__lengthofvisited^post35+__lengthofvisited^0 == 0 /\ -nodecount^post35+nodecount^0 == 0 /\ destflag^0-destflag^post35 == 0 /\ min^0-min^post35 == 0 /\ -k^post35+k^0 == 0 /\ edgecount^0-edgecount^post35 == 0 /\ j^0-j^post35 == 0 /\ i^0-i^post35 == 0), cost: 1 New rule: l17 -> l20 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality k_1^post35 = k_1^0 propagated equality h^post35 = h^0 propagated equality sourceflag^post35 = sourceflag^0 propagated equality __lengthofvisited^post35 = __lengthofvisited^0 propagated equality nodecount^post35 = nodecount^0 propagated equality destflag^post35 = destflag^0 propagated equality min^post35 = min^0 propagated equality k^post35 = k^0 propagated equality edgecount^post35 = edgecount^0 propagated equality j^post35 = j^0 propagated equality i^post35 = i^0 Simplified Guard Original rule: l17 -> l20 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l17 -> l20 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l17 -> l20 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l17 -> l20 : T, cost: 1 Propagated Equalities Original rule: l25 -> l10 : __lengthofvisited^0'=__lengthofvisited^post36, destflag^0'=destflag^post36, edgecount^0'=edgecount^post36, h^0'=h^post36, i^0'=i^post36, j^0'=j^post36, k^0'=k^post36, k_1^0'=k_1^post36, min^0'=min^post36, nodecount^0'=nodecount^post36, sourceflag^0'=sourceflag^post36, (-j^post36+j^0 == 0 /\ k^0-k^post36 == 0 /\ min^post36 == 0 /\ h^0-h^post36 == 0 /\ -sourceflag^post36+sourceflag^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post36 == 0 /\ -edgecount^post36+edgecount^0 == 0 /\ k_1^0-k_1^post36 == 0 /\ nodecount^0-nodecount^post36 == 0 /\ -destflag^post36+destflag^0 == 0 /\ i^post36 == 0), cost: 1 New rule: l25 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality j^post36 = j^0 propagated equality k^post36 = k^0 propagated equality min^post36 = 0 propagated equality h^post36 = h^0 propagated equality sourceflag^post36 = sourceflag^0 propagated equality __lengthofvisited^post36 = __lengthofvisited^0 propagated equality edgecount^post36 = edgecount^0 propagated equality k_1^post36 = k_1^0 propagated equality nodecount^post36 = nodecount^0 propagated equality destflag^post36 = destflag^0 propagated equality i^post36 = 0 Simplified Guard Original rule: l25 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l25 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l25 -> l10 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l25 -> l10 : i^0'=0, min^0'=0, T, cost: 1 made implied equalities explicit Original rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^post37, destflag^0'=destflag^post37, edgecount^0'=edgecount^post37, h^0'=h^post37, i^0'=i^post37, j^0'=j^post37, k^0'=k^post37, k_1^0'=k_1^post37, min^0'=min^post37, nodecount^0'=nodecount^post37, sourceflag^0'=sourceflag^post37, (-1+nodecount^0-k^0 <= 0 /\ k^0-k^post37 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ -min^post37+min^0 == 0 /\ k_1^0-k_1^post37 == 0 /\ i^0-i^post37 == 0 /\ 1-nodecount^0+k^0 <= 0 /\ h^0-h^post37 == 0 /\ nodecount^0-nodecount^post37 == 0 /\ -j^post37+j^0 == 0 /\ destflag^0-destflag^post37 == 0), cost: 1 New rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^post37, destflag^0'=destflag^post37, edgecount^0'=edgecount^post37, h^0'=h^post37, i^0'=i^post37, j^0'=j^post37, k^0'=k^post37, k_1^0'=k_1^post37, min^0'=min^post37, nodecount^0'=nodecount^post37, sourceflag^0'=sourceflag^post37, (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ k^0-k^post37 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ -min^post37+min^0 == 0 /\ k_1^0-k_1^post37 == 0 /\ i^0-i^post37 == 0 /\ 1-nodecount^0+k^0 <= 0 /\ h^0-h^post37 == 0 /\ nodecount^0-nodecount^post37 == 0 /\ -j^post37+j^0 == 0 /\ destflag^0-destflag^post37 == 0), cost: 1 Propagated Equalities Original rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^post37, destflag^0'=destflag^post37, edgecount^0'=edgecount^post37, h^0'=h^post37, i^0'=i^post37, j^0'=j^post37, k^0'=k^post37, k_1^0'=k_1^post37, min^0'=min^post37, nodecount^0'=nodecount^post37, sourceflag^0'=sourceflag^post37, (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ k^0-k^post37 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ -min^post37+min^0 == 0 /\ k_1^0-k_1^post37 == 0 /\ i^0-i^post37 == 0 /\ 1-nodecount^0+k^0 <= 0 /\ h^0-h^post37 == 0 /\ nodecount^0-nodecount^post37 == 0 /\ -j^post37+j^0 == 0 /\ destflag^0-destflag^post37 == 0), cost: 1 New rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 propagated equality k^post37 = k^0 propagated equality sourceflag^post37 = sourceflag^0 propagated equality edgecount^post37 = edgecount^0 propagated equality __lengthofvisited^post37 = __lengthofvisited^0 propagated equality min^post37 = min^0 propagated equality k_1^post37 = k_1^0 propagated equality i^post37 = i^0 propagated equality h^post37 = h^0 propagated equality nodecount^post37 = nodecount^0 propagated equality j^post37 = j^0 propagated equality destflag^post37 = destflag^0 Simplified Guard Original rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 New rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 made implied equalities explicit Original rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 New rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l5 -> l26 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 New rule: l5 -> l26 : (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 Propagated Equalities Original rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^post38, destflag^0'=destflag^post38, edgecount^0'=edgecount^post38, h^0'=h^post38, i^0'=i^post38, j^0'=j^post38, k^0'=k^post38, k_1^0'=k_1^post38, min^0'=min^post38, nodecount^0'=nodecount^post38, sourceflag^0'=sourceflag^post38, (k^0-k^post38 == 0 /\ -__lengthofvisited^post38+__lengthofvisited^0 == 0 /\ -min^post38+min^0 == 0 /\ -edgecount^post38+edgecount^0 == 0 /\ -sourceflag^post38+sourceflag^0 == 0 /\ i^0-i^post38 == 0 /\ k_1^0-k_1^post38 == 0 /\ -j^post38+j^0 == 0 /\ -h^post38+h^0 == 0 /\ -nodecount^post38+nodecount^0 == 0 /\ nodecount^0-k^0 <= 0 /\ destflag^0-destflag^post38 == 0), cost: 1 New rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ nodecount^0-k^0 <= 0), cost: 1 propagated equality k^post38 = k^0 propagated equality __lengthofvisited^post38 = __lengthofvisited^0 propagated equality min^post38 = min^0 propagated equality edgecount^post38 = edgecount^0 propagated equality sourceflag^post38 = sourceflag^0 propagated equality i^post38 = i^0 propagated equality k_1^post38 = k_1^0 propagated equality j^post38 = j^0 propagated equality h^post38 = h^0 propagated equality nodecount^post38 = nodecount^0 propagated equality destflag^post38 = destflag^0 Simplified Guard Original rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ nodecount^0-k^0 <= 0), cost: 1 New rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, nodecount^0-k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, nodecount^0-k^0 <= 0, cost: 1 New rule: l5 -> l25 : nodecount^0-k^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^post39, destflag^0'=destflag^post39, edgecount^0'=edgecount^post39, h^0'=h^post39, i^0'=i^post39, j^0'=j^post39, k^0'=k^post39, k_1^0'=k_1^post39, min^0'=min^post39, nodecount^0'=nodecount^post39, sourceflag^0'=sourceflag^post39, (min^0-min^post39 == 0 /\ __lengthofvisited^0-__lengthofvisited^post39 == 0 /\ -sourceflag^post39+sourceflag^0 == 0 /\ -k^post39+k^0 == 0 /\ -edgecount^post39+edgecount^0 == 0 /\ -destflag^post39+destflag^0 == 0 /\ h^0-h^post39 == 0 /\ j^0-j^post39 == 0 /\ -nodecount^post39+nodecount^0 == 0 /\ 2-nodecount^0+k^0 <= 0 /\ k_1^0-k_1^post39 == 0 /\ i^0-i^post39 == 0), cost: 1 New rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 2-nodecount^0+k^0 <= 0), cost: 1 propagated equality min^post39 = min^0 propagated equality __lengthofvisited^post39 = __lengthofvisited^0 propagated equality sourceflag^post39 = sourceflag^0 propagated equality k^post39 = k^0 propagated equality edgecount^post39 = edgecount^0 propagated equality destflag^post39 = destflag^0 propagated equality h^post39 = h^0 propagated equality j^post39 = j^0 propagated equality nodecount^post39 = nodecount^0 propagated equality k_1^post39 = k_1^0 propagated equality i^post39 = i^0 Simplified Guard Original rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 2-nodecount^0+k^0 <= 0), cost: 1 New rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 2-nodecount^0+k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l25 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 2-nodecount^0+k^0 <= 0, cost: 1 New rule: l5 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l4 : __lengthofvisited^0'=__lengthofvisited^post40, destflag^0'=destflag^post40, edgecount^0'=edgecount^post40, h^0'=h^post40, i^0'=i^post40, j^0'=j^post40, k^0'=k^post40, k_1^0'=k_1^post40, min^0'=min^post40, nodecount^0'=nodecount^post40, sourceflag^0'=sourceflag^post40, (nodecount^0-nodecount^post40 == 0 /\ i^0-i^post40 == 0 /\ -sourceflag^post40+sourceflag^0 == 0 /\ h^0-h^post40 == 0 /\ -j^post40+j^0 == 0 /\ k^post40 == 0 /\ __lengthofvisited^0-__lengthofvisited^post40 == 0 /\ destflag^0-destflag^post40 == 0 /\ k_1^0-k_1^post40 == 0 /\ -edgecount^post40+edgecount^0 == 0 /\ -1-i^0+nodecount^0 <= 0 /\ -min^post40+min^0 == 0), cost: 1 New rule: l3 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -1-i^0+nodecount^0 <= 0), cost: 1 propagated equality nodecount^post40 = nodecount^0 propagated equality i^post40 = i^0 propagated equality sourceflag^post40 = sourceflag^0 propagated equality h^post40 = h^0 propagated equality j^post40 = j^0 propagated equality k^post40 = 0 propagated equality __lengthofvisited^post40 = __lengthofvisited^0 propagated equality destflag^post40 = destflag^0 propagated equality k_1^post40 = k_1^0 propagated equality edgecount^post40 = edgecount^0 propagated equality min^post40 = min^0 Simplified Guard Original rule: l3 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -1-i^0+nodecount^0 <= 0), cost: 1 New rule: l3 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -1-i^0+nodecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -1-i^0+nodecount^0 <= 0, cost: 1 New rule: l3 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : __lengthofvisited^0'=__lengthofvisited^post41, destflag^0'=destflag^post41, edgecount^0'=edgecount^post41, h^0'=h^post41, i^0'=i^post41, j^0'=j^post41, k^0'=k^post41, k_1^0'=k_1^post41, min^0'=min^post41, nodecount^0'=nodecount^post41, sourceflag^0'=sourceflag^post41, (2+i^0-nodecount^0 <= 0 /\ destflag^0-destflag^post41 == 0 /\ -j^post41+j^0 == 0 /\ -h^post41+h^0 == 0 /\ -edgecount^post41+edgecount^0 == 0 /\ -__lengthofvisited^post41+__lengthofvisited^0 == 0 /\ k_1^0-k_1^post41 == 0 /\ -1-i^0+i^post41 == 0 /\ -k^post41+k^0 == 0 /\ -sourceflag^post41+sourceflag^0 == 0 /\ nodecount^0-nodecount^post41 == 0 /\ -min^post41+min^0 == 0), cost: 1 New rule: l3 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 2+i^0-nodecount^0 <= 0), cost: 1 propagated equality destflag^post41 = destflag^0 propagated equality j^post41 = j^0 propagated equality h^post41 = h^0 propagated equality edgecount^post41 = edgecount^0 propagated equality __lengthofvisited^post41 = __lengthofvisited^0 propagated equality k_1^post41 = k_1^0 propagated equality i^post41 = 1+i^0 propagated equality k^post41 = k^0 propagated equality sourceflag^post41 = sourceflag^0 propagated equality nodecount^post41 = nodecount^0 propagated equality min^post41 = min^0 Simplified Guard Original rule: l3 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 2+i^0-nodecount^0 <= 0), cost: 1 New rule: l3 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 2+i^0-nodecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 2+i^0-nodecount^0 <= 0, cost: 1 New rule: l3 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l13 -> l15 : __lengthofvisited^0'=__lengthofvisited^post42, destflag^0'=destflag^post42, edgecount^0'=edgecount^post42, h^0'=h^post42, i^0'=i^post42, j^0'=j^post42, k^0'=k^post42, k_1^0'=k_1^post42, min^0'=min^post42, nodecount^0'=nodecount^post42, sourceflag^0'=sourceflag^post42, (-__lengthofvisited^post42+__lengthofvisited^0 == 0 /\ -edgecount^post42+edgecount^0 == 0 /\ k_1^0-k_1^post42 == 0 /\ min^0-min^post42 == 0 /\ destflag^0-destflag^post42 == 0 /\ -sourceflag^post42+sourceflag^0 == 0 /\ i^0-i^post42 == 0 /\ -h^post42+h^0 == 0 /\ -nodecount^post42+nodecount^0 == 0 /\ -k^post42+k^0 == 0 /\ -j^post42+j^0 == 0), cost: 1 New rule: l13 -> l15 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality __lengthofvisited^post42 = __lengthofvisited^0 propagated equality edgecount^post42 = edgecount^0 propagated equality k_1^post42 = k_1^0 propagated equality min^post42 = min^0 propagated equality destflag^post42 = destflag^0 propagated equality sourceflag^post42 = sourceflag^0 propagated equality i^post42 = i^0 propagated equality h^post42 = h^0 propagated equality nodecount^post42 = nodecount^0 propagated equality k^post42 = k^0 propagated equality j^post42 = j^0 Simplified Guard Original rule: l13 -> l15 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l13 -> l15 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l13 -> l15 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l13 -> l15 : T, cost: 1 Propagated Equalities Original rule: l1 -> l2 : __lengthofvisited^0'=__lengthofvisited^post43, destflag^0'=destflag^post43, edgecount^0'=edgecount^post43, h^0'=h^post43, i^0'=i^post43, j^0'=j^post43, k^0'=k^post43, k_1^0'=k_1^post43, min^0'=min^post43, nodecount^0'=nodecount^post43, sourceflag^0'=sourceflag^post43, (-i^0+nodecount^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post43 == 0 /\ -j^post43+j^0 == 0 /\ i^post43 == 0 /\ -k_1^post43+k_1^0 == 0 /\ -destflag^post43+destflag^0 == 0 /\ nodecount^0-nodecount^post43 == 0 /\ -min^post43+min^0 == 0 /\ k^0-k^post43 == 0 /\ -sourceflag^post43+sourceflag^0 == 0 /\ h^0-h^post43 == 0 /\ -edgecount^post43+edgecount^0 == 0), cost: 1 New rule: l1 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -i^0+nodecount^0 <= 0), cost: 1 propagated equality __lengthofvisited^post43 = __lengthofvisited^0 propagated equality j^post43 = j^0 propagated equality i^post43 = 0 propagated equality k_1^post43 = k_1^0 propagated equality destflag^post43 = destflag^0 propagated equality nodecount^post43 = nodecount^0 propagated equality min^post43 = min^0 propagated equality k^post43 = k^0 propagated equality sourceflag^post43 = sourceflag^0 propagated equality h^post43 = h^0 propagated equality edgecount^post43 = edgecount^0 Simplified Guard Original rule: l1 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ -i^0+nodecount^0 <= 0), cost: 1 New rule: l1 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -i^0+nodecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, -i^0+nodecount^0 <= 0, cost: 1 New rule: l1 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l0 : __lengthofvisited^0'=__lengthofvisited^post44, destflag^0'=destflag^post44, edgecount^0'=edgecount^post44, h^0'=h^post44, i^0'=i^post44, j^0'=j^post44, k^0'=k^post44, k_1^0'=k_1^post44, min^0'=min^post44, nodecount^0'=nodecount^post44, sourceflag^0'=sourceflag^post44, (k_1^0-k_1^post44 == 0 /\ -k^post44+k^0 == 0 /\ -1-i^0+i^post44 == 0 /\ -nodecount^post44+nodecount^0 == 0 /\ -sourceflag^post44+sourceflag^0 == 0 /\ destflag^0-destflag^post44 == 0 /\ min^0-min^post44 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ -h^post44+h^0 == 0 /\ j^0-j^post44 == 0 /\ -__lengthofvisited^post44+__lengthofvisited^0 == 0 /\ -edgecount^post44+edgecount^0 == 0), cost: 1 New rule: l1 -> l0 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+i^0-nodecount^0 <= 0), cost: 1 propagated equality k_1^post44 = k_1^0 propagated equality k^post44 = k^0 propagated equality i^post44 = 1+i^0 propagated equality nodecount^post44 = nodecount^0 propagated equality sourceflag^post44 = sourceflag^0 propagated equality destflag^post44 = destflag^0 propagated equality min^post44 = min^0 propagated equality h^post44 = h^0 propagated equality j^post44 = j^0 propagated equality __lengthofvisited^post44 = __lengthofvisited^0 propagated equality edgecount^post44 = edgecount^0 Simplified Guard Original rule: l1 -> l0 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, (0 == 0 /\ 1+i^0-nodecount^0 <= 0), cost: 1 New rule: l1 -> l0 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+i^0-nodecount^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : __lengthofvisited^0'=__lengthofvisited^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1+i^0, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 1+i^0-nodecount^0 <= 0, cost: 1 New rule: l1 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1 Propagated Equalities Original rule: l28 -> l0 : __lengthofvisited^0'=__lengthofvisited^post45, destflag^0'=destflag^post45, edgecount^0'=edgecount^post45, h^0'=h^post45, i^0'=i^post45, j^0'=j^post45, k^0'=k^post45, k_1^0'=k_1^post45, min^0'=min^post45, nodecount^0'=nodecount^post45, sourceflag^0'=sourceflag^post45, (edgecount^0-edgecount^post46 == 0 /\ k_1^0-k_1^post46 == 0 /\ h^post46-h^post45 == 0 /\ -j^post45+j^post46 == 0 /\ -k^post46+k^0 == 0 /\ -1+i^post45 == 0 /\ min^0-min^post46 == 0 /\ -k_1^post45+k_1^post46 == 0 /\ k^post46-k^post45 == 0 /\ -__lengthofvisited^post46+__lengthofvisited^0 == 0 /\ -nodecount^post46+nodecount^0 == 0 /\ -min^post45+min^post46 == 0 /\ destflag^0-destflag^post46 == 0 /\ -destflag^post45+destflag^post46 == 0 /\ sourceflag^post46-sourceflag^post45 == 0 /\ __lengthofvisited^post45-edgecount^post46 == 0 /\ -sourceflag^post46+sourceflag^0 == 0 /\ nodecount^post46-nodecount^post45 == 0 /\ j^0-j^post46 == 0 /\ -h^post46+h^0 == 0 /\ -edgecount^post45+edgecount^post46 == 0 /\ i^0-i^post46 == 0), cost: 1 New rule: l28 -> l0 : __lengthofvisited^0'=edgecount^post46, destflag^0'=destflag^post46, edgecount^0'=edgecount^post46, h^0'=h^post46, i^0'=1, j^0'=j^post46, k^0'=k^post46, k_1^0'=k_1^post46, min^0'=min^post46, nodecount^0'=nodecount^post46, sourceflag^0'=sourceflag^post46, (0 == 0 /\ edgecount^0-edgecount^post46 == 0 /\ k_1^0-k_1^post46 == 0 /\ -k^post46+k^0 == 0 /\ min^0-min^post46 == 0 /\ -__lengthofvisited^post46+__lengthofvisited^0 == 0 /\ -nodecount^post46+nodecount^0 == 0 /\ destflag^0-destflag^post46 == 0 /\ -sourceflag^post46+sourceflag^0 == 0 /\ j^0-j^post46 == 0 /\ -h^post46+h^0 == 0 /\ i^0-i^post46 == 0), cost: 1 propagated equality h^post45 = h^post46 propagated equality j^post45 = j^post46 propagated equality i^post45 = 1 propagated equality k_1^post45 = k_1^post46 propagated equality k^post45 = k^post46 propagated equality min^post45 = min^post46 propagated equality destflag^post45 = destflag^post46 propagated equality sourceflag^post45 = sourceflag^post46 propagated equality __lengthofvisited^post45 = edgecount^post46 propagated equality nodecount^post45 = nodecount^post46 propagated equality edgecount^post45 = edgecount^post46 Propagated Equalities Original rule: l28 -> l0 : __lengthofvisited^0'=edgecount^post46, destflag^0'=destflag^post46, edgecount^0'=edgecount^post46, h^0'=h^post46, i^0'=1, j^0'=j^post46, k^0'=k^post46, k_1^0'=k_1^post46, min^0'=min^post46, nodecount^0'=nodecount^post46, sourceflag^0'=sourceflag^post46, (0 == 0 /\ edgecount^0-edgecount^post46 == 0 /\ k_1^0-k_1^post46 == 0 /\ -k^post46+k^0 == 0 /\ min^0-min^post46 == 0 /\ -__lengthofvisited^post46+__lengthofvisited^0 == 0 /\ -nodecount^post46+nodecount^0 == 0 /\ destflag^0-destflag^post46 == 0 /\ -sourceflag^post46+sourceflag^0 == 0 /\ j^0-j^post46 == 0 /\ -h^post46+h^0 == 0 /\ i^0-i^post46 == 0), cost: 1 New rule: l28 -> l0 : __lengthofvisited^0'=edgecount^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 propagated equality edgecount^post46 = edgecount^0 propagated equality k_1^post46 = k_1^0 propagated equality k^post46 = k^0 propagated equality min^post46 = min^0 propagated equality __lengthofvisited^post46 = __lengthofvisited^0 propagated equality nodecount^post46 = nodecount^0 propagated equality destflag^post46 = destflag^0 propagated equality sourceflag^post46 = sourceflag^0 propagated equality j^post46 = j^0 propagated equality h^post46 = h^0 propagated equality i^post46 = i^0 Simplified Guard Original rule: l28 -> l0 : __lengthofvisited^0'=edgecount^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, 0 == 0, cost: 1 New rule: l28 -> l0 : __lengthofvisited^0'=edgecount^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 Removed Trivial Updates Original rule: l28 -> l0 : __lengthofvisited^0'=edgecount^0, destflag^0'=destflag^0, edgecount^0'=edgecount^0, h^0'=h^0, i^0'=1, j^0'=j^0, k^0'=k^0, k_1^0'=k_1^0, min^0'=min^0, nodecount^0'=nodecount^0, sourceflag^0'=sourceflag^0, T, cost: 1 New rule: l28 -> l0 : __lengthofvisited^0'=edgecount^0, i^0'=1, T, cost: 1 Step with 91 Trace 91[T] Blocked [{}, {}] Step with 47 Trace 91[T], 47[T] Blocked [{}, {}, {}] Step with 89 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 48 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T] Blocked [{}, {}, {}, {}, {}] Step with 86 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}] Step with 49 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T] Blocked [{}, {}, {}, {}, {}, {}, {}] Step with 83 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T], 83[(-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {}, {}] Backtrack Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T] Blocked [{}, {}, {}, {}, {}, {}, {83[T]}] Step with 84 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T], 84[(nodecount^0-k^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {83[T]}, {}] Step with 82 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T], 84[(nodecount^0-k^0 <= 0)], 82[T] Blocked [{}, {}, {}, {}, {}, {}, {83[T]}, {}, {}] Step with 57 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T], 84[(nodecount^0-k^0 <= 0)], 82[T], 57[T] Blocked [{}, {}, {}, {}, {}, {}, {83[T]}, {}, {}, {}] Step with 79 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T], 84[(nodecount^0-k^0 <= 0)], 82[T], 57[T], 79[(-i^0+edgecount^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {83[T]}, {}, {}, {}, {}] Step with 65 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T], 84[(nodecount^0-k^0 <= 0)], 82[T], 57[T], 79[(-i^0+edgecount^0 <= 0)], 65[T] Blocked [{}, {}, {}, {}, {}, {}, {83[T]}, {}, {}, {}, {}, {}] Step with 77 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 49[T], 84[(nodecount^0-k^0 <= 0)], 82[T], 57[T], 79[(-i^0+edgecount^0 <= 0)], 65[T], 77[(-k_1^0+edgecount^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {83[T]}, {}, {}, {}, {}, {}, {}] Nonterm Start location: l28 Program variables: __lengthofvisited^0 destflag^0 edgecount^0 h^0 i^0 j^0 k^0 k_1^0 min^0 nodecount^0 sourceflag^0 47: l0 -> l1 : T, cost: 1 89: l1 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 90: l1 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1 48: l2 -> l3 : T, cost: 1 86: l3 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 1 87: l3 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 1 49: l4 -> l5 : T, cost: 1 92: l4 -> LoAT_sink : (-nodecount^0+k^0 >= 0 /\ -1+n >= 0 /\ -edgecount^0 >= 0), cost: NONTERM 93: l4 -> l4 : i^0'=0, k^0'=n+k^0, k_1^0'=0, min^0'=0, (-nodecount^0+k^0 >= 0 /\ -1+n >= 0 /\ -edgecount^0 >= 0), cost: 1 83: l5 -> l26 : (-1+nodecount^0-k^0 <= 0 /\ -1+nodecount^0-k^0 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1 84: l5 -> l25 : nodecount^0-k^0 <= 0, cost: 1 85: l5 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 1 50: l6 -> l7 : k_1^0'=1+k_1^0, T, cost: 1 65: l7 -> l18 : T, cost: 1 51: l8 -> l6 : 1-destflag^0 <= 0, cost: 1 52: l8 -> l6 : 1+destflag^0 <= 0, cost: 1 53: l8 -> l6 : (destflag^0 <= 0 /\ destflag^0 == 0 /\ -destflag^0 <= 0), cost: 1 54: l9 -> l6 : 1-sourceflag^0 <= 0, cost: 1 55: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1 56: l9 -> l8 : (-sourceflag^0 <= 0 /\ -sourceflag^0 == 0 /\ sourceflag^0 <= 0), cost: 1 57: l10 -> l11 : T, cost: 1 79: l11 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 1 80: l11 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 1 58: l12 -> l13 : j^0'=1+j^0, T, cost: 1 88: l13 -> l15 : T, cost: 1 59: l14 -> l12 : T, cost: 1 60: l14 -> l12 : destflag^0'=0, T, cost: 1 61: l14 -> l12 : T, cost: 1 62: l15 -> l9 : nodecount^0-j^0 <= 0, cost: 1 63: l15 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 1 64: l16 -> l17 : j^0'=1+j^0, T, cost: 1 81: l17 -> l20 : T, cost: 1 77: l18 -> l4 : k^0'=1+k^0, -k_1^0+edgecount^0 <= 0, cost: 1 78: l18 -> l22 : h^0'=0, 1+k_1^0-edgecount^0 <= 0, cost: 1 66: l19 -> l16 : T, cost: 1 67: l19 -> l16 : sourceflag^0'=1, T, cost: 1 68: l19 -> l16 : T, cost: 1 69: l20 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 1 70: l20 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 1 71: l21 -> l22 : h^0'=1+h^0, T, cost: 1 74: l22 -> l24 : T, cost: 1 72: l23 -> l21 : min^0'=h^0, T, cost: 1 73: l23 -> l21 : T, cost: 1 75: l24 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1 76: l24 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 1 82: l25 -> l10 : i^0'=0, min^0'=0, T, cost: 1 91: l28 -> l0 : __lengthofvisited^0'=edgecount^0, i^0'=1, T, cost: 1 Certificate of Non-Termination Original rule: l4 -> l4 : i^0'=0, k^0'=1+k^0, k_1^0'=0, min^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 1 New rule: l4 -> LoAT_sink : (-nodecount^0+k^0 >= 0 /\ -1+n >= 0 /\ -edgecount^0 >= 0), cost: NONTERM -nodecount^0+k^0 >= 0 [0]: monotonic increase yields -nodecount^0+k^0 >= 0 -edgecount^0 >= 0 [0]: monotonic increase yields -edgecount^0 >= 0 Replacement map: {-nodecount^0+k^0 >= 0 -> -nodecount^0+k^0 >= 0, -edgecount^0 >= 0 -> -edgecount^0 >= 0} Loop Acceleration Original rule: l4 -> l4 : i^0'=0, k^0'=1+k^0, k_1^0'=0, min^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 1 New rule: l4 -> l4 : i^0'=0, k^0'=n+k^0, k_1^0'=0, min^0'=0, (-nodecount^0+k^0 >= 0 /\ -1+n >= 0 /\ -edgecount^0 >= 0), cost: 1 -nodecount^0+k^0 >= 0 [0]: monotonic increase yields -nodecount^0+k^0 >= 0 -edgecount^0 >= 0 [0]: monotonic increase yields -edgecount^0 >= 0 Replacement map: {-nodecount^0+k^0 >= 0 -> -nodecount^0+k^0 >= 0, -edgecount^0 >= 0 -> -edgecount^0 >= 0} Step with 92 Trace 91[T], 47[T], 89[(-i^0+nodecount^0 <= 0)], 48[T], 86[(-1-i^0+nodecount^0 <= 0)], 92[(-nodecount^0+k^0 >= 0 /\ -1+n >= 0 /\ -edgecount^0 >= 0)] Blocked [{}, {}, {}, {}, {}, {}, {92[T]}] Refute Counterexample [ __lengthofvisited^0=0 destflag^0=0 edgecount^0=0 h^0=0 i^0=1 j^0=0 k^0=0 k_1^0=0 min^0=0 nodecount^0=0 sourceflag^0=0 ] 91 [ __lengthofvisited^0=0 destflag^0=0 edgecount^0=0 h^0=0 i^0=1 j^0=0 k^0=0 k_1^0=0 min^0=0 nodecount^0=0 sourceflag^0=0 ] 47 [ __lengthofvisited^0=0 destflag^0=0 edgecount^0=0 h^0=0 i^0=0 j^0=0 k^0=0 k_1^0=0 min^0=0 nodecount^0=0 sourceflag^0=0 ] 89 [ __lengthofvisited^0=0 destflag^0=0 edgecount^0=0 h^0=0 i^0=0 j^0=0 k^0=0 k_1^0=0 min^0=0 nodecount^0=0 sourceflag^0=0 ] 48 [ __lengthofvisited^0=0 destflag^0=0 edgecount^0=0 h^0=0 i^0=0 j^0=0 k^0=0 k_1^0=0 min^0=0 nodecount^0=0 sourceflag^0=0 ] 86 [ __lengthofvisited^0=__lengthofvisited^0 destflag^0=0 edgecount^0=0 h^0=0 i^0=i^0 j^0=0 k^0=0 k_1^0=0 min^0=0 nodecount^0=0 sourceflag^0=0 ] 92 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b