From 9bfe815dd45800cd0fb44a419e7c10cd19346e3b Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 19 Jun 2024 19:07:12 +0300
Subject: [PATCH] Assume loop increments by one if increment cannot be found by
 heuristics

---
 src/util/loopUnrolling.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index c1a6a9238f..301ab49b4d 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -264,7 +264,11 @@ let fixedLoopSize loopStatement func =
     None
   else
     constBefore var loopStatement func >>= fun start ->
-    assignmentDifference (loopBody loopStatement) var >>= fun diff ->
+    let diff =
+      match assignmentDifference (loopBody loopStatement) var with
+      | Some d -> d
+      | None -> Z.one (* When we find a fixed loop and its start, but cannot detect the increment within the loop, we assume the increment is 1 *)
+    in
     Logs.debug "comparison: ";
     Pretty.fprint stderr (dn_exp () comparison) ~width:max_int;
     Logs.debug "";