Update dinitz.h

src/dinitz.h

@@ -33,7 +33,7 @@ void popHead(Node **head_ref);
   @ ensures \result == 0 || \result == 1;
   @ ensures \forall int i; 0 <= i <= end ==> levels[i] >= -1 && levels[i] <= end;
   @ ensures \forall int i; 0 <= i <= end && levels[i] == -1 ==> (\forall int j; 0 <= j <= end && levels[j] != -1 ==> graph[j][i] == 0.0 && graph[i][j] == 0.0);
-  @ ensures levels[end] > 0 ==> (\forall int i; 0 <= i < levels[end]; \exists int j, int k; 0 <= j <= end && 0 <= k <= end && levels[j] == i && levels[k] == i + 1 && graph[j][k] > 0);
+  @ ensures levels[end] > 0 ==> (\forall int i; \exists int j; \exists int k; 0 <= i < levels[end] && 0 <= j <= end && 0 <= k <= end && (levels[j] == i && levels[k] == i + 1) && graph[j][k] > 0);
   @*/
 int BFS(int start, int end, double **graph, int *levels);