diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 8826638ba57d1c5cebe29760dc3f81f4be08d39c..00cbe316e7fe89092629df8f3c9e7182d73cff98 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -350,6 +350,14 @@ let rE = ['E''e']['+''-']? rD+
 let rP = ['P''p']['+''-']? rD+
 let rFS	= ('f'|'F'|'l'|'L'|'d'|'D')
 let rIS = ('u'|'U'|'l'|'L')*
+let rOP = [
+  '=' '<' '>' '~'
+  '+' '-' '*' '/' '\\' '%'
+  '!' '$' '&' '?' '@' '^' '.' ':' '|' '#'
+  '_' '\''
+  'a'-'z' 'A'-'Z' '0'-'9'
+  '[' ']' '{' '}'
+]
 let comment_line = "//" [^'\n']*
 let rIdentifier = rL (rL | rD)*
 
@@ -381,7 +389,8 @@ rule token = parse
      check_ext_plugin (fst cabsloc) plugin tok
      }
   | '\\' rIdentifier { bs_identifier lexbuf }
-  | rIdentifier ( "::" rIdentifier )+ { lex_error lexbuf "unexpected long identifier" }
+  | rIdentifier ( "::" rIdentifier )+ { LONGIDENT (lexeme lexbuf) }
+  | rIdentifier ( "::" rIdentifier )* "::(" rOP+ ")" { LONGIDENT(lexeme lexbuf)}
   | rIdentifier       {
       let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
       let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 4e8987cc60448820622a9b4d855f9b9e4d432edf..45af8f8aa29d5ca4729f35170d5826fc0c62a70b 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -2,7 +2,7 @@
 /*                                                                        */
 /*  This file is part of Frama-C.                                         */
 /*                                                                        */
-/*  Copyright (C) 2007-2024                                               */
+/*  Copyright (C) 2007-2023                                               */
 /*    CEA   (Commissariat à l'énergie atomique et aux énergies            */
 /*           alternatives)                                                */
 /*    INRIA (Institut National de Recherche en Informatique et en         */
@@ -254,7 +254,7 @@
 
 %token MODULE FUNCTION CONTRACT INCLUDE EXT_AT EXT_LET
 /* ACSL extension for external spec  file */
-%token <string> IDENTIFIER TYPENAME IDENTIFIER_EXT
+%token <string> LONGIDENT IDENTIFIER TYPENAME IDENTIFIER_EXT
 %token <bool*string> STRING_LITERAL
 %token <string> INT_CONSTANT
 %token <string> FLOAT_CONSTANT
@@ -874,6 +874,7 @@ ne_logic_type_list(tname):
 
 full_identifier:
 | id = identifier { id }
+| id = LONGIDENT { id }
 | ADMIT { "admit" }
 | ALLOCATES { "allocates" }
 | ASSERT { "assert" }
@@ -1182,7 +1183,7 @@ ne_decreases:
 ;
 
 variant:
-| lexpr FOR any_identifier { ($1, Some $3) }
+| lexpr FOR full_identifier { ($1, Some $3) }
 | lexpr                    { ($1, None) }
 ;
 
@@ -1453,8 +1454,8 @@ loop_grammar_extension:
 }
 ;
 
-/*** code annotations ***/
 
+/*** code annotations ***/
 beg_code_annotation:
 | FOR {}
 | ASSERT {}
@@ -1901,7 +1902,7 @@ post_cond:
 
 is_acsl_spec:
 | post_cond  { snd $1 }
-| EXT_CONTRACT { $1 }
+| EXT_CONTRACT   { $1 }
 | ASSIGNS    { "assigns" }
 | ALLOCATES  { "allocates" }
 | FREES      { "frees" }
@@ -1917,8 +1918,8 @@ is_acsl_spec:
 
 is_acsl_decl_or_code_annot:
 | EXT_CODE_ANNOT { $1 }
-| EXT_GLOBAL { $1 }
-| EXT_GLOBAL_BLOCK { $1 }
+| EXT_GLOBAL     { $1 }
+| EXT_GLOBAL_BLOCK     { $1 }
 | IDENTIFIER_EXT { $1 }
 | ASSUMES   { "assumes" }
 | ASSERT    { "assert" }
@@ -2013,6 +2014,7 @@ bs_keyword:
 
 wildcard:
 | any_identifier { () }
+| LONGIDENT { () }
 | bs_keyword { () }
 | AMP { () }
 | AND { () }
diff --git a/tests/spec/oracle/module.res.oracle b/tests/spec/oracle/module.res.oracle
index 809701e2a74442563ec63fdaceee2e2364d53805..8f264b51c5568ddd50b291770cdf9cab00eafbf4 100644
--- a/tests/spec/oracle/module.res.oracle
+++ b/tests/spec/oracle/module.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing module.i (no preprocessing)
 [kernel:annot-error] module.i:7: Warning: 
-  lexical error, unexpected long identifier
+  unbound logic function int::Int::add. Ignoring global annotation
 [kernel] User Error: warning annot-error treated as fatal error.
 [kernel] Frama-C aborted: invalid user input.