Poor error message for simple syntax error

[FliegendeWurst]

Description

Try to load the file below. It contains a syntax error (== instead of = in the problem statement), but the error message produced by KeY is bad:

line 1:1 mismatched input '5' expecting {<EOF>, '\sorts', '\schemaVariables', '\programVariables', '\include', '\includeLDTs', '\classpath', '\bootclasspath', '\javaSource', '\withOptions', '\optionsDecl', '\settings', '\profile', '\heuristicsDecl', '\predicates', '\functions', '\datatypes', '\transformers', '\rules', '\axioms', '\problem', '\chooseContract', '\proofObligation', '\proof', '\contracts', '\invariants', '/*!'}

The issue occurs because the stream is not reset to the start of the file after trying the parsing process again in non-SLL mode.

testing.key:

\functions {
    int b;
}

\problem {
    (\exists int c; c == 5 && c < b)
    & (\exists int c; c = 7 && c > b)
    -> 
    b == 6
}

Reproducible

always

Steps to reproduce

1. Load testing.key
2. Observe the error message

Expected behaviour: reasonable error message
Actual behaviour: stupid error message (see above)

Additional information

• Commit: 9ad6cc8