diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index d31c8c679e07a341b20cddc5c021497c6a766392..c16497fde988313e85ab2038b2e81518e5c989a1 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -367,17 +367,17 @@ rule token = parse
       end else curr_tok
     }
 
-  | '0'['x''X'] rH+ rIS?    { CONSTANT (IntConstant (lexeme lexbuf)) }
-  | '0'['b''B'] rB+ rIS?    { CONSTANT (IntConstant (lexeme lexbuf)) }
-  | '0' rD+ rIS?            { CONSTANT (IntConstant (lexeme lexbuf)) }
-  | rD+                     { CONSTANT10 (lexeme lexbuf) }
-  | rD+ rIS                 { CONSTANT (IntConstant (lexeme lexbuf)) }
+  | '0'['x''X'] rH+ rIS?    { INT_CONSTANT (lexeme lexbuf) }
+  | '0'['b''B'] rB+ rIS?    { INT_CONSTANT (lexeme lexbuf) }
+  | '0' rD+ rIS?            { INT_CONSTANT (lexeme lexbuf) }
+  | rD+                     { INT_CONSTANT (lexeme lexbuf) }
+  | rD+ rIS                 { INT_CONSTANT (lexeme lexbuf) }
   | ('L'? "'" as prelude) (([^ '\\' '\'' '\n']|("\\"[^ '\n']))+ as content) "'"
       {
         let b = Buffer.create 5 in
         Buffer.add_string b prelude;
         let lbf = Lexing.from_string content in
-        CONSTANT (IntConstant (chr b lbf ^ "'"))
+        INT_CONSTANT (chr b lbf ^ "'")
       }
 (* floating-point literals, both decimal and hexadecimal *)
   | rD+ rE rFS?
@@ -386,11 +386,11 @@ rule token = parse
   | '0'['x''X'] rH+ '.' rH* rP rFS?
   | '0'['x''X'] rH* '.' rH+ rP rFS?
   | '0'['x''X'] rH+ rP rFS?
-      { CONSTANT (FloatConstant (lexeme lexbuf)) }
+      { FLOAT_CONSTANT (lexeme lexbuf) }
 
  (* hack to lex 0..3 as 0 .. 3 and not as 0. .3 *)
   | (rD+ as n) ".."         { lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos - 2;
-                              CONSTANT (IntConstant n) }
+                              INT_CONSTANT n }
 
   | 'L'? '"' as prelude (([^ '\\' '"' '\n']|("\\"[^ '\n']))* as content) '"'
       { STRING_LITERAL (prelude.[0] = 'L',content) }
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 8a41fe69f4f24827622a3d4d6c56ed638821d3eb..ab09ffd36dc9e10884f4729b907dab1ae1e7ad68 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -264,8 +264,10 @@
 /* ACSL extension for external spec  file */
 %token <string> IDENTIFIER TYPENAME
 %token <bool*string> STRING_LITERAL
-%token <Logic_ptree.constant> CONSTANT
-%token <string> CONSTANT10
+%token <string> INT_CONSTANT
+%token <string> FLOAT_CONSTANT
+%token <string> STRING_CONSTANT
+%token <string> WSTRING_CONSTANT
 %token LPAR RPAR IF ELSE COLON COLON2 COLONCOLON DOT DOTDOT DOTDOTDOT
 %token INT INTEGER REAL BOOLEAN BOOL FLOAT LT GT LE GE EQ NE COMMA ARROW EQUAL
 %token FORALL EXISTS IFF IMPLIES AND OR NOT SEPARATED
@@ -678,12 +680,14 @@ var_spec:
 ;
 
 constant:
-| CONSTANT   { $1 }
-| CONSTANT10 { IntConstant $1 }
+| INT_CONSTANT   { IntConstant $1 }
+| FLOAT_CONSTANT { FloatConstant $1 }
+| STRING_CONSTANT { StringConstant $1 }
+| WSTRING_CONSTANT { WStringConstant $1 }
 ;
 
 array_size:
-| CONSTANT10 { ASinteger $1 }
+| INT_CONSTANT { ASinteger $1 }
 | identifier { ASidentifier $1 }
 | /* empty */ { ASnone }
 ;
@@ -1040,7 +1044,7 @@ ext_contract_markup:
 
 stmt_markup:
 | any_identifier { $1 }
-| CONSTANT10 { $1 }
+| INT_CONSTANT { $1 }
 ;
 
 stmt_markup_attr:
@@ -2041,8 +2045,10 @@ wildcard:
 | COLON2 { () }
 | COLONCOLON { () }
 | COMMA { () }
-| CONSTANT { () }
-| CONSTANT10 { () }
+| INT_CONSTANT { () }
+| FLOAT_CONSTANT { () }
+| STRING_CONSTANT { () }
+| WSTRING_CONSTANT { () }
 | DOLLAR { () }
 | DOT { () }
 | DOTDOT { () }
diff --git a/tests/spec/oracle/qarrsize.res.oracle b/tests/spec/oracle/qarrsize.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d5b9c2f7b0099744a28564af333132057d53d1fe
--- /dev/null
+++ b/tests/spec/oracle/qarrsize.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing tests/spec/qarrsize.c (with preprocessing)
+/* Generated by Frama-C */
+int a[0xFFu];
+int b[128L];
+int c[0x8A];
+int sa = (int)sizeof(int [0xFFu]);
+int sb = (int)sizeof(int [128L]);
+int sc = (int)sizeof(int [0x8A]);
+/*@ requires \valid(n + (0 .. sizeof(int [0xFFu])));
+    requires \valid(p + (0 .. sizeof(int [128L])));
+    requires \valid(q + (0 .. sizeof(int [0x8A])));
+    assigns \nothing;
+ */
+void f(int *n, int *p, int *q);
+
+
diff --git a/tests/spec/qarrsize.c b/tests/spec/qarrsize.c
new file mode 100644
index 0000000000000000000000000000000000000000..50c0f886d779b4e1d760cf5e65bcd90574b50f46
--- /dev/null
+++ b/tests/spec/qarrsize.c
@@ -0,0 +1,25 @@
+// Qualified Type-Array Size
+
+#define N 0xFFu
+#define P 128L
+#define Q 0x8A
+
+int a[N];
+int b[P];
+int c[Q];
+
+typedef int Ta[N];
+typedef int Tb[P];
+typedef int Tc[Q];
+
+int sa = sizeof(int[N]);
+int sb = sizeof(int[P]);
+int sc = sizeof(int[Q]);
+
+/*@
+  requires \valid(n + (0 .. sizeof(int[N])));
+  requires \valid(p + (0 .. sizeof(int[P])));
+  requires \valid(q + (0 .. sizeof(int[Q])));
+  assigns \nothing;
+ */
+void f(int *n, int *p, int *q);