RunAllProofsFunctional

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

tests
0

failures
0

ignored
1h58m4.80s

duration
100%

successful

Tests

Test Method name Duration Result
project.key data()[10] 49.119s passed
project.key#1 data()[11] 20.077s passed
lcp.key data()[12] 22.203s passed
project.key#2 data()[13] 27.182s passed
ArrayList_contains.key data()[14] 19.238s passed
ArrayList_get.key data()[15] 20.510s passed
ArrayList_size.key data()[16] 18.579s passed
UpdateAbstraction_ex7_3_secure.key data()[17] 17.681s passed
UpdateAbstraction_ex7_4_secure.key data()[18] 17.832s passed
UpdateAbstraction_ex7_5_secure.key data()[19] 17.576s passed
newBook data()[1] 1m20.96s passed
UpdateAbstraction_ex7_6_secure.key data()[20] 18.224s passed
UpdateAbstraction_ex9_secure.key data()[21] 19.966s passed
list data()[22] 5m47.28s passed
list_ghost data()[23] 1m30.08s passed
list_recursive data()[24] 31.640s passed
list_seq data()[25] 3m26.14s passed
observer data()[26] 2m7.13s passed
removeDups data()[27] 51.886s passed
Saddleback_search.key data()[28] 2m3.58s passed
quicksort data()[29] 2m20.25s passed
oldBook data()[2] 23.795s passed
simpleTests data()[30] 3m24.32s passed
SmansEtAl data()[31] 4m10.44s passed
VACID0 data()[32] 1m42.78s passed
VSTTE10 data()[33] 4m5.68s passed
WeideEtAl data()[34] 38.351s passed
arithmetic data()[35] 10m57.31s passed
arrays data()[36] 1m14.44s passed
javadl data()[37] 13m34.95s passed
FOL data()[38] 6m5.74s passed
strings data()[39] 3m16.85s passed
comprehensions data()[3] 1m27.94s passed
simple_info_flow data()[40] 18.338s passed
modelMethods data()[41] 3m59.63s passed
permissionHeap data()[42] 17m50.35s passed
completionScopes data()[43] 1m7.11s passed
reload_examples data()[44] 58.951s passed
proofLoadRepair data()[45] 26.209s passed
switch data()[46] 1m22.81s passed
redux data()[47] 2m51.66s passed
performance data()[4] 5m7.46s passed
performancePOConstruction data()[5] 1m44.85s passed
applicationRestrictions data()[6] 1m3.18s passed
blockContracts data()[7] 3m3.99s passed
jmlAsserts data()[8] 1m57.46s passed
javaCard data()[9] 43.082s passed

Standard output

13:32:29,165 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:32:29,200 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:32:29,215 |-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]
13:32:29,397 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:32:29,399 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:32:29,430 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:32:29,430 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:32:29,432 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:32:29,455 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:32:29,467 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:32:29,467 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@64bc21ac - End of configuration.
13:32:29,468 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@493dfb8e - Registering current configuration as safe fallback point

Running test newBook
13:32:29,903 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:32:29,953 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:32:29,978 |-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]
13:32:30,217 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:32:30,217 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:32:30,238 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:32:30,238 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:32:30,240 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:32:30,268 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:32:30,276 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:32:30,276 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:32:30,277 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

528        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
13:33:50,882 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:33:50,921 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:33:50,946 |-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]
13:33:51,165 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:33:51,165 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:33:51,187 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:33:51,187 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:33:51,188 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:33:51,213 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:33:51,222 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:33:51,222 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@1ff4931d - End of configuration.
13:33:51,223 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@65e98b1c - Registering current configuration as safe fallback point

486        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
13:34:14,595 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:34:14,627 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:34:14,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]
13:34:14,850 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:34:14,851 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:34:14,872 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:34:14,872 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:34:14,873 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:34:14,901 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:34:14,907 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:34:14,907 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:34:14,908 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

450        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
13:35:42,547 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:35:42,584 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:35:42,609 |-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]
13:35:42,824 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:35:42,824 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:35:42,845 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:35:42,845 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:35:42,847 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:35:42,875 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:35:42,882 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:35:42,883 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:35:42,884 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

516        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
13:40:50,005 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:40:50,068 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:40:50,104 |-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]
13:40:50,310 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:40:50,310 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:40:50,335 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:40:50,335 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:40:50,337 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:40:50,364 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:40:50,371 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:40:50,371 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:40:50,372 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

511        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
13:42:34,854 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:42:34,899 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:42:34,926 |-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]
13:42:35,147 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:42:35,148 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:42:35,170 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:42:35,171 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:42:35,172 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:42:35,214 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:42:35,233 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:42:35,234 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@1ff4931d - End of configuration.
13:42:35,235 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@65e98b1c - Registering current configuration as safe fallback point

569        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
13:43:38,060 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:43:38,116 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:43:38,156 |-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]
13:43:38,397 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:43:38,398 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:43:38,423 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:43:38,423 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:43:38,424 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:43:38,451 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:43:38,457 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:43:38,457 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:43:38,458 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

555        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
13:46:42,036 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:46:42,082 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:46:42,127 |-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]
13:46:42,346 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:46:42,346 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:46:42,366 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:46:42,366 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:46:42,368 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:46:42,413 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:46:42,431 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:46:42,432 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:46:42,433 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

575        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
13:48:39,479 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:48:39,513 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:48:39,549 |-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]
13:48:39,763 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:48:39,763 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:48:39,799 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:48:39,799 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:48:39,800 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:48:39,836 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:48:39,843 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:48:39,843 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:48:39,844 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

527        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
13:49:22,562 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:49:22,598 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:49:22,627 |-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]
13:49:22,831 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:49:22,832 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:49:22,852 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:49:22,852 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:49:22,854 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:49:22,882 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:49:22,888 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:49:22,889 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:49:22,890 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

478        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
13:50:11,679 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:50:11,730 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:50:11,776 |-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]
13:50:11,984 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:50:11,985 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:50:12,005 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:50:12,005 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:50:12,006 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:50:12,036 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:50:12,043 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:50:12,043 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:50:12,044 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

548        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
13:50:31,767 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:50:31,808 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:50:31,833 |-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]
13:50:32,056 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:50:32,057 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:50:32,086 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:50:32,086 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:50:32,092 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:50:32,138 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:50:32,155 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:50:32,156 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:50:32,156 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

587        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
13:50:53,955 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:50:54,006 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:50:54,042 |-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]
13:50:54,239 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:50:54,239 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:50:54,259 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:50:54,259 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:50:54,260 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:50:54,293 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:50:54,300 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:50:54,301 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:50:54,302 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

525        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
13:51:21,187 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:51:21,234 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:51:21,255 |-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]
13:51:21,515 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:51:21,515 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:51:21,544 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:51:21,544 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:51:21,545 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:51:21,598 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:51:21,613 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:51:21,614 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:51:21,615 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

629        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
13:51:40,404 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:51:40,441 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:51:40,467 |-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]
13:51:40,703 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:51:40,703 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:51:40,724 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:51:40,724 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:51:40,726 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:51:40,756 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:51:40,763 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:51:40,764 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:51:40,765 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

531        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
13:52:00,904 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:52:00,951 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:52:00,982 |-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]
13:52:01,205 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:52:01,206 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:52:01,242 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:52:01,242 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:52:01,243 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:52:01,272 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:52:01,278 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:52:01,279 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:52:01,279 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

572        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
13:52:19,467 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:52:19,508 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:52:19,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]
13:52:19,754 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:52:19,755 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:52:19,775 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:52:19,775 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:52:19,777 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:52:19,807 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:52:19,815 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:52:19,815 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:52:19,816 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

508        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
13:52:37,156 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:52:37,196 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:52:37,220 |-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]
13:52:37,440 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:52:37,441 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:52:37,460 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:52:37,460 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:52:37,461 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:52:37,488 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:52:37,495 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:52:37,495 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:52:37,496 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

490        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
13:52:54,979 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:52:55,014 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:52:55,039 |-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]
13:52:55,291 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:52:55,292 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:52:55,313 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:52:55,313 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:52:55,314 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:52:55,341 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:52:55,348 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:52:55,349 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:52:55,350 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

540        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
13:53:12,566 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:53:12,606 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:53:12,632 |-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]
13:53:12,847 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:53:12,848 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:53:12,870 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:53:12,870 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:53:12,871 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:53:12,899 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:53:12,912 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:53:12,912 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:53:12,913 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

495        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
13:53:30,772 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:53:30,808 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:53:30,832 |-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]
13:53:31,036 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:53:31,037 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:53:31,060 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:53:31,060 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:53:31,062 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:53:31,102 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:53:31,109 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:53:31,109 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:53:31,110 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

507        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
13:53:50,739 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:53:50,778 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:53:50,801 |-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]
13:53:51,055 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:53:51,056 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:53:51,083 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:53:51,083 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:53:51,084 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:53:51,129 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:53:51,145 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:53:51,146 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:53:51,147 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

592        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
13:59:38,042 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
13:59:38,082 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
13:59:38,125 |-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]
13:59:38,368 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
13:59:38,368 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
13:59:38,397 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
13:59:38,398 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
13:59:38,399 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
13:59:38,444 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
13:59:38,460 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
13:59:38,460 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
13:59:38,461 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

597        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
14:01:08,110 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:01:08,152 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:01:08,190 |-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]
14:01:08,382 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:01:08,382 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:01:08,402 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:01:08,402 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:01:08,403 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:01:08,440 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:01:08,446 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:01:08,447 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:01:08,448 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

500        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
14:01:39,769 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:01:39,814 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:01:39,842 |-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]
14:01:40,066 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:01:40,066 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:01:40,105 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:01:40,105 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:01:40,106 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:01:40,161 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:01:40,174 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:01:40,174 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:01:40,175 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

628        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
14:05:05,885 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:05:05,922 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:05:05,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]
14:05:06,144 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:05:06,144 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:05:06,167 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:05:06,167 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:05:06,168 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:05:06,206 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:05:06,225 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:05:06,226 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:05:06,227 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

553        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
14:07:13,033 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:07:13,071 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:07:13,098 |-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]
14:07:13,301 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:07:13,302 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:07:13,343 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:07:13,343 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:07:13,344 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:07:13,386 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:07:13,403 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:07:13,404 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:07:13,405 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

571        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
14:08:04,887 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:08:04,940 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:08:04,959 |-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]
14:08:05,194 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:08:05,194 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:08:05,221 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:08:05,222 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:08:05,223 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:08:05,267 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:08:05,282 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:08:05,282 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:08:05,283 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

564        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
14:10:08,495 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:10:08,540 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:10:08,565 |-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]
14:10:08,755 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:10:08,755 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:10:08,776 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:10:08,776 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:10:08,777 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:10:08,805 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:10:08,825 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:10:08,826 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:10:08,827 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

509        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
14:12:28,726 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:12:28,766 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:12:28,800 |-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]
14:12:28,992 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:12:28,992 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:12:29,011 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:12:29,011 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:12:29,012 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:12:29,049 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:12:29,054 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:12:29,055 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:12:29,056 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

497        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
14:15:53,067 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:15:53,112 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:15:53,147 |-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]
14:15:53,374 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:15:53,374 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:15:53,398 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:15:53,398 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:15:53,399 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:15:53,441 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:15:53,455 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:15:53,456 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:15:53,457 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

603        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
14:20:03,492 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:20:03,545 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:20:03,574 |-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]
14:20:03,769 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:20:03,769 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:20:03,791 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:20:03,791 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:20:03,793 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:20:03,823 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:20:03,837 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:20:03,842 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:20:03,843 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

523        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
14:21:46,278 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:21:46,312 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:21:46,353 |-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]
14:21:46,594 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:21:46,594 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:21:46,622 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:21:46,622 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:21:46,623 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:21:46,664 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:21:46,674 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:21:46,675 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:21:46,675 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

594        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
14:25:51,975 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:25:52,016 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:25:52,040 |-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]
14:25:52,282 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:25:52,282 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:25:52,305 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:25:52,305 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:25:52,307 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:25:52,350 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:25:52,372 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:25:52,373 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:25:52,374 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

578        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
14:26:30,318 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:26:30,368 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:26:30,392 |-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]
14:26:30,651 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:26:30,651 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:26:30,691 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:26:30,691 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:26:30,694 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:26:30,743 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:26:30,749 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:26:30,750 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:26:30,751 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

593        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
14:37:27,618 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:37:27,653 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:37:27,676 |-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]
14:37:27,879 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:37:27,880 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:37:27,901 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:37:27,901 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:37:27,902 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:37:27,952 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:37:27,974 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:37:27,975 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:37:27,976 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

515        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
14:38:42,080 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:38:42,121 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:38:42,145 |-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]
14:38:42,368 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:38:42,368 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:38:42,396 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:38:42,396 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:38:42,397 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:38:42,440 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:38:42,457 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:38:42,458 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:38:42,461 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

576        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
66660      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 
66660      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 
66660      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 
70673      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 
70673      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 
70673      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 
81520      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 
81528      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 
81533      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 
85192      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 
85193      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 
85193      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 
113628     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 
113628     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 
113629     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 
117395     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 
117397     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 
117397     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 
120859     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 
120859     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 
120859     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 
124878     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 
124878     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 
124878     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 
174957     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 
174959     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 
174959     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 
179049     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 
179050     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 
179051     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 
197087     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 
197087     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 
197089     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 
200853     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 
200854     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 
200854     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 
499974     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 
499974     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 
499974     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 
510485     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 
510489     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 
510490     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 
514895     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 
514896     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 
514897     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 
520963     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 
520963     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 
520964     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 
708875     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 
708876     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 
708876     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 
713526     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 
713527     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 
713527     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 
716862     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 
716862     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 
721938     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 
721938     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 
725441     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 
725441     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 
729622     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 
729622     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 
733005     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 
733006     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 
737012     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 
737013     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 
740215     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 
740215     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 
744509     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 
744510     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 
747830     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 
747831     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 
752256     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 
752257     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 
755565     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 
755565     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 
776749     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 
776749     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 
783212     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 
783213     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 
787834     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 
787835     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 
798588     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 
802865     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
14:52:17,037 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:52:17,076 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:52:17,102 |-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]
14:52:17,294 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:52:17,294 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:52:17,316 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:52:17,316 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:52:17,317 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:52:17,345 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:52:17,352 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:52:17,353 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:52:17,354 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

498        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
14:58:22,794 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
14:58:22,834 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
14:58:22,861 |-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]
14:58:23,098 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
14:58:23,098 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
14:58:23,122 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
14:58:23,122 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
14:58:23,127 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
14:58:23,160 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
14:58:23,168 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
14:58:23,168 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
14:58:23,169 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

561        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
15:01:39,611 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:01:39,647 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:01:39,672 |-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]
15:01:39,915 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:01:39,916 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:01:39,935 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:01:39,935 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:01:39,937 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:01:39,980 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:01:39,990 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:01:39,991 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:01:39,992 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

590        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
15:01:57,954 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:01:57,993 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:01:58,016 |-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]
15:01:58,215 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:01:58,215 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:01:58,246 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:01:58,247 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:01:58,248 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:01:58,287 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:01:58,296 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:01:58,297 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:01:58,298 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

498        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
15:05:57,577 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:05:57,620 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:05:57,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]
15:05:57,870 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:05:57,870 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:05:57,895 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:05:57,895 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:05:57,898 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:05:57,944 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:05:57,962 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:05:57,963 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:05:57,964 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

622        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
1068901    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
1068905    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
1068915    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
1068916    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
1068918    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter 
1068920    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
1068923    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
1068926    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
1068929    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
1068932    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
1068933    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
1068935    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
1068936    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
1068937    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
1068939    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
1068940    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1068941    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
1068943    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
1068944    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1068945    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1068946    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1068949    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
15:23:47,906 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:23:47,939 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:23:47,960 |-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]
15:23:48,197 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:23:48,197 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:23:48,224 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:23:48,224 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:23:48,225 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:23:48,268 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:23:48,284 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:23:48,285 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:23:48,286 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

559        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
15:24:55,050 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:24:55,100 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:24:55,134 |-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]
15:24:55,317 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:24:55,317 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:24:55,337 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:24:55,337 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:24:55,338 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:24:55,364 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:24:55,371 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:24:55,372 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:24:55,373 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

499        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
15:25:53,988 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:25:54,031 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:25:54,067 |-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]
15:25:54,272 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:25:54,272 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:25:54,294 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:25:54,294 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:25:54,296 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:25:54,325 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:25:54,333 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:25:54,334 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:25:54,335 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

503        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
11273      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft 
11274      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right 
11278      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close 
15386      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
15:26:20,205 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:26:20,250 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:26:20,284 |-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]
15:26:20,504 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:26:20,504 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:26:20,521 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:26:20,521 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:26:20,523 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:26:20,549 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:26:20,556 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:26:20,557 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:26:20,558 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

508        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
15:27:43,000 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
15:27:43,035 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
15:27:43,082 |-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]
15:27:43,293 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
15:27:43,294 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
15:27:43,323 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
15:27:43,323 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
15:27:43,324 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
15:27:43,375 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
15:27:43,394 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
15:27:43,395 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
15:27:43,401 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

591        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test redux

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.)
Mar 30, 2023 2:10:30 PM 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: 54 ms; valid
SMT Runtime, goal 27: 44 ms; valid