diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index fb644a0f70ca24b7b1714e2611c9087bb86abb3f..db72d3ac6311cc746a454c6d0dd5598e4c2fb39b 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -892,6 +892,36 @@ struct
     | Ltype _ | Linteger | Lreal | Lvar _ | Larrow _ ->
       C.error loc "not a C type"
 
+  let parseInt loc s =
+    let explode s =
+      let l = ref [] in
+      String.iter (fun c -> l:=Int64.of_int (Char.code c) :: !l) s;
+      List.rev !l
+    in
+    match String.get s 0 with
+    | 'L' -> (* L'wide_char' *)
+      let content = String.sub s 2 (String.length s - 3) in
+      let tokens = explode content in
+      let value = Cil.reduce_multichar Cil.theMachine.Cil.wcharType tokens
+      in
+      tinteger_s64 ~loc value
+    | '\'' -> (* 'char' *)
+      let content = String.sub s 1 (String.length s - 2) in
+      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
+
+  let find_logic_label loc env l =
+    try Lenv.find_logic_label l env
+    with Not_found ->
+    (* look for a C label *)
+    try
+      let lab = C.find_label l in
+      StmtLabel lab
+    with Not_found ->
+      C.error loc "logic label `%s' not found" l
+
   let logic_type ctxt loc env t =
     (* force calls to go through ctxt *)
     let module [@warning "-60"] C = struct end in
@@ -904,7 +934,12 @@ struct
     | LTarray (ty,length) ->
       let size = match length with
         | ASnone -> None
-        | ASinteger s -> Some (parseIntExp ~loc s)
+        | ASinteger s ->
+          let t = parseInt loc s in
+          (match t.term_node with
+           | TConst lconst ->
+             Some (new_exp ~loc (Const (lconstant_to_constant lconst)))
+           | _ -> Kernel.fatal ~loc "integer literal not parsed as constant")
         | ASidentifier s ->
           let size = ctxt.type_term ctxt env
               {lexpr_node=PLvar(s);lexpr_loc=loc} in
@@ -1907,36 +1942,6 @@ struct
 
   (* Typing terms *)
 
-  let parseInt loc s =
-    let explode s =
-      let l = ref [] in
-      String.iter (fun c -> l:=Int64.of_int (Char.code c) :: !l) s;
-      List.rev !l
-    in
-    match String.get s 0 with
-    | 'L' -> (* L'wide_char' *)
-      let content = String.sub s 2 (String.length s - 3) in
-      let tokens = explode content in
-      let value = Cil.reduce_multichar Cil.theMachine.Cil.wcharType tokens
-      in
-      tinteger_s64 ~loc value
-    | '\'' -> (* 'char' *)
-      let content = String.sub s 1 (String.length s - 2) in
-      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
-
-  let find_logic_label loc env l =
-    try Lenv.find_logic_label l env
-    with Not_found ->
-    (* look for a C label *)
-    try
-      let lab = C.find_label l in
-      StmtLabel lab
-    with Not_found ->
-      C.error loc "logic label `%s' not found" l
-
   let find_old_label loc env =
     try Lenv.find_logic_label "Old" env
     with Not_found ->
diff --git a/tests/spec/oracle/qarrsize.res.oracle b/tests/spec/oracle/qarrsize.res.oracle
index d5b9c2f7b0099744a28564af333132057d53d1fe..093a9470ebbf0e1df7d673557bcdca82d209de80 100644
--- a/tests/spec/oracle/qarrsize.res.oracle
+++ b/tests/spec/oracle/qarrsize.res.oracle
@@ -3,14 +3,17 @@
 int a[0xFFu];
 int b[128L];
 int c[0x8A];
+int d['r'];
 int sa = (int)sizeof(int [0xFFu]);
 int sb = (int)sizeof(int [128L]);
 int sc = (int)sizeof(int [0x8A]);
+int sd = (int)sizeof(int ['r']);
 /*@ requires \valid(n + (0 .. sizeof(int [0xFFu])));
     requires \valid(p + (0 .. sizeof(int [128L])));
     requires \valid(q + (0 .. sizeof(int [0x8A])));
+    requires \valid(r + (0 .. sizeof(int ['r'])));
     assigns \nothing;
  */
-void f(int *n, int *p, int *q);
+void f(int *n, int *p, int *q, int *r);
 
 
diff --git a/tests/spec/qarrsize.c b/tests/spec/qarrsize.c
index 50c0f886d779b4e1d760cf5e65bcd90574b50f46..169f12ed03882499ea1726968ebd3e74fedaf895 100644
--- a/tests/spec/qarrsize.c
+++ b/tests/spec/qarrsize.c
@@ -3,23 +3,28 @@
 #define N 0xFFu
 #define P 128L
 #define Q 0x8A
+#define R 'r'
 
 int a[N];
 int b[P];
 int c[Q];
+int d[R];
 
 typedef int Ta[N];
 typedef int Tb[P];
 typedef int Tc[Q];
+typedef int Td[R];
 
 int sa = sizeof(int[N]);
 int sb = sizeof(int[P]);
 int sc = sizeof(int[Q]);
+int sd = sizeof(int[R]);
 
 /*@
   requires \valid(n + (0 .. sizeof(int[N])));
   requires \valid(p + (0 .. sizeof(int[P])));
   requires \valid(q + (0 .. sizeof(int[Q])));
+  requires \valid(r + (0 .. sizeof(int[R])));
   assigns \nothing;
  */
-void f(int *n, int *p, int *q);
+void f(int *n, int *p, int *q, int* r);