Assume loop increments by one if increment cannot be found by heuristics

goblint · Jun 19, 2024 · 9bfe815 · 9bfe815
1 parent ae2d9d5
commit 9bfe815
Showing 1 changed file with 5 additions and 1 deletion.
diff --git 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 "";