diff --git a/src/dinitz.h b/src/dinitz.h
index 00a5ca33e9abf0783d241230bea9e30ef7045a8f..030a7c725ccb4982bf74be949ab4081751923f71 100644
--- a/src/dinitz.h
+++ b/src/dinitz.h
@@ -38,7 +38,7 @@ void popHead(Node **head_ref);
 int BFS(int start, int end, double **graph, int *levels);
 
 
-/*@ requires 0 <= cur <= end && end >= 0 && end <= 300000;
+/*@ requires 0 <= cur <= end && end >= 0 && end < 300000;
   @ requires 0 <= flow <= DBL_MAX;
   @ requires graph != \null && \valid(levels + (0..end)) && \valid(visited + (0..end));
   @ requires \forall int i; 0 <= i <= end ==> \valid(graph[i] + (0..end));