RunAllProofsFunctional

all > de.uka.ilkd.key.proof.runallproofs > RunAllProofsFunctional
47

tests
1

failures
0

ignored
1h30m50.04s

duration
97%

successful

Failed tests

redux

org.opentest4j.AssertionFailedError: Executed process terminated with non-zero exit value. ==> expected: <0> but was: <1>
	at app//org.junit.jupiter.api.AssertionUtils.fail(AssertionUtils.java:55)
	at app//org.junit.jupiter.api.AssertionUtils.failNotEqual(AssertionUtils.java:62)
	at app//org.junit.jupiter.api.AssertEquals.assertEquals(AssertEquals.java:150)
	at app//org.junit.jupiter.api.Assertions.assertEquals(Assertions.java:559)
	at app//de.uka.ilkd.key.proof.runallproofs.proofcollection.ForkedTestFileRunner.processTestFiles(ForkedTestFileRunner.java:129)
	at app//de.uka.ilkd.key.proof.runallproofs.RunAllProofsTestUnit.runTest(RunAllProofsTestUnit.java:85)
	at app//de.uka.ilkd.key.proof.runallproofs.RunAllProofsTest.lambda$data$0(RunAllProofsTest.java:83)
	at app//org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.lambda$execute$0(DynamicTestTestDescriptor.java:53)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
	at app//org.junit.jupiter.api.extension.InvocationInterceptor.interceptDynamicTest(InvocationInterceptor.java:167)
	at app//org.junit.jupiter.api.extension.InvocationInterceptor.interceptDynamicTest(InvocationInterceptor.java:184)
	at app//org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.lambda$execute$1(DynamicTestTestDescriptor.java:61)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptorCall.lambda$ofVoid$0(InvocationInterceptorChain.java:78)
	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.descriptor.DynamicTestTestDescriptor.execute(DynamicTestTestDescriptor.java:60)
	at app//org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.execute(DynamicTestTestDescriptor.java:32)
	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 app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:226)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:204)
	at java.base@11.0.18/java.util.Optional.ifPresent(Optional.java:183)
	at app//org.junit.jupiter.engine.descriptor.TestFactoryTestDescriptor.lambda$invokeTestMethod$1(TestFactoryTestDescriptor.java:108)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.jupiter.engine.descriptor.TestFactoryTestDescriptor.invokeTestMethod(TestFactoryTestDescriptor.java:95)
	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)

Tests

Test Method name Duration Result
project.key data()[10] 34.804s passed
project.key#1 data()[11] 14.470s passed
lcp.key data()[12] 15.637s passed
project.key#2 data()[13] 18.786s passed
ArrayList_contains.key data()[14] 13.756s passed
ArrayList_get.key data()[15] 14.270s passed
ArrayList_size.key data()[16] 12.924s passed
UpdateAbstraction_ex7_3_secure.key data()[17] 13.115s passed
UpdateAbstraction_ex7_4_secure.key data()[18] 13.612s passed
UpdateAbstraction_ex7_5_secure.key data()[19] 12.961s passed
newBook data()[1] 58.885s passed
UpdateAbstraction_ex7_6_secure.key data()[20] 13.398s passed
UpdateAbstraction_ex9_secure.key data()[21] 14.830s passed
list data()[22] 4m35.31s passed
list_ghost data()[23] 1m8.25s passed
list_recursive data()[24] 22.205s passed
list_seq data()[25] 2m27.07s passed
observer data()[26] 1m39.07s passed
removeDups data()[27] 39.811s passed
Saddleback_search.key data()[28] 1m35.60s passed
quicksort data()[29] 1m43.02s passed
oldBook data()[2] 17.504s passed
simpleTests data()[30] 2m43.00s passed
SmansEtAl data()[31] 3m17.97s passed
VACID0 data()[32] 1m18.63s passed
VSTTE10 data()[33] 2m57.54s passed
WeideEtAl data()[34] 30.210s passed
arithmetic data()[35] 8m16.26s passed
arrays data()[36] 57.702s passed
javadl data()[37] 9m40.33s passed
FOL data()[38] 4m51.42s passed
strings data()[39] 2m35.34s passed
comprehensions data()[3] 1m8.37s passed
simple_info_flow data()[40] 13.568s passed
modelMethods data()[41] 3m4.13s passed
permissionHeap data()[42] 15m6.83s passed
completionScopes data()[43] 49.967s passed
reload_examples data()[44] 44.755s passed
proofLoadRepair data()[45] 18.994s passed
switch data()[46] 1m5.98s passed
redux data()[47] 2m10.15s failed
performance data()[4] 3m42.42s passed
performancePOConstruction data()[5] 1m18.91s passed
applicationRestrictions data()[6] 50.037s passed
blockContracts data()[7] 2m23.85s passed
jmlAsserts data()[8] 1m31.96s passed
javaCard data()[9] 32.472s passed

Standard output

08:49:14,364 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:49:14,364 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:49:14,419 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:49:14,420 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:49:14,424 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:49:14,428 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:49:14,429 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:49:14,429 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:49:14,442 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:49:14,442 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:49:14,442 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:49:14,443 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@19fb8826 - Registering current configuration as safe fallback point

Running test newBook
08:49:14,781 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:49:14,788 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:49:14,945 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:49:14,945 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:49:14,954 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:49:14,958 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:49:14,958 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:49:14,959 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:49:14,991 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:49:14,991 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:49:14,991 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:49:14,993 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

373        WARN  main            d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
	at java.base/java.io.FileInputStream.open0(Native Method)

Returning from test newBook
Running test oldBook
08:50:13,638 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:50:13,639 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:50:13,742 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:50:13,743 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:50:13,754 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:50:13,758 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:50:13,758 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:50:13,759 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:50:13,778 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:50:13,778 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:50:13,779 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:50:13,780 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

280        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test oldBook
Running test comprehensions
08:50:31,109 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:50:31,109 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:50:31,203 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:50:31,203 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:50:31,214 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:50:31,219 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:50:31,220 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:50:31,221 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:50:31,241 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:50:31,241 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:50:31,241 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:50:31,242 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

294        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test comprehensions
Running test performance
08:51:39,463 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:51:39,464 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:51:39,557 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:51:39,557 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:51:39,566 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:51:39,574 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:51:39,574 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:51:39,575 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:51:39,600 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:51:39,600 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:51:39,600 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:51:39,604 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

295        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test performance
Running test performancePOConstruction
08:55:21,869 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:55:21,871 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:55:21,976 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:55:21,977 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:55:21,988 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:55:21,992 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:55:21,992 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:55:21,994 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:55:22,036 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:55:22,036 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:55:22,038 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:55:22,039 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

288        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test performancePOConstruction
Running test applicationRestrictions
08:56:40,764 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:56:40,765 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:56:40,878 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:56:40,878 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:56:40,889 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:56:40,894 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:56:40,894 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:56:40,895 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:56:40,915 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:56:40,915 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:56:40,915 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:56:40,916 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

286        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test applicationRestrictions
Running test blockContracts
08:57:30,797 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:57:30,798 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:57:30,892 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:57:30,893 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:57:30,903 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:57:30,907 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:57:30,908 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:57:30,909 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:57:30,935 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:57:30,935 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:57:30,935 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:57:30,937 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

290        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test blockContracts
Running test jmlAsserts
08:59:54,648 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:59:54,648 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:59:54,753 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
08:59:54,754 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:59:54,771 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
08:59:54,775 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
08:59:54,775 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
08:59:54,776 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:59:54,812 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
08:59:54,812 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
08:59:54,812 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
08:59:54,814 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

299        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test jmlAsserts
Running test javaCard
09:01:26,608 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:01:26,608 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:01:26,722 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:01:26,722 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:01:26,735 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:01:26,739 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:01:26,739 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:01:26,741 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:01:26,760 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:01:26,760 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:01:26,761 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:01:26,762 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

272        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test javaCard
Running test project.key
09:01:59,077 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:01:59,078 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:01:59,195 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:01:59,195 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:01:59,205 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:01:59,214 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:01:59,214 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:01:59,215 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:01:59,236 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:01:59,236 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:01:59,236 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:01:59,238 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

286        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test project.key
Running test project.key#1
09:02:33,888 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:02:33,888 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:02:33,992 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:02:33,992 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:02:34,008 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:02:34,019 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:02:34,019 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:02:34,021 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:02:34,044 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:02:34,044 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:02:34,045 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:02:34,048 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

314        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test project.key#1
Running test lcp.key
09:02:48,385 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:02:48,386 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:02:48,478 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:02:48,478 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:02:48,488 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:02:48,492 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:02:48,492 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:02:48,493 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:02:48,513 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:02:48,513 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:02:48,513 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:02:48,515 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

275        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test lcp.key
Running test project.key#2
09:03:04,005 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:03:04,006 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:03:04,101 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:03:04,101 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:03:04,116 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:03:04,120 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:03:04,121 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:03:04,122 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:03:04,142 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:03:04,142 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:03:04,142 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:03:04,144 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

268        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test project.key#2
Running test ArrayList_contains.key
09:03:22,779 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:03:22,780 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:03:22,901 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:03:22,901 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:03:22,914 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:03:22,921 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:03:22,922 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:03:22,923 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:03:22,950 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:03:22,950 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:03:22,950 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:03:22,952 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

290        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test ArrayList_contains.key
Running test ArrayList_get.key
09:03:36,547 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:03:36,548 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:03:36,647 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:03:36,647 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:03:36,665 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:03:36,669 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:03:36,670 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:03:36,671 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:03:36,689 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:03:36,689 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:03:36,690 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:03:36,691 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

271        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test ArrayList_get.key
Running test ArrayList_size.key
09:03:50,804 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:03:50,805 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:03:50,902 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:03:50,903 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:03:50,913 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:03:50,917 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:03:50,918 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:03:50,919 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:03:50,938 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:03:50,938 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:03:50,939 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:03:50,940 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

263        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test ArrayList_size.key
Running test UpdateAbstraction_ex7_3_secure.key
09:04:03,739 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:04:03,740 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:04:03,843 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:04:03,844 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:04:03,860 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:04:03,864 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:04:03,864 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:04:03,865 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:04:03,887 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:04:03,887 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:04:03,887 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:04:03,889 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

287        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test UpdateAbstraction_ex7_3_secure.key
Running test UpdateAbstraction_ex7_4_secure.key
09:04:16,844 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:04:16,845 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:04:16,951 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:04:16,952 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:04:16,963 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:04:16,967 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:04:16,968 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:04:16,969 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:04:16,988 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:04:16,989 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:04:16,989 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:04:16,990 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

298        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test UpdateAbstraction_ex7_4_secure.key
Running test UpdateAbstraction_ex7_5_secure.key
09:04:30,460 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:04:30,461 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:04:30,557 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:04:30,557 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:04:30,573 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:04:30,578 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:04:30,578 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:04:30,579 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:04:30,607 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:04:30,607 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:04:30,608 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:04:30,612 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

298        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test UpdateAbstraction_ex7_5_secure.key
Running test UpdateAbstraction_ex7_6_secure.key
09:04:43,424 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:04:43,425 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:04:43,541 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:04:43,541 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:04:43,552 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:04:43,557 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:04:43,557 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:04:43,558 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:04:43,579 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:04:43,579 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:04:43,579 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:04:43,581 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

277        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test UpdateAbstraction_ex7_6_secure.key
Running test UpdateAbstraction_ex9_secure.key
09:04:56,825 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:04:56,826 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:04:56,930 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:04:56,930 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:04:56,940 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:04:56,945 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:04:56,945 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:04:56,946 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:04:56,966 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:04:56,966 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:04:56,966 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:04:56,968 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

292        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test UpdateAbstraction_ex9_secure.key
Running test list
09:05:11,648 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:05:11,649 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:05:11,746 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:05:11,747 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:05:11,757 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:05:11,761 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:05:11,761 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:05:11,762 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:05:11,782 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:05:11,782 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:05:11,782 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:05:11,784 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

271        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test list
Running test list_ghost
09:09:46,960 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:09:46,961 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:09:47,061 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:09:47,061 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:09:47,071 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:09:47,075 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:09:47,075 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:09:47,076 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:09:47,097 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:09:47,097 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:09:47,097 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:09:47,099 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

279        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test list_ghost
Running test list_recursive
09:10:55,197 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:10:55,198 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:10:55,314 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:10:55,314 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:10:55,324 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:10:55,328 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:10:55,328 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:10:55,329 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:10:55,349 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:10:55,349 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:10:55,349 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:10:55,351 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

298        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test list_recursive
Running test list_seq
09:11:17,407 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:11:17,408 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:11:17,506 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:11:17,507 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:11:17,521 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:11:17,525 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:11:17,526 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:11:17,527 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:11:17,564 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:11:17,564 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:11:17,565 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:11:17,566 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

285        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test list_seq
Running test observer
09:13:44,489 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:13:44,490 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:13:44,585 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:13:44,585 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:13:44,604 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:13:44,612 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:13:44,613 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:13:44,616 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:13:44,638 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:13:44,638 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:13:44,638 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:13:44,640 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

293        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test observer
Running test removeDups
09:15:23,540 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:15:23,541 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:15:23,671 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:15:23,673 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:15:23,684 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:15:23,689 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:15:23,689 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:15:23,690 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:15:23,711 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:15:23,711 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:15:23,711 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:15:23,713 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

287        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test removeDups
Running test Saddleback_search.key
09:16:03,349 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:16:03,350 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:16:03,467 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:16:03,468 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:16:03,480 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:16:03,484 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:16:03,484 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:16:03,488 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:16:03,518 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:16:03,518 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:16:03,518 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:16:03,520 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

292        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test Saddleback_search.key
Running test quicksort
09:17:38,950 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:17:38,954 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:17:39,060 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:17:39,060 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:17:39,073 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:17:39,077 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:17:39,077 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:17:39,078 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:17:39,097 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:17:39,097 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:17:39,098 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:17:39,099 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

278        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test quicksort
Running test simpleTests
09:19:21,983 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:19:21,984 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:19:22,086 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:19:22,087 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:19:22,098 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:19:22,102 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:19:22,102 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:19:22,104 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:19:22,138 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:19:22,138 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:19:22,139 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:19:22,140 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

290        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test simpleTests
Running test SmansEtAl
09:22:04,961 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:22:04,962 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:22:05,061 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:22:05,061 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:22:05,076 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:22:05,081 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:22:05,081 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:22:05,082 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:22:05,102 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:22:05,102 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:22:05,102 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:22:05,104 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

287        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test SmansEtAl
Running test VACID0
09:25:22,942 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:25:22,943 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:25:23,035 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:25:23,036 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:25:23,046 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:25:23,052 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:25:23,052 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:25:23,053 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:25:23,074 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:25:23,074 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:25:23,074 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:25:23,076 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

265        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test VACID0
Running test VSTTE10
09:26:41,569 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:26:41,570 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:26:41,676 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:26:41,677 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:26:41,689 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:26:41,693 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:26:41,694 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:26:41,695 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:26:41,714 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:26:41,715 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:26:41,715 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:26:41,717 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

270        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test VSTTE10
Running test WeideEtAl
09:29:39,110 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:29:39,111 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:29:39,220 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:29:39,220 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:29:39,230 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:29:39,235 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:29:39,235 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:29:39,236 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:29:39,272 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:29:39,272 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:29:39,272 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:29:39,274 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

295        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test WeideEtAl
Running test arithmetic
09:30:09,323 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:30:09,324 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:30:09,426 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:30:09,426 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:30:09,435 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:30:09,440 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:30:09,441 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:30:09,442 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:30:09,476 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:30:09,476 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:30:09,477 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:30:09,478 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

309        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test arithmetic
Running test arrays
09:38:25,579 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:38:25,580 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:38:25,693 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:38:25,694 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:38:25,704 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:38:25,708 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:38:25,709 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:38:25,710 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:38:25,729 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:38:25,729 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:38:25,729 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:38:25,731 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

282        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test arrays
Running test javadl
09:39:23,297 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:39:23,298 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:39:23,406 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:39:23,406 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:39:23,417 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:39:23,424 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:39:23,425 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:39:23,426 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:39:23,450 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:39:23,450 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:39:23,450 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:39:23,452 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

306        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
47980      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
47980      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
47981      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
50898      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
50898      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
50898      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
58973      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
58973      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
58973      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
61767      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
61768      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
61770      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
83307      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
83308      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
83308      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
86086      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
86087      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
86087      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
88666      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
88667      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
88667      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
91550      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
91552      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
91552      WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
129592     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
129592     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
129592     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
132509     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
132510     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
132510     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
145518     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
145519     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
145519     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
148343     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
148344     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
148344     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
359018     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
359018     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
359018     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
366041     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
366041     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
366042     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
369160     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
369161     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
369163     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
373445     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
373445     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
373446     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
503647     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
503647     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
503647     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
507004     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
507005     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java 
507005     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
509473     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
509473     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
513125     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
513126     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
515679     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
515679     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
518704     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
518705     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
521120     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
521120     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
524181     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
524182     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
526671     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
526672     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
529859     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
529859     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
532323     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
532324     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
535462     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
535462     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
537936     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
537936     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
552567     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
552568     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
557177     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
557178     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
560527     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java 
560527     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java 
568343     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype cp.C declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.class and once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml, Keeping one from FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml 
571484     WARN  main            d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype cp.C declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.class and once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml, Keeping one from FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml 
Returning from test javadl
Running test FOL
09:49:03,616 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:49:03,616 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:49:03,710 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:49:03,710 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:49:03,721 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:49:03,725 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:49:03,726 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:49:03,727 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:49:03,747 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:49:03,747 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:49:03,747 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:49:03,749 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

285        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test FOL
Running test strings
09:53:55,029 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:53:55,029 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:53:55,132 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:53:55,133 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:53:55,147 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:53:55,151 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:53:55,151 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:53:55,152 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:53:55,171 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:53:55,171 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:53:55,172 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:53:55,173 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

287        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test strings
Running test simple_info_flow
09:56:30,362 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:56:30,363 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:56:30,468 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:56:30,469 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:56:30,481 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:56:30,486 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:56:30,486 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:56:30,487 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:56:30,515 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:56:30,515 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:56:30,516 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:56:30,518 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

283        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test simple_info_flow
Running test modelMethods
09:56:43,941 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:56:43,941 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:56:44,044 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:56:44,045 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:56:44,056 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:56:44,064 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:56:44,064 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:56:44,065 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:56:44,088 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:56:44,088 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:56:44,088 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:56:44,094 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

316        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test modelMethods
Running test permissionHeap
09:59:48,067 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
09:59:48,068 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
09:59:48,169 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
09:59:48,169 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
09:59:48,180 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
09:59:48,184 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
09:59:48,184 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
09:59:48,185 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
09:59:48,227 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
09:59:48,231 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
09:59:48,232 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
09:59:48,237 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

302        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
905895     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
905900     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
905902     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
905903     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
905904     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter 
905906     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
905907     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
905909     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
905911     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
905913     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
905914     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
905915     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
905916     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
905917     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
905917     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
905918     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
905919     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
905920     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
905921     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
905921     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
905922     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
905922     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter 
Returning from test permissionHeap
Running test completionScopes
10:14:54,909 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:14:54,910 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:14:55,011 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
10:14:55,012 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:14:55,024 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
10:14:55,032 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
10:14:55,033 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
10:14:55,036 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:14:55,074 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
10:14:55,074 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
10:14:55,074 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
10:14:55,076 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

299        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test completionScopes
Running test reload_examples
10:15:44,858 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:15:44,858 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:15:44,964 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
10:15:44,965 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:15:44,975 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
10:15:44,979 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
10:15:44,980 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
10:15:44,981 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:15:45,000 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
10:15:45,000 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
10:15:45,000 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
10:15:45,002 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

292        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test reload_examples
Running test proofLoadRepair
10:16:29,610 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:16:29,611 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:16:29,703 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
10:16:29,704 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:16:29,723 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
10:16:29,728 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
10:16:29,728 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
10:16:29,729 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:16:29,750 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
10:16:29,750 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
10:16:29,750 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
10:16:29,752 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

267        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
7909       WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft 
7910       WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right 
7914       WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close 
10863      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for applyEq 
Returning from test proofLoadRepair
Running test switch
10:16:48,606 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:16:48,606 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:16:48,716 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
10:16:48,717 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:16:48,727 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
10:16:48,732 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
10:16:48,732 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
10:16:48,733 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:16:48,756 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
10:16:48,757 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
10:16:48,757 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
10:16:48,760 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

296        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test switch
Running test redux
10:17:54,589 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:17:54,589 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:17:54,706 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
10:17:54,706 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:17:54,716 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
10:17:54,720 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
10:17:54,720 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
10:17:54,721 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:17:54,745 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
10:17:54,745 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
10:17:54,745 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
10:17:54,747 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

282        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read.

Standard error

Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Feb 24, 2023 9:17:55 AM de.uka.ilkd.key.macros.scripts.ScriptCommand execute
INFO: Included script /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/sort.script
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
SMT Runtime, goal 17: 49 ms; valid
java.lang.Exception: Exception while loading proof (see cause for details): /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOf.float.key.proof
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.reloadProof(TestFile.java:311)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.reload(TestFile.java:241)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.runKey(TestFile.java:215)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.ForkedTestFileRunner.main(ForkedTestFileRunner.java:171)
Caused by: org.opentest4j.AssertionFailedError: Reloaded proof did not close: /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOf.float.key.proof, open goals were [17] ==> expected: <true> but was: <false>
	at org.junit.jupiter.api.AssertionUtils.fail(AssertionUtils.java:55)
	at org.junit.jupiter.api.AssertTrue.assertTrue(AssertTrue.java:40)
	at org.junit.jupiter.api.Assertions.assertTrue(Assertions.java:210)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.reloadProof(TestFile.java:308)
	... 3 more
SMT Runtime, goal 27: 37 ms; valid
java.lang.Exception: Exception while loading proof (see cause for details): /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOfRange.float.key.proof
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.reloadProof(TestFile.java:311)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.reload(TestFile.java:241)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.runKey(TestFile.java:215)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.ForkedTestFileRunner.main(ForkedTestFileRunner.java:171)
Caused by: org.opentest4j.AssertionFailedError: Reloaded proof did not close: /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOfRange.float.key.proof, open goals were [27] ==> expected: <true> but was: <false>
	at org.junit.jupiter.api.AssertionUtils.fail(AssertionUtils.java:55)
	at org.junit.jupiter.api.AssertTrue.assertTrue(AssertTrue.java:40)
	at org.junit.jupiter.api.Assertions.assertTrue(Assertions.java:210)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile.reloadProof(TestFile.java:308)
	... 3 more
Exception in thread "main" org.opentest4j.AssertionFailedError: Exception during the execution of proofs. See log for more details.
	at org.junit.jupiter.api.AssertionUtils.fail(AssertionUtils.java:39)
	at org.junit.jupiter.api.Assertions.fail(Assertions.java:134)
	at de.uka.ilkd.key.proof.runallproofs.proofcollection.ForkedTestFileRunner.main(ForkedTestFileRunner.java:192)