diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index c60b1bb3b5a46aa9c4d125df8c79cf05d8de77db..e09cbae6a55f438c37032b0cf60ea5a332178db9 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -51,7 +51,14 @@ let update_info global_find_init emitter info spec =
           in
           let i = Logic_utils.constFoldTermToInt t in
           match i with
-          | Some i -> { info with unroll_number = Some (Integer.to_int i) }
+          | Some i ->
+            begin
+              match Integer.to_int_opt i with
+              | Some _ as unroll_number -> { info with unroll_number }
+              | None -> Kernel.abort ~current:true
+                          "count too large in unrolling directive: %a"
+                          (Integer.pretty ~hexa:false) i
+            end
           | None ->
             Kernel.warning ~once:true ~current:true
               "ignoring unrolling directive (not an understood constant \