Update dinitz.c

src/dinitz.c

@@ -25,7 +25,7 @@ void popHead(Node** head_ref) {
 int BFS(int start, int end, double **graph, int *levels){
-    /*@ loop invariant 0 <= i <= end;
+    /*@ loop invariant 0 <= i <= end + 1;
       @ loop invariant \forall int j; 0 <= j < i ==> levels[j] == -1;
       @ loop assigns i, levels[0..end];
       @ loop variant end - i;
@@ -44,7 +44,7 @@ int BFS(int start, int end, double **graph, int *levels){
     while(queueHead != NULL){
         cur = queueHead->data;
         popHead(&queueHead);
-        /*@ loop invariant \forall int i; 0 <= i <= end ==> levels[i] >= -1 && levels[i] <= end;
+        /*@ loop invariant \forall int i; 0 <= i <= end + 1 ==> levels[i] >= -1 && levels[i] <= end;
           @ loop assigns queueHead, levels[0..end];
           @*/
         for (int i = 0; i <= end; ++i) {