TestCE

all > de.uka.ilkd.key.testcase.smt.ce > TestCE
12

tests
1

failures
0

ignored
1.323s

duration
91%

successful

Failed tests

testMiddle()

line 135:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 135:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 135:44 mismatched input ')' expecting {'(', '{'}
line 141:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 141:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 141:41 mismatched input ')' expecting {'(', '{'}
line 148:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 148:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 148:35 mismatched input '=' expecting {'(', '{'}
line 150:38 mismatched input '}' expecting {'(', '{'}
line 155:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 155:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 155:35 mismatched input '=' expecting {'(', '{'}
line 157:38 mismatched input '}' expecting {'(', '{'}
line 163:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 163:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 163:30 mismatched input '=' expecting {'(', '{'}
line 165:38 mismatched input '}' expecting {'(', '{'}
line 171:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 171:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 171:30 mismatched input '=' expecting {'(', '{'}
line 173:38 mismatched input '}' expecting {'(', '{'}
line 179:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 179:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 179:32 mismatched input '&' expecting {'(', '{'}
line 181:42 mismatched input '}' expecting {'(', '{'}
line 182:39 mismatched input '}' expecting {'(', '{'}
line 188:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 188:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 188:32 mismatched input '&' expecting {'(', '{'}
line 190:42 mismatched input '}' expecting {'(', '{'}
line 191:39 mismatched input '}' expecting {'(', '{'}
line 198:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 198:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 198:32 mismatched input '&' expecting {'(', '{'}
line 200:42 mismatched input '}' expecting {'(', '{'}
line 201:39 mismatched input '}' expecting {'(', '{'}
line 208:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 208:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 208:32 mismatched input '&' expecting {'(', '{'}
line 210:42 mismatched input '}' expecting {'(', '{'}
line 211:39 mismatched input '}' expecting {'(', '{'}
line 218:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 218:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 218:31 mismatched input ')' expecting {'(', '{'}
line 220:44 mismatched input ')' expecting {'(', '{'}
line 225:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 225:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 225:31 mismatched input ')' expecting {'(', '{'}
line 227:44 mismatched input ')' expecting {'(', '{'}
line 233:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 233:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 233:31 mismatched input ')' expecting {'(', '{'}
line 237:42 mismatched input '}' expecting {'(', '{'}
line 238:34 mismatched input '}' expecting {'(', '{'}
line 239:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 239:33 mismatched input '->' expecting {'(', '{'}
line 240:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 240:25 mismatched input ')' expecting {'(', '{'}
line 240:56 mismatched input ')' expecting {'(', '{'}
line 245:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 245:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 245:31 mismatched input ')' expecting {'(', '{'}
line 248:45 mismatched input '}' expecting {'(', '{'}
line 249:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 249:38 mismatched input ')' expecting {'(', '{'}
line 250:42 mismatched input '}' expecting {'(', '{'}
line 251:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 251:33 mismatched input '->' expecting {'(', '{'}
line 255:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 255:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 255:31 mismatched input ')' expecting {'(', '{'}
line 258:52 extraneous input '0' expecting {'\lemma', '}', IDENT, '/*!'}
line 258:54 mismatched input 'then' expecting {<EOF>, '\problem', '\chooseContract', '\proofObligation', '\proof'}
 (file: src/test/resources/testcase/smt/ce/middle.key; caused by: de.uka.ilkd.key.proof.init.ProofInputException: line 135:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 135:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 135:44 mismatched input ')' expecting {'(', '{'}
line 141:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 141:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 141:41 mismatched input ')' expecting {'(', '{'}
line 148:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 148:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 148:35 mismatched input '=' expecting {'(', '{'}
line 150:38 mismatched input '}' expecting {'(', '{'}
line 155:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 155:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 155:35 mismatched input '=' expecting {'(', '{'}
line 157:38 mismatched input '}' expecting {'(', '{'}
line 163:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 163:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 163:30 mismatched input '=' expecting {'(', '{'}
line 165:38 mismatched input '}' expecting {'(', '{'}
line 171:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 171:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 171:30 mismatched input '=' expecting {'(', '{'}
line 173:38 mismatched input '}' expecting {'(', '{'}
line 179:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 179:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 179:32 mismatched input '&' expecting {'(', '{'}
line 181:42 mismatched input '}' expecting {'(', '{'}
line 182:39 mismatched input '}' expecting {'(', '{'}
line 188:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 188:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 188:32 mismatched input '&' expecting {'(', '{'}
line 190:42 mismatched input '}' expecting {'(', '{'}
line 191:39 mismatched input '}' expecting {'(', '{'}
line 198:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 198:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 198:32 mismatched input '&' expecting {'(', '{'}
line 200:42 mismatched input '}' expecting {'(', '{'}
line 201:39 mismatched input '}' expecting {'(', '{'}
line 208:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 208:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 208:32 mismatched input '&' expecting {'(', '{'}
line 210:42 mismatched input '}' expecting {'(', '{'}
line 211:39 mismatched input '}' expecting {'(', '{'}
line 218:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 218:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 218:31 mismatched input ')' expecting {'(', '{'}
line 220:44 mismatched input ')' expecting {'(', '{'}
line 225:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 225:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 225:31 mismatched input ')' expecting {'(', '{'}
line 227:44 mismatched input ')' expecting {'(', '{'}
line 233:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 233:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 233:31 mismatched input ')' expecting {'(', '{'}
line 237:42 mismatched input '}' expecting {'(', '{'}
line 238:34 mismatched input '}' expecting {'(', '{'}
line 239:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 239:33 mismatched input '->' expecting {'(', '{'}
line 240:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 240:25 mismatched input ')' expecting {'(', '{'}
line 240:56 mismatched input ')' expecting {'(', '{'}
line 245:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 245:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 245:31 mismatched input ')' expecting {'(', '{'}
line 248:45 mismatched input '}' expecting {'(', '{'}
line 249:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 249:38 mismatched input ')' expecting {'(', '{'}
line 250:42 mismatched input '}' expecting {'(', '{'}
line 251:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 251:33 mismatched input '->' expecting {'(', '{'}
line 255:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 255:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 255:31 mismatched input ')' expecting {'(', '{'}
line 258:52 extraneous input '0' expecting {'\lemma', '}', IDENT, '/*!'}
line 258:54 mismatched input 'then' expecting {<EOF>, '\problem', '\chooseContract', '\proofObligation', '\proof'}
)
	at app//de.uka.ilkd.key.control.AbstractUserInterfaceControl.load(AbstractUserInterfaceControl.java:221)
	at app//de.uka.ilkd.key.control.KeYEnvironment.load(KeYEnvironment.java:251)
	at app//de.uka.ilkd.key.control.KeYEnvironment.load(KeYEnvironment.java:224)
	at app//de.uka.ilkd.key.control.KeYEnvironment.load(KeYEnvironment.java:184)
	at app//de.uka.ilkd.key.testcase.smt.ce.TestCE.testMiddle(TestCE.java:128)
	at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
	at app//org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:725)
	at app//org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:149)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:140)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:84)
	at app//org.junit.jupiter.engine.execution.ExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(ExecutableInvoker.java:115)
	at app//org.junit.jupiter.engine.execution.ExecutableInvoker.lambda$invoke$0(ExecutableInvoker.java:105)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
	at app//org.junit.jupiter.engine.execution.ExecutableInvoker.invoke(ExecutableInvoker.java:104)
	at app//org.junit.jupiter.engine.execution.ExecutableInvoker.invoke(ExecutableInvoker.java:98)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$7(TestMethodTestDescriptor.java:214)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:210)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:135)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:66)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:151)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at java.base@11.0.18/java.util.ArrayList.forEach(ArrayList.java:1541)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at java.base@11.0.18/java.util.ArrayList.forEach(ArrayList.java:1541)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
	at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
	at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
	at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
	at org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
	at org.junit.platform.launcher.core.SessionPerRequestLauncher.execute(SessionPerRequestLauncher.java:53)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:99)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:79)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:75)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:62)
	at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
	at com.sun.proxy.$Proxy2.stop(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:193)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Caused by: de.uka.ilkd.key.proof.init.ProofInputException: line 135:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 135:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 135:44 mismatched input ')' expecting {'(', '{'}
line 141:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 141:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 141:41 mismatched input ')' expecting {'(', '{'}
line 148:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 148:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 148:35 mismatched input '=' expecting {'(', '{'}
line 150:38 mismatched input '}' expecting {'(', '{'}
line 155:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 155:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 155:35 mismatched input '=' expecting {'(', '{'}
line 157:38 mismatched input '}' expecting {'(', '{'}
line 163:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 163:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 163:30 mismatched input '=' expecting {'(', '{'}
line 165:38 mismatched input '}' expecting {'(', '{'}
line 171:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 171:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 171:30 mismatched input '=' expecting {'(', '{'}
line 173:38 mismatched input '}' expecting {'(', '{'}
line 179:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 179:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 179:32 mismatched input '&' expecting {'(', '{'}
line 181:42 mismatched input '}' expecting {'(', '{'}
line 182:39 mismatched input '}' expecting {'(', '{'}
line 188:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 188:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 188:32 mismatched input '&' expecting {'(', '{'}
line 190:42 mismatched input '}' expecting {'(', '{'}
line 191:39 mismatched input '}' expecting {'(', '{'}
line 198:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 198:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 198:32 mismatched input '&' expecting {'(', '{'}
line 200:42 mismatched input '}' expecting {'(', '{'}
line 201:39 mismatched input '}' expecting {'(', '{'}
line 208:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 208:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 208:32 mismatched input '&' expecting {'(', '{'}
line 210:42 mismatched input '}' expecting {'(', '{'}
line 211:39 mismatched input '}' expecting {'(', '{'}
line 218:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 218:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 218:31 mismatched input ')' expecting {'(', '{'}
line 220:44 mismatched input ')' expecting {'(', '{'}
line 225:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 225:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 225:31 mismatched input ')' expecting {'(', '{'}
line 227:44 mismatched input ')' expecting {'(', '{'}
line 233:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 233:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 233:31 mismatched input ')' expecting {'(', '{'}
line 237:42 mismatched input '}' expecting {'(', '{'}
line 238:34 mismatched input '}' expecting {'(', '{'}
line 239:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 239:33 mismatched input '->' expecting {'(', '{'}
line 240:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 240:25 mismatched input ')' expecting {'(', '{'}
line 240:56 mismatched input ')' expecting {'(', '{'}
line 245:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 245:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 245:31 mismatched input ')' expecting {'(', '{'}
line 248:45 mismatched input '}' expecting {'(', '{'}
line 249:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 249:38 mismatched input ')' expecting {'(', '{'}
line 250:42 mismatched input '}' expecting {'(', '{'}
line 251:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 251:33 mismatched input '->' expecting {'(', '{'}
line 255:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 255:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 255:31 mismatched input ')' expecting {'(', '{'}
line 258:52 extraneous input '0' expecting {'\lemma', '}', IDENT, '/*!'}
line 258:54 mismatched input 'then' expecting {<EOF>, '\problem', '\chooseContract', '\proofObligation', '\proof'}

	at app//de.uka.ilkd.key.proof.io.KeYFile.readIncludes(KeYFile.java:210)
	at app//de.uka.ilkd.key.proof.init.ProblemInitializer.readIncludes(ProblemInitializer.java:177)
	at app//de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:325)
	at app//de.uka.ilkd.key.proof.init.ProblemInitializer.readIncludes(ProblemInitializer.java:188)
	at app//de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:325)
	at app//de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:449)
	at app//de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:518)
	at app//de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:288)
	at app//de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:252)
	at app//de.uka.ilkd.key.control.AbstractUserInterfaceControl.load(AbstractUserInterfaceControl.java:209)
	... 89 more
Caused by: de.uka.ilkd.key.util.parsing.SyntaxErrorReporter$ParserException: line 135:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 135:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 135:44 mismatched input ')' expecting {'(', '{'}
line 141:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 141:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 141:41 mismatched input ')' expecting {'(', '{'}
line 148:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 148:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 148:35 mismatched input '=' expecting {'(', '{'}
line 150:38 mismatched input '}' expecting {'(', '{'}
line 155:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 155:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 155:35 mismatched input '=' expecting {'(', '{'}
line 157:38 mismatched input '}' expecting {'(', '{'}
line 163:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 163:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 163:30 mismatched input '=' expecting {'(', '{'}
line 165:38 mismatched input '}' expecting {'(', '{'}
line 171:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 171:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 171:30 mismatched input '=' expecting {'(', '{'}
line 173:38 mismatched input '}' expecting {'(', '{'}
line 179:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 179:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 179:32 mismatched input '&' expecting {'(', '{'}
line 181:42 mismatched input '}' expecting {'(', '{'}
line 182:39 mismatched input '}' expecting {'(', '{'}
line 188:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 188:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 188:32 mismatched input '&' expecting {'(', '{'}
line 190:42 mismatched input '}' expecting {'(', '{'}
line 191:39 mismatched input '}' expecting {'(', '{'}
line 198:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 198:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 198:32 mismatched input '&' expecting {'(', '{'}
line 200:42 mismatched input '}' expecting {'(', '{'}
line 201:39 mismatched input '}' expecting {'(', '{'}
line 208:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 208:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 208:32 mismatched input '&' expecting {'(', '{'}
line 210:42 mismatched input '}' expecting {'(', '{'}
line 211:39 mismatched input '}' expecting {'(', '{'}
line 218:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 218:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 218:31 mismatched input ')' expecting {'(', '{'}
line 220:44 mismatched input ')' expecting {'(', '{'}
line 225:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 225:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 225:31 mismatched input ')' expecting {'(', '{'}
line 227:44 mismatched input ')' expecting {'(', '{'}
line 233:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 233:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 233:31 mismatched input ')' expecting {'(', '{'}
line 237:42 mismatched input '}' expecting {'(', '{'}
line 238:34 mismatched input '}' expecting {'(', '{'}
line 239:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 239:33 mismatched input '->' expecting {'(', '{'}
line 240:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 240:25 mismatched input ')' expecting {'(', '{'}
line 240:56 mismatched input ')' expecting {'(', '{'}
line 245:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 245:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 245:31 mismatched input ')' expecting {'(', '{'}
line 248:45 mismatched input '}' expecting {'(', '{'}
line 249:8 extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'}
line 249:38 mismatched input ')' expecting {'(', '{'}
line 250:42 mismatched input '}' expecting {'(', '{'}
line 251:28 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 251:33 mismatched input '->' expecting {'(', '{'}
line 255:14 mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL}
line 255:27 extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'}
line 255:31 mismatched input ')' expecting {'(', '{'}
line 258:52 extraneous input '0' expecting {'\lemma', '}', IDENT, '/*!'}
line 258:54 mismatched input 'then' expecting {<EOF>, '\problem', '\chooseContract', '\proofObligation', '\proof'}

	at app//de.uka.ilkd.key.util.parsing.SyntaxErrorReporter.throwException(SyntaxErrorReporter.java:89)
	at app//de.uka.ilkd.key.nparser.ParsingFacade.parseFile(ParsingFacade.java:125)
	at app//de.uka.ilkd.key.proof.io.KeYFile.getParseContext(KeYFile.java:160)
	at app//de.uka.ilkd.key.proof.io.KeYFile.readIncludes(KeYFile.java:206)
	... 98 more

Tests

Test Duration Result
testMiddle() 1.165s failed
testOverFlow1() 0.126s passed
testOverFlow2() 0.004s passed
testTypes1() 0.003s passed
testTypes2() 0.002s passed
testTypes3() 0.001s passed
testTypes4() 0.009s passed
testTypes5() 0.001s passed
testTypes6() 0.009s passed
testTypes7() 0.001s passed
testTypes8() 0.001s passed
testTypes9() 0.001s passed

Standard output

14:49:37,104 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:49:37,105 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core.testgen/build/resources/test/logback.xml]
14:49:37,186 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
14:49:37,187 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:49:37,192 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
14:49:37,197 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
14:49:37,197 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
14:49:37,198 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:49:37,216 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
14:49:37,216 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
14:49:37,216 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
14:49:37,217 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@388ba540 - Registering current configuration as safe fallback point

326        WARN  Test worker     d.u.i.k.t.s.c.TestCE      Warning: Z3_CE is not installed, tests skipped. 
328        WARN  Test worker     d.u.i.k.t.s.c.TestCE      Maybe use JVM system property "z3SolverPath" to define the path to the Z3 command. 
408        WARN  Test worker     d.u.i.k.s.ProofIndependentSettings The settings in /home/runner/.key/proofIndependentSettings.props are *not* read due to flag 'key.disregardSettings' 
728        WARN  Test worker     d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
1396       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:135:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@745,3563:3573='\ifExintVar',<188>,135:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1401       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:135:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@748,3576:3576='(',<146>,135:27] (rulesOrAxioms, decls, file) 
1401       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:135:44: mismatched input ')' expecting {'(', '{'} [@754,3593:3593=')',<147>,135:44] (taclet, rulesOrAxioms, decls, file) 
1402       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:141:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@780,3716:3726='\ifExintVar',<188>,141:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1403       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:141:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@783,3729:3729='(',<146>,141:27] (rulesOrAxioms, decls, file) 
1418       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:141:41: mismatched input ')' expecting {'(', '{'} [@789,3743:3743=')',<147>,141:41] (taclet, rulesOrAxioms, decls, file) 
1418       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:148:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@819,3896:3906='\ifExintVar',<188>,148:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1419       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:148:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@822,3909:3909='(',<146>,148:27] (rulesOrAxioms, decls, file) 
1421       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:148:35: mismatched input '=' expecting {'(', '{'} [@825,3917:3917='=',<159>,148:35] (taclet, rulesOrAxioms, decls, file) 
1422       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:150:38: mismatched input '}' expecting {'(', '{'} [@859,4023:4023='}',<149>,150:38] (taclet, rulesOrAxioms, decls, file) 
1423       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:155:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@877,4109:4119='\ifExintVar',<188>,155:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1424       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:155:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@880,4122:4122='(',<146>,155:27] (rulesOrAxioms, decls, file) 
1424       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:155:35: mismatched input '=' expecting {'(', '{'} [@883,4130:4130='=',<159>,155:35] (taclet, rulesOrAxioms, decls, file) 
1425       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:157:38: mismatched input '}' expecting {'(', '{'} [@917,4230:4230='}',<149>,157:38] (taclet, rulesOrAxioms, decls, file) 
1425       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:163:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@939,4350:4360='\ifExintVar',<188>,163:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1426       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:163:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@942,4363:4363='(',<146>,163:27] (rulesOrAxioms, decls, file) 
1426       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:163:30: mismatched input '=' expecting {'(', '{'} [@945,4366:4366='=',<159>,163:30] (taclet, rulesOrAxioms, decls, file) 
1427       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:165:38: mismatched input '}' expecting {'(', '{'} [@979,4477:4477='}',<149>,165:38] (taclet, rulesOrAxioms, decls, file) 
1428       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:171:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1001,4604:4614='\ifExintVar',<188>,171:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1430       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:171:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1004,4617:4617='(',<146>,171:27] (rulesOrAxioms, decls, file) 
1431       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:171:30: mismatched input '=' expecting {'(', '{'} [@1007,4620:4620='=',<159>,171:30] (taclet, rulesOrAxioms, decls, file) 
1431       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:173:38: mismatched input '}' expecting {'(', '{'} [@1041,4725:4725='}',<149>,173:38] (taclet, rulesOrAxioms, decls, file) 
1432       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:179:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1063,4848:4858='\ifExintVar',<188>,179:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1432       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:179:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1066,4861:4861='(',<146>,179:27] (rulesOrAxioms, decls, file) 
1440       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:179:32: mismatched input '&' expecting {'(', '{'} [@1069,4866:4866='&',<156>,179:32] (taclet, rulesOrAxioms, decls, file) 
1440       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:181:42: mismatched input '}' expecting {'(', '{'} [@1109,4985:4985='}',<149>,181:42] (taclet, rulesOrAxioms, decls, file) 
1441       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:182:39: mismatched input '}' expecting {'(', '{'} [@1122,5030:5030='}',<149>,182:39] (taclet, rulesOrAxioms, decls, file) 
1441       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:188:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1146,5149:5159='\ifExintVar',<188>,188:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1442       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:188:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1149,5162:5162='(',<146>,188:27] (rulesOrAxioms, decls, file) 
1442       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:188:32: mismatched input '&' expecting {'(', '{'} [@1152,5167:5167='&',<156>,188:32] (taclet, rulesOrAxioms, decls, file) 
1443       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:190:42: mismatched input '}' expecting {'(', '{'} [@1192,5280:5280='}',<149>,190:42] (taclet, rulesOrAxioms, decls, file) 
1445       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:191:39: mismatched input '}' expecting {'(', '{'} [@1205,5325:5325='}',<149>,191:39] (taclet, rulesOrAxioms, decls, file) 
1447       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:198:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1233,5475:5485='\ifExintVar',<188>,198:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1449       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:198:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1236,5488:5488='(',<146>,198:27] (rulesOrAxioms, decls, file) 
1450       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:198:32: mismatched input '&' expecting {'(', '{'} [@1239,5493:5493='&',<156>,198:32] (taclet, rulesOrAxioms, decls, file) 
1450       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:200:42: mismatched input '}' expecting {'(', '{'} [@1279,5612:5612='}',<149>,200:42] (taclet, rulesOrAxioms, decls, file) 
1458       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:201:39: mismatched input '}' expecting {'(', '{'} [@1292,5657:5657='}',<149>,201:39] (taclet, rulesOrAxioms, decls, file) 
1458       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:208:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1320,5817:5827='\ifExintVar',<188>,208:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1459       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:208:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1323,5830:5830='(',<146>,208:27] (rulesOrAxioms, decls, file) 
1460       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:208:32: mismatched input '&' expecting {'(', '{'} [@1326,5835:5835='&',<156>,208:32] (taclet, rulesOrAxioms, decls, file) 
1460       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:210:42: mismatched input '}' expecting {'(', '{'} [@1366,5948:5948='}',<149>,210:42] (taclet, rulesOrAxioms, decls, file) 
1461       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:211:39: mismatched input '}' expecting {'(', '{'} [@1379,5993:5993='}',<149>,211:39] (taclet, rulesOrAxioms, decls, file) 
1462       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:218:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1407,6146:6156='\ifExintVar',<188>,218:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1463       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:218:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1410,6159:6159='(',<146>,218:27] (rulesOrAxioms, decls, file) 
1463       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:218:31: mismatched input ')' expecting {'(', '{'} [@1412,6163:6163=')',<147>,218:31] (taclet, rulesOrAxioms, decls, file) 
1464       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:220:44: mismatched input ')' expecting {'(', '{'} [@1444,6275:6275=')',<147>,220:44] (taclet, rulesOrAxioms, decls, file) 
1464       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:225:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1471,6389:6399='\ifExintVar',<188>,225:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1465       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:225:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1474,6402:6402='(',<146>,225:27] (rulesOrAxioms, decls, file) 
1465       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:225:31: mismatched input ')' expecting {'(', '{'} [@1476,6406:6406=')',<147>,225:31] (taclet, rulesOrAxioms, decls, file) 
1466       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:227:44: mismatched input ')' expecting {'(', '{'} [@1508,6509:6509=')',<147>,227:44] (taclet, rulesOrAxioms, decls, file) 
1467       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:233:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1539,6656:6666='\ifExintVar',<188>,233:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1467       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:233:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1542,6669:6669='(',<146>,233:27] (rulesOrAxioms, decls, file) 
1468       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:233:31: mismatched input ')' expecting {'(', '{'} [@1544,6673:6673=')',<147>,233:31] (taclet, rulesOrAxioms, decls, file) 
1468       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:237:42: mismatched input '}' expecting {'(', '{'} [@1586,6850:6850='}',<149>,237:42] (taclet, rulesOrAxioms, decls, file) 
1469       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:238:34: mismatched input '}' expecting {'(', '{'} [@1599,6891:6891='}',<149>,238:34] (taclet, rulesOrAxioms, decls, file) 
1470       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:239:28: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1608,6925:6925='(',<146>,239:28] (rulesOrAxioms, decls, file) 
1470       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:239:33: mismatched input '->' expecting {'(', '{'} [@1611,6930:6931='->',<158>,239:33] (taclet, rulesOrAxioms, decls, file) 
1471       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:240:8: extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'} [@1626,6979:6990='\replacewith',<105>,240:8] (rulesOrAxioms, decls, file) 
1472       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:240:25: mismatched input ')' expecting {'(', '{'} [@1629,6996:6996=')',<147>,240:25] (taclet, rulesOrAxioms, decls, file) 
1472       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:240:56: mismatched input ')' expecting {'(', '{'} [@1642,7027:7027=')',<147>,240:56] (taclet, rulesOrAxioms, decls, file) 
1473       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:245:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1658,7109:7119='\ifExintVar',<188>,245:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1473       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:245:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1661,7122:7122='(',<146>,245:27] (rulesOrAxioms, decls, file) 
1479       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:245:31: mismatched input ')' expecting {'(', '{'} [@1663,7126:7126=')',<147>,245:31] (taclet, rulesOrAxioms, decls, file) 
1481       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:248:45: mismatched input '}' expecting {'(', '{'} [@1696,7268:7268='}',<149>,248:45] (taclet, rulesOrAxioms, decls, file) 
1483       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:249:8: extraneous input '\replacewith' expecting {'\lemma', '}', IDENT, '/*!'} [@1701,7284:7295='\replacewith',<105>,249:8] (rulesOrAxioms, decls, file) 
1483       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:249:38: mismatched input ')' expecting {'(', '{'} [@1708,7314:7314=')',<147>,249:38] (taclet, rulesOrAxioms, decls, file) 
1484       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:250:42: mismatched input '}' expecting {'(', '{'} [@1731,7381:7381='}',<149>,250:42] (taclet, rulesOrAxioms, decls, file) 
1484       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:251:28: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1741,7416:7416='(',<146>,251:28] (rulesOrAxioms, decls, file) 
1485       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:251:33: mismatched input '->' expecting {'(', '{'} [@1744,7421:7422='->',<158>,251:33] (taclet, rulesOrAxioms, decls, file) 
1487       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:255:14: mismatched input '\ifExintVar' expecting {MODALITY, FORALL, EXISTS, '\if', '\ifEx', 'true', 'false', '(', '{', '@', NOT, SEQARROW, '-', STRING_LITERAL, CHAR_LITERAL, BIN_LITERAL, HEX_LITERAL, IDENT, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL} [@1765,7506:7516='\ifExintVar',<188>,255:14] (termorseq, taclet, rulesOrAxioms, decls, file) 
1488       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:255:27: extraneous input '(' expecting {'\lemma', '}', IDENT, '/*!'} [@1768,7519:7519='(',<146>,255:27] (rulesOrAxioms, decls, file) 
1488       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:255:31: mismatched input ')' expecting {'(', '{'} [@1770,7523:7523=')',<147>,255:31] (taclet, rulesOrAxioms, decls, file) 
1489       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:258:52: extraneous input '0' expecting {'\lemma', '}', IDENT, '/*!'} [@1809,7667:7667='0',<184>,258:52] (rulesOrAxioms, decls, file) 
1490       WARN  Test worker     d.u.i.k.n.KeYParser       [syntax-error] jar:file:/home/runner/work/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key:258:54: mismatched input 'then' expecting {<EOF>, '\problem', '\chooseContract', '\proofObligation', '\proof'} [@1811,7669:7672='then',<183>,258:54] (file)