diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index a8594d8bbf4..5a3c6c7cb58 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -66,14 +66,14 @@ PUBLIC: 'public';
 PURE: 'pure';
 RETURN_BEHAVIOR: 'return_' BEHAVIOR;
 FINAL: 'final';
-MODEL: 'model'/*  -> pushMode(expr)*/;
+MODEL: 'model'/* */;
 
 fragment Pred: '_redundantly'?; //suffix
 fragment Pfree: '_free'?;       //suffix
 
-ACCESSIBLE: 'accessible' Pred -> pushMode(expr);
-ASSERT: 'assert' Pred  -> pushMode(expr);
-ASSUME: 'assume' Pred -> pushMode(expr);
+ACCESSIBLE: 'accessible' Pred;
+ASSERT: 'assert' Pred;
+ASSUME: 'assume' Pred;
 /**
  * The name 'assignable' is kept here for legacy reasons.
  * Note that KeY does only verify what can be modified (i.e., what is 'modifiable').
@@ -81,7 +81,7 @@ ASSUME: 'assume' Pred -> pushMode(expr);
 ASSIGNABLE
     : ('assignable' | 'assigns'  | 'assigning' |
        'modifiable' | 'modifies' | 'modifying' |
-       'writable'   | 'writes'   | 'writing') (Pfree|Pred) -> pushMode(expr);
+       'writable'   | 'writes'   | 'writing') (Pfree|Pred);
 /**
  * The name 'assignable' is kept here for legacy reasons.
  * Note that KeY does only verify what can be modified (i.e., what is 'modifiable').
@@ -89,82 +89,59 @@ ASSIGNABLE
 LOOP_ASSIGNABLE
     : ('loop_assignable' | 'loop_assigns' | 'loop_assigning' |
        'loop_modifiable' | 'loop_modifies' | 'loop_modifying' |
-       'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr);
-AXIOM: 'axiom' -> pushMode(expr);
-BREAKS: 'breaks' -> pushMode(expr);
-CAPTURES: 'captures' Pred -> pushMode(expr);
+       'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred);
+AXIOM: 'axiom';
+BREAKS: 'breaks';
+CAPTURES: 'captures' Pred;
 CODE: 'code'; //?
-CONSTRAINT: 'constraint' Pred -> pushMode(expr);
-CONTINUES: 'continues' -> pushMode(expr);
+CONSTRAINT: 'constraint' Pred;
+CONTINUES: 'continues';
 DEBUG: 'debug'; //?
-DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr);
-DETERMINES: 'determines' -> pushMode(expr);
-DIVERGES: 'diverges' Pred -> pushMode(expr);
-//DURATION: 'duration' Pred -> pushMode(expr);
-ENSURES: ('ensures' | 'post') (Pfree|Pred) -> pushMode(expr);
-FOR_EXAMPLE: 'for_example' -> pushMode(expr);
-//FORALL: 'forall' -> pushMode(expr); //?
+DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred;
+DETERMINES: 'determines';
+DIVERGES: 'diverges' Pred;
+DURATION: 'duration' Pred;
+ENSURES: ('ensures' | 'post') (Pfree|Pred);
+FOR_EXAMPLE: 'for_example';
+//FORALL: 'forall'; //?
 HELPER: 'helper';
-IMPLIES_THAT: 'implies_that' -> pushMode(expr);
-IN: 'in' Pred -> pushMode(expr);
-INITIALLY: 'initially' -> pushMode(expr);
+IMPLIES_THAT: 'implies_that';
+IN: 'in' Pred;
+INITIALLY: 'initially';
 INSTANCE: 'instance';
-INVARIANT: 'invariant' (Pfree|Pred) -> pushMode(expr);
+INVARIANT: 'invariant' (Pfree|Pred);
 LOOP_CONTRACT: 'loop_contract';
-LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred) -> pushMode(expr);
+LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred);
 LOOP_DETERMINES: 'loop_determines';  // internal translation for 'determines' in loop invariants
 LOOP_SEPARATES: 'loop_separates';  //KeY extension, deprecated
-MAPS: 'maps' Pred -> pushMode(expr);
-MEASURED_BY: 'measured_by' Pred -> pushMode(expr);
+MAPS: 'maps' Pred;
+MEASURED_BY: 'measured_by' Pred;
 MERGE_POINT: 'merge_point';
 MERGE_PROC: 'merge_proc';
-MERGE_PARAMS: 'merge_params' -> pushMode(expr);
-MONITORED: 'monitored' -> pushMode(expr);
-MONITORS_FOR: 'monitors_for' -> pushMode(expr);
-//OLD: 'old' -> pushMode(expr);
-//POST: 'post'Pred -> pushMode(expr);
-//PRE: 'pre' Pred -> pushMode(expr);
+MERGE_PARAMS: 'merge_params';
+MONITORED: 'monitored';
+MONITORS_FOR: 'monitors_for';
 READABLE: 'readable';
-REPRESENTS: 'represents' Pred -> pushMode(expr);
-REQUIRES: ('requires'| 'pre') (Pfree|Pred) -> pushMode(expr);
-RETURN: 'return' -> pushMode(expr);
-RETURNS: 'returns' -> pushMode(expr);
-RESPECTS: 'respects' -> pushMode(expr);
-SEPARATES: 'separates' -> pushMode(expr);
-SET: 'set' -> pushMode(expr);
-SIGNALS: ('signals' Pred | 'exsures' Pred) -> pushMode(expr);
-SIGNALS_ONLY: 'signals_only' Pred -> pushMode(expr);
-WHEN: 'when' Pred -> pushMode(expr);
-WORKING_SPACE: 'working_space' Pred -> pushMode(expr);
-WRITABLE: 'writable' -> pushMode(expr);
-
+REPRESENTS: 'represents' Pred;
+REQUIRES: ('requires'| 'pre') (Pfree|Pred);
+RETURN: 'return';
+RETURNS: 'returns';
+RESPECTS: 'respects';
+SEPARATES: 'separates';
+SET: 'set';
+SIGNALS: ('signals' Pred | 'exsures' Pred);
+SIGNALS_ONLY: 'signals_only' Pred;
+WHEN: 'when' Pred;
+WORKING_SPACE: 'working_space' Pred;
+WRITABLE: 'writable';
 JML_ML_END: '*/' -> channel(HIDDEN);
 WS: (' ' | '\t' | '\n' | '\r' | '@')+ -> channel(HIDDEN);
 NEST_START: '{|' ;
 NEST_END: '|}' ;
-C_RBRACKET: ']' -> type(RBRACKET);
-C_LBRACKET: '[' -> type(LBRACKET);
-SEMICOLON : ';' -> type(SEMI_TOPLEVEL);
-C_LBRACE: '{' -> type(LBRACE);
-C_RBRACE: '}' -> type(RBRACE);
-C_EQUAL: '=' -> type(EQUAL_SINGLE), pushMode(expr);
-C_LPAREN: '(' -> type(LPAREN);
-C_RPAREN: ')' -> type(RPAREN);
 C_STRING_LITERAL: '"' -> pushMode(string), more;
-C_IDENT: '\\'? LETTER (LETTERORDIGIT)* -> type(IDENT);
-C_COLON: ':' -> type(COLON);
-C_DOT: '.' -> type(DOT);
-C_COMMA: ',' -> type(COMMA);
-
-SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN);
-ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment);
-
-JML_SL_START: {!jmlMarkerDecision.isComment("//")}? '//' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);
-JML_ML_START: {!jmlMarkerDecision.isComment("/*")}?'/*' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);
-
-ERROR_CHAR: .;
-
-mode expr;
+COLON: ':';
+DOT: '.';
+COMMA: ',';
 
 /* Java keywords */
 BOOLEAN: 'boolean';
@@ -181,33 +158,8 @@ THIS: 'this';
 TRUE: 'true';
 VOID: 'void';
 
-E_NULLABLE: 'nullable'->type(NULLABLE);
-E_NONNULL: 'non_null' -> type(NON_NULL);
-
-
 DEPENDS: 'depends';  // internal translation for 'accessible' on model fields
 
-/* JML and JML* keywords */
-/*ACCESSIBLE: 'accessible';
-MODIFIABLE: 'modifiable';
-BREAKS: 'breaks';
-CONTINUES: 'continues';
-DECREASES: 'decreases'; // internal translation for 'measured_by'
-DETERMINES: 'determines';  //KeY extension, not official JML
-ENSURES: 'ensures';
-ENSURES_FREE: 'ensures_free';
-MODEL_METHOD_AXIOM: 'model_method_axiom';  //KeY extension, not official JML
-MERGE_PARAMS: 'merge_params';  //KeY extension, not official JML
-NON_NULL: 'non_null';
-NULLABLE: 'nullable';
-REPRESENTS: 'represents';
-REQUIRES: 'requires';
-REQUIRES_FREE: 'requires_free';
-RETURNS: 'returns';  //KeY extension, not official JML
-SEPARATES: 'separates';  //KeY extension, not official JML
-SIGNALS: 'signals';
-SIGNALS_ONLY: 'signals_only';*/
-
 /* JML keywords prefixed with a backslash */
 ALLFIELDS: '\\all_fields';  //KeY extension, not official JML
 ALLOBJECTS: '\\all_objects';  //KeY extension, not official JML
@@ -219,7 +171,7 @@ BY: '\\by';  //KeY extension, not official JML
 DECLASSIFIES: '\\declassifies';  //KeY extension, not official JML
 DISJOINT: '\\disjoint';  //KeY extension, not official JML
 DOMAIN_IMPLIES_CREATED: '\\domain_implies_created';  //KeY extension, not official JML
-DURATION: '\\duration';
+ESC_DURATION: '\\duration';
 ELEMTYPE: '\\elemtype';
 EMPTYSET: '\\empty';
 ERASES: '\\erases';  //KeY extension, not official JML
@@ -320,22 +272,19 @@ WORKINGSPACE: '\\working_space';
 // ONLY_CALLED: '\\only_called';
 // ONLY_CAPTURED: '\\only_captured';
 
-E_JML_SL_START: '//@' -> type(JML_SL_START), channel(HIDDEN);
-E_JML_ML_START: '/*@' -> type(JML_ML_START), channel(HIDDEN);
-E_JML_ML_END: '*/' -> channel(HIDDEN);
-E_SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> type(COMMENT), channel(HIDDEN);
-E_ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment);
+SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN);
+ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment);
+
+JML_SL_START: {!jmlMarkerDecision.isComment("//")}? '//' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);
+JML_ML_START: {!jmlMarkerDecision.isComment("/*")}?'/*' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);
 
 AND: '&';
 BITWISENOT: '~';
-COLON: ':';
-COMMA: ',';
 DIV: '/';
-DOT: '.';
 DOTDOT: '..';
-EQUAL_SINGLE: '=';
 EQV_ANTIV: '<==>' | '<=!=>';
 EQ_NEQ: '==' | '!=';
+EQUAL_SINGLE: '=';
 GEQ: '>=';
 IMPLIES: '==>';
 IMPLIESBACKWARD: '<==';
@@ -368,8 +317,7 @@ LBRACE:               '{' {incrBrace();};
 RBRACE:               '}' {decrBrace();};
 LBRACKET:             '[' {incrBracket();};
 RBRACKET:             ']' {decrBracket();};
-SEMI_TOPLEVEL:        {   semicolonOnToplevel()}? ';' -> popMode; //jump back to contract mode
-SEMI:                 { ! semicolonOnToplevel()}? ';';
+SEMI:                 ';';
 
 fragment LETTER: 'a'..'z' | 'A'..'Z' | '_' | '$';
 
@@ -446,10 +394,13 @@ DOUBLE_LITERAL
 fragment
 LETTERORDIGIT: LETTER | DIGIT;
 
+ESCAPED_IDENTIFIER: '`' IDENT '`' -> type(IDENT);
 IDENT: LETTER (LETTERORDIGIT)*;
-JML_IDENT: '\\' IDENT ;
+JML_IDENT: '\\' IDENT;
+JML_ESCAPED_IDENT: '`' JML_IDENT '`' -> type(JML_IDENT);
 SPECIAL_IDENT: '<'IDENT'>';
 
+
 //DL_ESCAPE: '\\dl_'  LETTER  ( LETTERORDIGIT )*  ;
 
 /*
@@ -483,10 +434,9 @@ STRING_LITERAL: '"' -> pushMode(string),more;
 E_WS: [ \t\n\r\u000c@]+ -> channel(HIDDEN), type(WS);
 INFORMAL_DESCRIPTION: '(*'  ( '*' ~')' | ~'*' )* '*)';
 
-DOC_COMMENT: '/**' -> pushMode(mlComment);
 fragment PRAGMA: '\\nowarn';
 
-E_ERROR_CHAR: . -> type(ERROR_CHAR);
+ERROR_CHAR: .;
 
 mode mlComment;
 ML_COMMENT_END: ('*/'|EOF) -> type(COMMENT), channel(HIDDEN), popMode;
diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4
index 40f27ec6acc..677eef95bdc 100644
--- a/key.core/src/main/antlr4/JmlParser.g4
+++ b/key.core/src/main/antlr4/JmlParser.g4
@@ -12,24 +12,34 @@ options { tokenVocab=JmlLexer; }
 }
 
 
-classlevel_comments: classlevel_comment* EOF;
-classlevel_comment: classlevel_element | modifiers | set_statement;
-classlevel_element0: modifiers? (classlevel_element modifiers?);
+classlevel_comments: classlevel_comment* modifiers EOF;
+
+/* weigl: Gammar not good here. High ambiguity in the parser.
+   Abstractly speaking:
+   we have:        S ->    A? B | A;
+   but:            S ->    A B? | B;
+      could be better.
+*/
+classlevel_comment: modifiers? classlevel_element;
 classlevel_element
-  : class_invariant /*| depends_clause*/     | method_specification
-  | method_declaration  | field_declaration  | represents_clause
-  | history_constraint  | initially_clause   | class_axiom
-  | monitors_for_clause | readable_if_clause | writable_if_clause
-  | datagroup_clause    | set_statement      | nowarn_pragma
-  | accessible_clause   | assert_statement   | assume_statement
+// The order matters! The rules with clear lookahead in front.
+// In the new lexer w/o contract and expr mode. The keyword "ensures"   can also be an identifier.
+// This means, that the following text could also be seen as a field declaration:
+//      //@   ensures ensures;
+  : class_invariant       | accessible_clause
+  | method_declaration    | field_declaration  | represents_clause
+  | history_constraint    | initially_clause   | class_axiom
+  | monitors_for_clause   | readable_if_clause | writable_if_clause
+  | datagroup_clause      | set_statement      | nowarn_pragma
+  | assert_statement      | assume_statement   | method_specification
   ;
 
 methodlevel_comment: (modifiers? methodlevel_element modifiers?)* EOF;
 methodlevel_element
-  : field_declaration | set_statement | merge_point_statement
-  | loop_specification | assert_statement | assume_statement | nowarn_pragma
-  | debug_statement | block_specification | block_loop_specification
-  | assert_statement | assume_statement
+  : field_declaration  | set_statement       | merge_point_statement
+  | loop_specification | assert_statement    | assume_statement
+  | debug_statement    | block_specification | block_loop_specification
+  | assert_statement   | assume_statement    | nowarn_pragma
  ;
 
 modifiers: modifier+;
@@ -43,21 +53,18 @@ modifier
 
 
 
-class_axiom: AXIOM expression SEMI_TOPLEVEL;
-initially_clause: INITIALLY expression SEMI_TOPLEVEL;
-class_invariant: INVARIANT expression SEMI_TOPLEVEL;
-//axiom_name: AXIOM_NAME_BEGIN IDENT AXIOM_NAME_END;
-method_specification: (also_keyword)* spec_case ((also_keyword)+ spec_case)*;
+class_axiom: AXIOM expression SEMI;
+initially_clause: INITIALLY expression SEMI;
+class_invariant: INVARIANT expression SEMI;
+method_specification: also_keyword* spec_case (also_keyword+ spec_case)*;
 also_keyword: (ALSO | FOR_EXAMPLE | IMPLIES_THAT);
 spec_case:
-  (modifiers)?
+  modifiers?
   behavior=(BEHAVIOR | NORMAL_BEHAVIOR | MODEL_BEHAVIOUR | EXCEPTIONAL_BEHAVIOUR
-           | BREAK_BEHAVIOR | CONTINUE_BEHAVIOR | RETURN_BEHAVIOR )?
+           | BREAK_BEHAVIOR | CONTINUE_BEHAVIOR | RETURN_BEHAVIOR)?
   spec_body
 ;
 
-/*spec_var_decls: (old_clause | FORALL expression)+;
-spec_header: requires_clause+;*/
 
 spec_body: a+=clause+ (NEST_START inner+=clause* (also_keyword+ spec_body)* NEST_END)?;
 clauseEOF: clause EOF;
@@ -73,32 +80,32 @@ clause
 
 // clauses
 targetHeap : SPECIAL_IDENT+;
-ensures_clause: ENSURES targetHeap? predornot SEMI_TOPLEVEL;
-requires_clause: REQUIRES targetHeap? predornot SEMI_TOPLEVEL;
-measured_by_clause: MEASURED_BY predornot (COMMA predornot)* SEMI_TOPLEVEL;
-captures_clause: CAPTURES predornot SEMI_TOPLEVEL;
-diverges_clause: DIVERGES predornot SEMI_TOPLEVEL;
-working_space_clause: WORKING_SPACE predornot SEMI_TOPLEVEL;
-duration_clause: DURATION predornot SEMI_TOPLEVEL;
-when_clause: WHEN predornot SEMI_TOPLEVEL;
+ensures_clause: ENSURES targetHeap? predornot SEMI;
+requires_clause: REQUIRES targetHeap? predornot SEMI;
+measured_by_clause: MEASURED_BY predornot (COMMA predornot)* SEMI;
+captures_clause: CAPTURES predornot SEMI;
+diverges_clause: DIVERGES predornot SEMI;
+working_space_clause: WORKING_SPACE predornot SEMI;
+duration_clause: DURATION predornot SEMI;
+when_clause: WHEN predornot SEMI;
 accessible_clause
 :
   ACCESSIBLE targetHeap?
                     (lhs=expression COLON)? rhs=storeRefUnion
                     (MEASURED_BY mby=expression)?
-    SEMI_TOPLEVEL;
+    SEMI;
 /**
  * The name 'assignable' is kept here for legacy reasons.
  * Note that KeY does only verify what can be modified (i.e., what is 'modifiable').
  */
-assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI;
 //depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ;
 //decreases_clause: DECREASES termexpression (COMMA termexpression)*;
 represents_clause
   : REPRESENTS lhs=expression
     (((LARROW|EQUAL_SINGLE) (rhs=expression|t=storeRefUnion))
     | (SUCH_THAT predicate))
-    SEMI_TOPLEVEL
+    SEMI
   ;
 
 separates_clause
@@ -108,14 +115,14 @@ separates_clause
     | ERASES        erase+=infflowspeclist
     | NEW_OBJECTS  newobj+=infflowspeclist
     )*
-    SEMI_TOPLEVEL
+    SEMI
   ;
 
 loop_separates_clause
   : LOOP_SEPARATES
     sep=infflowspeclist
     (NEW_OBJECTS newobj+=infflowspeclist)*
-    SEMI_TOPLEVEL
+    SEMI
   ;
 
 infflowspeclist
@@ -131,7 +138,7 @@ determines_clause
     | ERASES       erases+=infflowspeclist
     | NEW_OBJECTS newObs+=infflowspeclist
     )*
-    SEMI_TOPLEVEL
+    SEMI
   ;
 
 loop_determines_clause
@@ -139,21 +146,21 @@ loop_determines_clause
     det=infflowspeclist
     BY ITSELF
     (NEW_OBJECTS newObs+=infflowspeclist)*
-    SEMI_TOPLEVEL
+    SEMI
   ;
 
-signals_clause: SIGNALS LPAREN referencetype (IDENT)? RPAREN (predornot)? SEMI_TOPLEVEL;
-signals_only_clause: SIGNALS_ONLY (NOTHING |referencetype (COMMA referencetype)*)  SEMI_TOPLEVEL;
-breaks_clause: BREAKS LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI_TOPLEVEL;
-continues_clause: CONTINUES LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI_TOPLEVEL;
-returns_clause: RETURNS predornot? SEMI_TOPLEVEL;
+signals_clause: SIGNALS LPAREN referencetype (IDENT)? RPAREN (predornot)? SEMI;
+signals_only_clause: SIGNALS_ONLY (NOTHING |referencetype (COMMA referencetype)*)  SEMI;
+breaks_clause: BREAKS LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI;
+continues_clause: CONTINUES LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI;
+returns_clause: RETURNS predornot? SEMI;
 
-name_clause: SPEC_NAME STRING_LITERAL SEMICOLON ;
+name_clause: SPEC_NAME STRING_LITERAL SEMI ;
 //old_clause: OLD modifiers type IDENT INITIALISER ;
 
-field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI_TOPLEVEL;
-method_declaration: typespec IDENT param_list (method_body|SEMI_TOPLEVEL);
-method_body: LBRACE RETURN expression SEMI_TOPLEVEL RBRACE;
+field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI;
+method_declaration: typespec IDENT param_list (method_body|SEMI);
+method_body: LBRACE RETURN expression SEMI RBRACE;
 param_list: LPAREN (param_decl (COMMA param_decl)*)? RPAREN;
 param_decl: ((NON_NULL | NULLABLE))? typespec p=IDENT (LBRACKET RBRACKET)*;
 history_constraint: CONSTRAINT expression;
@@ -165,12 +172,12 @@ in_group_clause: IN expression;
 maps_into_clause: MAPS expression;
 nowarn_pragma: NOWARN expression;
 debug_statement: DEBUG expression;
-set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI_TOPLEVEL;
+set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI;
 merge_point_statement:
   MERGE_POINT
   (MERGE_PROC (proc=STRING_LITERAL))?
   (mergeparamsspec)?
-  SEMI_TOPLEVEL
+  SEMI
 ;
 loop_specification
   : loop_invariant
@@ -181,22 +188,22 @@ loop_specification
     | loop_assignable_clause
     | variant_function)*;
 
-loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL;
+loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI;
 /**
  * The name 'assignable' is kept here for legacy reasons.
  * Note that KeY does only verify what can be modified (i.e., what is 'modifiable').
  */
-loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
-variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL;
+loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI;
+variant_function: DECREASING expression (COMMA expression)* SEMI;
 //loop_separates_clause: SEPARATES expression;
 //loop_determines_clause: DETERMINES expression;
-assume_statement: ASSUME expression SEMI_TOPLEVEL;
+assume_statement: ASSUME expression SEMI;
 initialiser: EQUAL_SINGLE expression;
 block_specification: method_specification;
 block_loop_specification:
   loop_contract_keyword spec_case ((also_keyword)+ loop_contract_keyword spec_case)*;
 loop_contract_keyword: LOOP_CONTRACT;
-assert_statement: (ASSERT expression | UNREACHABLE) SEMI_TOPLEVEL;
+assert_statement: (ASSERT expression | UNREACHABLE) SEMI;
 //breaks_clause: BREAKS expression;
 //continues_clause: CONTINUES expression;
 //returns_clause: RETURNS expression;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
index 7200d8f1887..fefa296e6c7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
@@ -199,6 +199,13 @@ public static ImmutableSet<LabeledParserRuleContext> createNonNullPositionedStri
 
             // use special "deep" non null predicate (see bug #1392)
             // ... looks a bit like a hack with those DL escapes ...
+
+            if (!varName.startsWith("\\")) {
+                // weigl: escape all variables, except JML identifiers like \result.
+                // Otherwise their meaning change, e.g., \result is a special token.
+                varName = "`%s`".formatted(varName);
+            }
+
             final String nonNullString =
                 arrayDepth > 0 ? format("\\dl_nonNull(\\dl_heap(),%s,%d)", varName, arrayDepth)
                         : format("%s != null", varName);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java
index 80b93be0ce9..0e9923e3c55 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java
@@ -78,7 +78,6 @@ public static ParserRuleContext parseExpr(String expr) {
     }
 
     private static ParserRuleContext getExpressionContext(JmlLexer lexer) {
-        lexer._mode = JmlLexer.expr;
         JmlParser parser = createParser(lexer);
         JmlParser.ExpressionEOFContext ctx = parser.expressionEOF();
         ParserRuleContext c;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java
index 7fce7c039aa..d682ad7fc9d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java
@@ -194,6 +194,8 @@ public JTerm translateTerm(ParserRuleContext expr) {
         Object interpret = interpret(expr);
         if (interpret instanceof SLExpression) {
             return ((SLExpression) interpret).getTerm();
+        } else if (interpret instanceof TranslatedDependencyContract tdc) {
+            return tdc.rhs(); // weigl is this correct?
         } else {
             return (JTerm) interpret;
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
index 6664f1069e6..fb12eb03b6b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
@@ -231,20 +231,17 @@ public Object visitWhen_clause(JmlParser.When_clauseContext ctx) {
 
     @Override
     public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) {
-        assert methodContract != null;
-        boolean depends = ctx.MEASURED_BY() != null || ctx.COLON() != null;
         Name[] heaps = visitTargetHeap(ctx.targetHeap());
         final LabeledParserRuleContext ctx2 =
             LabeledParserRuleContext.createLabeledParserRuleContext(ctx,
                 OriginTermLabel.SpecType.ACCESSIBLE, attachOriginLabel);
         for (Name heap : heaps) {
-            if (depends) {
+            if (methodContract == null) {
+                // weigl: this accessible_clause is for the class-level not for the method.
                 TextualJMLDepends d = new TextualJMLDepends(mods, heaps, ctx2);
                 constructs = constructs.append(d);
-            } else if (methodContract != null) {
-                methodContract.addClause(ACCESSIBLE, heap, ctx2);
             } else {
-                assert false;
+                methodContract.addClause(ACCESSIBLE, heap, ctx2);
             }
         }
         return null;
@@ -453,7 +450,9 @@ public Object visitClass_axiom(JmlParser.Class_axiomContext ctx) {
 
     @Override
     public Object visitField_declaration(JmlParser.Field_declarationContext ctx) {
-        assert !mods.isEmpty();
+        if (mods.isEmpty()) {
+            raiseError(ctx, "Modifiers are empty.");
+        }
         TextualJMLFieldDecl inv = new TextualJMLFieldDecl(mods, ctx);
         constructs = constructs.append(inv);
         return null;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
index 8554b5966c2..b0717fe8e49 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
@@ -44,6 +44,7 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
+import org.key_project.util.java.StringUtil;
 
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.Token;
@@ -900,8 +901,9 @@ public Object visitIdent(JmlParser.IdentContext ctx) {
         if (ctx.SUPER() != null) {
             raiseError("\"super\" is currently not supported", ctx);
         }
-        appendToFullyQualifiedName(ctx.getText());
-        return lookupIdentifier(ctx.getText(), null, null, ctx);
+        var id = StringUtil.trim(ctx.getText(), '`'); // weigl: remove '`' from quoted identifiers
+        appendToFullyQualifiedName(id);
+        return lookupIdentifier(id, null, null, ctx);
     }
 
     @Override
@@ -985,6 +987,8 @@ public SLExpression visitPrimarySuffixAccess(JmlParser.PrimarySuffixAccessContex
 
         if (ctx.IDENT() != null) {
             String id = ctx.IDENT().getText();
+            id = StringUtil.trim(id, '`'); // weigl: remove '`' from quoted identifiers
+
             if (receiver == null) {
                 // Receiver was only a package/classname prefix
                 lookupName = fullyQualifiedName + "." + id;
@@ -1753,7 +1757,6 @@ public SLExpression visitSpecquantifiedexpression(
     public SLExpression visitOldexpression(JmlParser.OldexpressionContext ctx) {
         KeYJavaType typ;
         SLExpression result = accept(ctx.expression());
-        @Nullable
         String id = accept(ctx.IDENT());
 
         if (atPres == null || atPres.get(getBaseHeap()) == null) {
diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
index 1bb79a7f558..f9f984864ec 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
@@ -55,26 +55,26 @@ public void testLexer1() {
 
     @Test
     public void testLexer2() {
-        lex("ensures //-key@ this should be ignored\n" + "true;", ENSURES, WS, COMMENT, WS, TRUE,
-            SEMI_TOPLEVEL, EOF);
+        lex("ensures //-key@ this should be ignored\n" + "true;", ENSURES, WS, SL_COMMENT, WS, TRUE,
+            SEMI, EOF);
     }
 
     @Test
     public void testLexer3() {
         lex("ensures      /*-key@ this should be ignored */ true;", ENSURES, WS, COMMENT, WS, TRUE,
-            SEMI_TOPLEVEL, EOF);
+            SEMI, EOF);
     }
 
     @Test
     public void testLexer4() {
-        lex("/*-openjml@ ensures true; */", JML_ML_START, WS, ENSURES, WS, TRUE, SEMI_TOPLEVEL, WS,
+        lex("/*-openjml@ ensures true; */", JML_ML_START, WS, ENSURES, WS, TRUE, SEMI, WS,
             JML_ML_END, EOF);
     }
 
     @Test
     public void testLexer5() {
         lex("/*@ pure */ /*@ ensures true;", JML_ML_START, WS, PURE, WS, JML_ML_END, WS,
-            JML_ML_START, WS, ENSURES, WS, TRUE, SEMI_TOPLEVEL, EOF);
+            JML_ML_START, WS, ENSURES, WS, TRUE, SEMI, EOF);
     }
 
     @Test
@@ -142,7 +142,7 @@ public void testSimpleSpec() {
 
         assertNotNull(constructs);
         assertEquals(1, constructs.size());
-        assertTrue(constructs.head() instanceof TextualJMLSpecCase);
+        assertInstanceOf(TextualJMLSpecCase.class, constructs.head());
         TextualJMLSpecCase specCase = (TextualJMLSpecCase) constructs.head();
 
         assertSame(Behavior.NORMAL_BEHAVIOR, specCase.getBehavior());
@@ -171,7 +171,7 @@ public void testComplexSpec() {
 
         assertNotNull(constructs);
         assertEquals(1, constructs.size());
-        assertTrue(constructs.head() instanceof TextualJMLSpecCase);
+        assertInstanceOf(TextualJMLSpecCase.class, constructs.head());
         TextualJMLSpecCase specCase = (TextualJMLSpecCase) constructs.head();
 
         assertSame(Behavior.BEHAVIOR, specCase.getBehavior());
@@ -211,8 +211,8 @@ public void testMultipleSpecs() {
 
         assertNotNull(constructs);
         assertEquals(2, constructs.size());
-        assertTrue(constructs.head() instanceof TextualJMLSpecCase);
-        assertTrue(constructs.tail().head() instanceof TextualJMLSpecCase);
+        assertInstanceOf(TextualJMLSpecCase.class, constructs.head());
+        assertInstanceOf(TextualJMLSpecCase.class, constructs.tail().head());
         TextualJMLSpecCase specCase1 = (TextualJMLSpecCase) constructs.head();
         TextualJMLSpecCase specCase2 = (TextualJMLSpecCase) constructs.tail().head();
 
diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java
index 25fcc15561d..2d5c11fac08 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java
@@ -129,7 +129,7 @@ public void testSelfVar() {
     @Test
     public void testLogicalExpression() {
         LocationVariable selfVar = buildSelfVarAsProgVar();
-        JTerm result = jmlIO.parseExpression("(b <= s &&  i > 5) ==> this != instance");
+        JTerm result = jmlIO.parseExpression("(b <= s &&  i > 5) ==> this != `instance`");
         assertNotNull(result);
         assertEquals(Junctor.IMP, result.op());
         assertEquals(Junctor.AND, result.sub(0).op());
diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java
index 1b403026aeb..c9d77e30997 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java
@@ -50,7 +50,6 @@ public void parseAndInterpret(String expr) {
         LocationVariable result = new LocationVariable(new ProgramElementName("result"), kjt);
         LocationVariable exc = new LocationVariable(new ProgramElementName("exc"), kjt);
         JmlLexer lexer = JmlFacade.createLexer(expr);
-        lexer._mode = JmlLexer.expr;
         JmlParser parser = new JmlParser(new CommonTokenStream(lexer));
         JmlParser.ExpressionContext ctx = parser.expressionEOF().expression();
         Assertions.assertEquals(0, parser.getNumberOfSyntaxErrors());