Repeated with clauses do not parse

[bobismijnnaam]

The following input:

class C { void m() { 
    assert
        //@ with 0; 
        //@ with 0;
        //@ with 0;
        true;
} }

Yields:

[INFO] Starting verification
======================================
 At test2.java:5:11:
--------------------------------------
    3          //@ with 0;
    4          //@ with 0;
                [-
    5          //@ with 0;
                 -]
    6          true;
    7  } }
--------------------------------------
[1/4] Parsing failed: no viable alternative at input 'assert@with0;\n@with0;\n@'
--------------------------------------
 At test2.java:5:11:
--------------------------------------
    3          //@ with 0;
    4          //@ with 0;
                [-
    5          //@ with 0;
                 -]
    6          true;
    7  } }
--------------------------------------
[2/4] Parsing failed: extraneous input '@' expecting {'inline', VAL_ASSERT, 'boolean', 'byte', 'char', 'double', 'float', 'int', 'long', 'short', 'super', 'this', 'void', IntegerLiteral, FloatingPointLiteral, 'true', 'false', CharacterLiteral, StringLiteral, 'null', '(', '{', '[', '<', '*', '|', LANG_ID_ESCAPE, 'resource', 'process', 'frac', 'zfrac', 'bool', 'ref', 'rational', 'seq', 'set', 'bag', 'pointer', 'map', 'option', 'either', 'tuple', 'type', 'any', 'nothing', 'pure', 'thread_local', 'with', 'then', 'given', 'yields', 'axiom', 'model', 'adt', 'modifies', 'accessible', 'requires', 'ensures', 'context_everywhere', 'context', 'loop_invariant', 'kernel_invariant', 'lock_invariant', 'signals', 'decreases', 'apply', 'fold', 'unfold', 'open', 'close', 'assume', 'inhale', 'exhale', 'label', 'refute', 'witness', 'ghost', 'send', 'to', 'recv', 'from', 'transfer', 'csl_subject', 'spec_ignore', 'action', 'atomic', 'Reducible', 'AddsTo', 'APerm', 'ArrayPerm', 'Contribution', 'held', 'committed', 'HPerm', 'idle', 'perm', 'Perm', 'PointsTo', 'running', 'Some', 'Left', 'Right', 'Value', '\unfolding', '\Unfolding', '\current_thread', '\sum', '\old', '\typeof', '\type', '\matrix', '\array', '\pointer', '\pointer_index', '\pointer_block_length', '\pointer_block_offset', '\pointer_length', '\shared_mem_size', '\values', '\vcmp', '\vrep', '\msum', '\mcmp', '\mrep', '\result', '\ltid', '\gtid', 'none', 'None', 'write', 'read', 'empty', TRIGGER_OPEN, 'b{', '[t:', '{t:', 'b{t:', Identifier, VAL_CREATE}
--------------------------------------
 At test2.java:5:18:
--------------------------------------
    3          //@ with 0;
    4          //@ with 0;
                       [-
    5          //@ with 0;
                        -]
    6          true;
    7  } }
--------------------------------------
[3/4] Parsing failed: extraneous input '0' expecting ';'
--------------------------------------
 At test2.java:5:20:
--------------------------------------
    3          //@ with 0;
    4          //@ with 0;
                         [-
    5          //@ with 0;
                          -]
    6          true;
    7  } }
--------------------------------------
[4/4] Parsing failed: extraneous input '\n' expecting {'inline', VAL_ASSERT, 'abstract', 'assert', 'boolean', 'break', 'byte', 'char', 'class', 'continue', 'do', 'double', 'enum', 'final', 'float', 'for', 'if', 'int', 'interface', 'long', 'new', 'package', 'private', 'protected', 'public', 'return', 'short', 'static', 'strictfp', 'super', 'switch', 'synchronized', 'this', 'throw', 'try', 'void', 'while', IntegerLiteral, FloatingPointLiteral, 'true', 'false', CharacterLiteral, StringLiteral, 'null', '(', '{', '}', '[', ';', '<', '!', '~', '++', '--', '+', '-', '*', '|', '@', BlockStartSpecImmediate, LANG_ID_ESCAPE, 'resource', 'process', 'frac', 'zfrac', 'bool', 'ref', 'rational', 'seq', 'set', 'bag', 'pointer', 'map', 'option', 'either', 'tuple', 'type', 'any', 'nothing', 'pure', 'thread_local', 'with', 'then', 'given', 'yields', 'axiom', 'model', 'adt', 'modifies', 'accessible', 'requires', 'ensures', 'context_everywhere', 'context', 'loop_invariant', 'kernel_invariant', 'lock_invariant', 'signals', 'decreases', 'apply', 'fold', 'unfold', 'open', 'close', 'assume', 'inhale', 'exhale', 'label', 'refute', 'witness', 'ghost', 'send', 'to', 'recv', 'from', 'transfer', 'csl_subject', 'spec_ignore', 'action', 'atomic', 'commit', 'Reducible', 'AddsTo', 'APerm', 'ArrayPerm', 'Contribution', 'held', 'committed', 'HPerm', 'idle', 'perm', 'Perm', 'PointsTo', 'running', 'Some', 'Left', 'Right', 'Value', '\unfolding', '\Unfolding', '\current_thread', '\sum', '\old', '\typeof', '\type', '\matrix', '\array', '\pointer', '\pointer_index', '\pointer_block_length', '\pointer_block_offset', '\pointer_length', '\shared_mem_size', '\values', '\vcmp', '\vrep', '\msum', '\mcmp', '\mrep', '\result', '\ltid', '\gtid', 'none', 'None', 'write', 'read', 'empty', TRIGGER_OPEN, 'b{', '[t:', '{t:', 'b{t:', Identifier, BlockStartSpec, LineStartSpec, VAL_CREATE}
======================================

Instead, I would expect it to verify succesfully.

[bobismijnnaam]

#909