diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 44868650b2fe56cbef8ca546f02e4993bed86486..9ba74c0138586be05ed753b6447cf06fd8917f74 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -880,7 +880,11 @@ struct
       let tokens = explode content in
       let value,_= Cil.interpret_character_constant tokens in
       term ~loc (TConst (constant_to_lconstant value)) Linteger
-    | _ -> Cil.parseIntLogic ~loc s
+    | _ ->
+      try
+        Cil.parseIntLogic ~loc s
+      with Cil.ParseIntError msg ->
+        Kernel.fatal ~source:(fst loc) "%s" msg
 
   let find_logic_label loc env l =
     try Lenv.find_logic_label l env
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index e568ddfc6aa1980f10b3d288ff3378fd865161f2..6cc3eae47434dd59d302d80b6cf8a52ba20823af 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -275,7 +275,15 @@ let constant_to_lconstant c = match c with
     LReal (real_of_float s f)
 
 let lconstant_to_constant c = match c with
-  | Integer (i,s) -> CInt64(i,Cil.intKindForValue i false,s)
+  | Integer (i,s) ->
+    begin
+      try
+        CInt64(i,Cil.intKindForValue i false,s)
+      with Cil.Not_representable ->
+        Kernel.fatal
+          "Cannot represent logical integer in C: %a"
+          (Integer.pretty ~hexa:false) i
+    end
   | LStr s -> CStr s
   | LWStr s -> CWStr s
   | LChr s -> CChr s
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index d7175f1e68f8886db5b823229062912e02a127ff..64ae83250fee7836a6a4c7702d1a64e0a85f35c8 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:18: User Error: 
+[kernel] tests/syntax/very_large_integers.c:21: User Error: 
   integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] tests/syntax/very_large_integers.c:19: User Error: 
+[kernel] tests/syntax/very_large_integers.c:22: User Error: 
   bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: 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 43f59ecb36a0bf51cd45b43e9d3ca7cae94cd35a..4c65204b2faa18b302bd50ba561aa4192227fcfe 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:25: User Error: 
+[kernel] tests/syntax/very_large_integers.c:28: User Error: 
   Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:25: User Error: 
+[kernel] tests/syntax/very_large_integers.c:28: User Error: 
   Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: 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
new file mode 100644
index 0000000000000000000000000000000000000000..a1176c2d521a2b0a257355922262475a6377318f
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
+  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
+  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+                                                   (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:85: 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 c21f3361baa4e87f77be7040bdc76355390d0145..2c763bf0674a6ffdacdab5d440e40387fc57f8d4 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:31: User Error: 
+[kernel] tests/syntax/very_large_integers.c:35: User Error: 
   integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:31: Failure: 
+[kernel] tests/syntax/very_large_integers.c:35: 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 39820b9d4cdca3ba177ff7560926ff726cb2bd0b..ac927237baf7cd2545380697b69b2d9851652cb9 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:36: Failure: 
+[kernel] tests/syntax/very_large_integers.c:40: 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 d93cd65fdee263baffac8383660f9daa89a7a4b6..403d2a65c2fd6968e35a53798b038a69496b277a 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:40: User Error: 
+[kernel] tests/syntax/very_large_integers.c:44: User Error: 
   INDEX initialization designator overflows
-  38    
-  39    #ifdef INIT_DESIGNATOR2
-  40    int arr3[1] = { [9999999999999999999U] = 42 };
+  42    
+  43    #ifdef INIT_DESIGNATOR2
+  44    int arr3[1] = { [9999999999999999999U] = 42 };
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  41    #endif
-  42
+  45    #endif
+  46
 [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 1de406bf2a6718338b06ad73b46bcf3b4249351b..46e43a1bedb0f44f1df6c29b995ed20d738f5336 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:44: User Error: 
+[kernel] tests/syntax/very_large_integers.c:48: User Error: 
   integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:44: User Error: 
+[kernel] tests/syntax/very_large_integers.c:48: User Error: 
   integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:44: Failure: 
+[kernel] tests/syntax/very_large_integers.c:48: 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 2518a170b6ff92fdfb61389d9dee248f4d9d7376..45af4ca20329ffc5985135901f421f33a18a7840 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:48: User Error: 
+[kernel] tests/syntax/very_large_integers.c:52: User Error: 
   Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: 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 18a61c349976753a791af005be76160b24de38a4..e34bb47c39d686dfebced25abf93180bbe7fdad9 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,12 +1,10 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[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] 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 9d4810ae44411318b1e001fe542c98a7f68acc31..0f63c2ee5d2cbc3743a4b735455ceee727102006 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,22 +1,11 @@
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:53: Warning: 
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[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;
-}
-
-
+[kernel] tests/syntax/very_large_integers.c:70: 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/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..95d122b7737555edb536980e820d1f4672e217e2
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
+  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:57: Warning: 
+  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+                                                   (9223372036854775808) )
+[kernel:annot-error] tests/syntax/very_large_integers.c:79: 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/very_large_integers.c b/tests/syntax/very_large_integers.c
index 4831ada7bc1e0c1e6f8179b45a49b6456a8eac21..48dff8b8376d5f74f2bd3698b2994a1420901286 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -8,10 +8,13 @@
    STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2"
    STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
    STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT"
+   STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT"
+   STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
    STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva"
    EXIT: 0
    STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
 */
+
 volatile int nondet;
 
 #ifdef BITFIELD
@@ -24,6 +27,7 @@ struct st {
 int arr[9999999999999999999U+18000000000000000000U];
 char arr1[99999999999999999999U];
 #endif
+
 #ifdef CASE_RANGE
 unsigned long nondetul;
 void case_range() {
@@ -58,6 +62,14 @@ typedef struct {
 
 //@ logic integer too_large_integer = 9999999999999999999;
 
+#ifdef LOGIC_CONSTANT
+//@ type too_large_logic_array = int[9999999999999999999U];
+#endif
+
+#ifdef LOGIC_CONSTANT_OCTAL
+//@ type too_large_logic_array_octal = int[09876543210];
+#endif
+
 int main() {
 #ifdef EVA_UNROLL
   //@ loop unroll (-9999999999999999999); // IntLimit