diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index e09cbae6a55f438c37032b0cf60ea5a332178db9..89c96fbb3a542cb595dd29918779d84587c6ce5e 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -50,15 +50,8 @@ let update_info global_find_init emitter info spec =
               (new Logic_utils.simplify_const_lval global_find_init) spec
           in
           let i = Logic_utils.constFoldTermToInt t in
-          match i with
-          | 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
+          match Option.bind i Integer.to_int_opt with
+          | Some _ as unroll_number -> { info with unroll_number }
           | None ->
             Kernel.warning ~once:true ~current:true
               "ignoring unrolling directive (not an understood constant \
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index a13d814a1d9743ba27c99c5dcc0b25cd2982acc5..d7175f1e68f8886db5b823229062912e02a127ff 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,11 +1,11 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:16: User Error: 
+[kernel] tests/syntax/very_large_integers.c:18: User Error: 
   integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] tests/syntax/very_large_integers.c:17: User Error: 
+[kernel] tests/syntax/very_large_integers.c:19: User Error: 
   bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 63275ad53b54bd590855fb9c73dc723478aef24d..53fe76c37f3be3de790eaf9a496c2a1896db9416 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -1,11 +1,11 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:23: User Error: 
+[kernel] tests/syntax/very_large_integers.c:25: User Error: 
   invalid integer constant: 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:23: User Error: 
+[kernel] tests/syntax/very_large_integers.c:25: User Error: 
   invalid integer constant: 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index 9a759fcdc0c8ff6e1a98cc50429ca48238ca77b5..c21f3361baa4e87f77be7040bdc76355390d0145 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -1,7 +1,7 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:29: User Error: 
+[kernel] tests/syntax/very_large_integers.c:31: User Error: 
   integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:29: Failure: 
+[kernel] tests/syntax/very_large_integers.c:31: Failure: 
   Cannot understand the constants in case range
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
index 0888626b7497711ce706b6e26a34891a183770b6..39820b9d4cdca3ba177ff7560926ff726cb2bd0b 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:34: Failure: 
+[kernel] tests/syntax/very_large_integers.c:36: Failure: 
   Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index cb0367c4b375bcce776bfaac338625fd7a7a0d04..d93cd65fdee263baffac8383660f9daa89a7a4b6 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,12 +1,12 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:38: User Error: 
+[kernel] tests/syntax/very_large_integers.c:40: User Error: 
   INDEX initialization designator overflows
-  36    
-  37    #ifdef INIT_DESIGNATOR2
-  38    int arr3[1] = { [9999999999999999999U] = 42 };
+  38    
+  39    #ifdef INIT_DESIGNATOR2
+  40    int arr3[1] = { [9999999999999999999U] = 42 };
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  39    #endif
-  40
+  41    #endif
+  42
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.
 [kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index bf735cd8f5c4268e5c3e34351878cb45b103c793..1de406bf2a6718338b06ad73b46bcf3b4249351b 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,9 +1,9 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:42: User Error: 
+[kernel] tests/syntax/very_large_integers.c:44: User Error: 
   integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:42: User Error: 
+[kernel] tests/syntax/very_large_integers.c:44: User Error: 
   integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:42: Failure: 
+[kernel] tests/syntax/very_large_integers.c:44: Failure: 
   INDEX_RANGE initialization designator is not a valid constant
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index fee0f227bcfae4befb054abbc847bc7c7dd9fc1c..2518a170b6ff92fdfb61389d9dee248f4d9d7376 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -1,9 +1,9 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:46: User Error: 
+[kernel] tests/syntax/very_large_integers.c:48: User Error: 
   Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 77ad998c981f4bf1eb5e313dcf4aaf2e597f179c..18a61c349976753a791af005be76160b24de38a4 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,10 +1,10 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:65: Warning: 
+[kernel:annot-error] tests/syntax/very_large_integers.c:67: Warning: 
   Invalid slevel directive. Ignoring code annotation
 [kernel] User Error: warning annot-error treated as fatal error.
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
index fe4bc11e18b18965d72ee7bc06f5cc8db92a2c9f..9d4810ae44411318b1e001fe542c98a7f68acc31 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,9 +1,22 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:71: User Error: 
-  count too large in unrolling directive: 99999999999999999999
-[kernel] Frama-C aborted: invalid user input.
+[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+  ignoring unrolling directive (not an understood constant expression)
+/* Generated by Frama-C */
+int volatile nondet;
+/*@ logic ℤ too_large_integer= 9999999999999999999;
+ */
+int main(void)
+{
+  int __retres;
+  /*@ loop pragma UNROLL 99999999999999999999; */
+  while (nondet) ;
+  __retres = 0;
+  return __retres;
+}
+
+
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 8c6bac17a68db5cce352215e78d90db92c1c4854..4831ada7bc1e0c1e6f8179b45a49b6456a8eac21 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -1,4 +1,5 @@
 /* run.config
+   PLUGIN: @EVA_PLUGINS@
    EXIT: 1
    STDOPT: #"-cpp-extra-args=-DBITFIELD"
    STDOPT: #"-cpp-extra-args=-DARRAY_DECL"
@@ -8,6 +9,7 @@
    STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
    STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT"
    STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva"
+   EXIT: 0
    STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
 */
 volatile int nondet;