Update dinitz.h

src/dinitz.h

@@ -43,7 +43,7 @@ int BFS(int start, int end, double **graph, int *levels);
   @ requires graph != \null && \valid(levels + (0..end)) && \valid(visited + (0..end));
   @ requires \forall int i; 0 <= i <= end ==> \valid(graph[i] + (0..end));
   @ assigns visited[0..end], graph[0..end][0..end];
-  @ ensures \result >= 0.0 && (\result > 0.0 ==> (\forall int i; 0 <= i <= end ==> (graph[cur][i] <= \old(graph[cur][i]) && graph[i][cur] >= \old(graph[i][cur]))));
+  @ ensures \result >= 0.0 && (\result > 0.0 ==> (\forall int i; 0 <= i <= end ==> graph[cur][i] <= \old(graph[cur][i])));
   @*/
 double DFS(int cur, int end, double **graph, int *levels, int *visited, double flow);