diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 75665dec0631f0844c434e7dacb8be41d85acee8..b5b1e8e6c8f05c82a117622a8d76381f1b1c85d5 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -10104,7 +10104,11 @@ and doStatement local_env (s : Cabs.statement) : chunk =
     in
     if il > ih then Kernel.error ~once:true ~current:true "Empty case range";
     let rec mkAll (i: int) =
-      if i > ih then [] else integer ~loc i :: mkAll (i + 1)
+      if i > ih then [] else
+      if ih - i > 100_000 then
+        Kernel.fatal ~current:true "Case range too large"
+      else
+        integer ~loc i :: mkAll (i + 1)
     in
     (sel @@ (seh,ghost)) @@
     (caseRangeChunk ~ghost (mkAll il) loc' (doStatement local_env s),
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index db573af932d7288a94e547a1e729ad2581a7c585..1cba593f0dce09c90a5f83f9c00ee9a0bca5a655 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:22: User Error: 
-  integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
 [kernel] tests/syntax/very_large_integers.c:23: User Error: 
+  integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
+[kernel] tests/syntax/very_large_integers.c:24: User Error: 
   bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: 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 23cfa866c0b1679b16c8da7e786139aeb6c49151..29f4d99b92870d25cf2e6d7e3c30eade2e4853ad 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:29: User Error: 
+[kernel] tests/syntax/very_large_integers.c:30: User Error: 
   Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:29: User Error: 
+[kernel] tests/syntax/very_large_integers.c:30: User Error: 
   Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: 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.10.res.oracle b/tests/syntax/oracle/very_large_integers.10.res.oracle
index b3e0404db43f656f65b325add1731256c9096eb1..b9200fafcf732ad23e1790a1244f683c4077eb89 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,12 +1,15 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:82: Warning: 
-  Invalid slevel directive. Ignoring code annotation
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  nondet ∈ [--..--]
+[kernel:annot-error] tests/syntax/very_large_integers.c:86: Warning: 
+  invalid loop unrolling parameter (-9999999999999999999); ignoring
 [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
-  '-kernel-msg-key pp' for preprocessing command.
 [kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index bb2ebf80688d97434727e1ff7e6f7bf40855006a..650607ffad8afa91c6601c4fc79e3dc5b5c3d1d9 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -1,11 +1,12 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:86: User Error: 
-  Invalid digit 9 in integer literal '09' in base 8.
+[kernel:annot-error] tests/syntax/very_large_integers.c:91: 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
   '-kernel-msg-key pp' for preprocessing command.
 [kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.12.res.oracle b/tests/syntax/oracle/very_large_integers.12.res.oracle
index db0893a7e07ec6d5c67210f1b2438ffbd77663ef..ba0dd7c26f203cbaa3c59a884191c006248d1ba9 100644
--- a/tests/syntax/oracle/very_large_integers.12.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
@@ -1,22 +1,11 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:91: 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;
-}
-
-
+[kernel] tests/syntax/very_large_integers.c:95: User Error: 
+  Invalid digit 9 in integer literal '09' in base 8.
+[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.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..29b15f32902d4b08969c58c31fb240c3e12a0fb0
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
+  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
+  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+                                                   (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:100: 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/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index bb5f47fe756242bc9ba320bc6435621eb289b4e1..25740fed33da86b20117393d4a25f8919e975238 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:36: User Error: 
+[kernel] tests/syntax/very_large_integers.c:37: User Error: 
   integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:36: Failure: 
+[kernel] tests/syntax/very_large_integers.c:37: 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 ad9de534b05aef91ec8a722ad0b193c72ef89375..f4cbe4f4e6d14e2acf9f68cbbcc46c39d8f90a12 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,6 +1,5 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:41: Failure: 
-  Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
+[kernel] tests/syntax/very_large_integers.c:45: Failure: Case range too large
 [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.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index 0d8599e32958e49f9a178eaa551bc2692388d0cb..e53651c2f5bff8cd11135c4216465253a4faf8c0 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,12 +1,6 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:45: User Error: 
-  INDEX initialization designator overflows
-  43    
-  44    #ifdef INIT_DESIGNATOR2
-  45    int arr3[1] = { [9999999999999999999U] = 42 };
-        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  46    #endif
-  47
+[kernel] tests/syntax/very_large_integers.c:50: 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.
 [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 1798bfe46e3610238348f88b53f77a757bb82440..028afa06f27e1524caf054410fd66a022790e970 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,10 +1,12 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:49: User Error: 
-  integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:49: User Error: 
-  integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:49: Failure: 
-  INDEX_RANGE initialization designator is not a valid constant
+[kernel] tests/syntax/very_large_integers.c:54: User Error: 
+  INDEX initialization designator overflows
+  52    
+  53    #ifdef INIT_DESIGNATOR2
+  54    int arr3[1] = { [9999999999999999999U] = 42 };
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  55    #endif
+  56
 [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.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index c531dfb15a1f18822fb312d21c18796860aae437..80ea4f9cf539e9e3643304efad8bd4760c7ffb06 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -1,11 +1,10 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:53: User Error: 
-  Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
-  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
-  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
-                                                   (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:58: User Error: 
+  integer constant too large in expression -9999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:58: User Error: 
+  integer constant too large in expression 9999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:58: 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.
 [kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 75dbebc66e69abf8a3bedb63843d538f6957ce7c..c998aaf5b33f994a1864b4fe96397055cc29680c 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,10 +1,11 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:62: User Error: 
+  Invalid attribute constant: 0x80000000000000000
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
 [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.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
index a0898661e147feeff6bc975032c9c15c8f0f9fd0..1028d33119a6f9eb712dfddbf7ec633b15687f19 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,11 +1,10 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:71: Failure: 
-  Invalid digit 9 in integer literal '09876543210' in base 8.
+[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
 [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.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index 3c17088f9595e1ee98d654797a24d9cf13396958..bcf3568e2a81f29b18bf9151dbacbf558a0d1890 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,15 +1,11 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning: 
+[kernel] tests/syntax/very_large_integers.c:67: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  nondet ∈ [--..--]
-[kernel:annot-error] tests/syntax/very_large_integers.c:77: Warning: 
-  invalid loop unrolling parameter (-9999999999999999999); ignoring
-[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] tests/syntax/very_large_integers.c:80: Failure: 
+  Invalid digit 9 in integer literal '09876543210' in base 8.
+[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/very_large_integers.c b/tests/syntax/very_large_integers.c
index 8cb37536c37aab5108ce98b5c98db5b3895a3953..47c3629e67cfda6cca3d3f839734c8ae167c29dd 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -4,6 +4,7 @@
    STDOPT: #"-cpp-extra-args=-DBITFIELD"
    STDOPT: #"-cpp-extra-args=-DARRAY_DECL"
    STDOPT: #"-cpp-extra-args=-DCASE_RANGE"
+   STDOPT: #"-cpp-extra-args=-DCASE_RANGE2"
    STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR"
    STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2"
    STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
@@ -34,6 +35,14 @@ unsigned long nondetul;
 void case_range() {
   switch (nondetul)
   case 0 ... 9999999999999999999U:;
+  case 0 ... 199999999999999999U:;
+}
+#endif
+
+#ifdef CASE_RANGE2
+void case_range() {
+  switch (nondet)
+  case 0 ... 10000000U:;
 }
 #endif