From 2bd488436b6ee55824b484aa8ffd9e690eb3627b Mon Sep 17 00:00:00 2001
From: Michal Patera <patermi2@fit.cvut.cz>
Date: Wed, 10 May 2023 21:29:22 +0200
Subject: [PATCH] Update dinitz.h

---
 src/dinitz.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/dinitz.h b/src/dinitz.h
index 00a5ca3..030a7c7 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));
-- 
GitLab