RunAllProofsFunctional

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

tests
0

failures
0

ignored
1h45m2.86s

duration
100%

successful

Tests

Test Method name Duration Result
project.key data()[10] 42.257s passed
project.key#1 data()[11] 16.177s passed
lcp.key data()[12] 18.415s passed
project.key#2 data()[13] 22.475s passed
ArrayList_contains.key data()[14] 15.811s passed
ArrayList_get.key data()[15] 17.312s passed
ArrayList_size.key data()[16] 15.259s passed
UpdateAbstraction_ex7_3_secure.key data()[17] 15.731s passed
UpdateAbstraction_ex7_4_secure.key data()[18] 15.623s passed
UpdateAbstraction_ex7_5_secure.key data()[19] 14.968s passed
newBook data()[1] 1m8.22s passed
UpdateAbstraction_ex7_6_secure.key data()[20] 16.607s passed
UpdateAbstraction_ex9_secure.key data()[21] 17.527s passed
list data()[22] 5m19.94s passed
list_ghost data()[23] 1m20.29s passed
list_recursive data()[24] 26.485s passed
list_seq data()[25] 3m2.77s passed
observer data()[26] 1m56.55s passed
removeDups data()[27] 47.782s passed
Saddleback_search.key data()[28] 1m46.97s passed
quicksort data()[29] 2m4.05s passed
oldBook data()[2] 20.952s passed
simpleTests data()[30] 3m7.58s passed
SmansEtAl data()[31] 3m50.78s passed
VACID0 data()[32] 1m34.00s passed
VSTTE10 data()[33] 3m38.73s passed
WeideEtAl data()[34] 34.019s passed
arithmetic data()[35] 9m31.72s passed
arrays data()[36] 1m7.48s passed
javadl data()[37] 11m26.16s passed
FOL data()[38] 5m24.79s passed
strings data()[39] 3m2.57s passed
comprehensions data()[3] 1m16.81s passed
simple_info_flow data()[40] 15.503s passed
modelMethods data()[41] 3m37.18s passed
permissionHeap data()[42] 16m39.05s passed
completionScopes data()[43] 1m0.68s passed
reload_examples data()[44] 52.519s passed
proofLoadRepair data()[45] 21.872s passed
switch data()[46] 1m13.01s passed
redux data()[47] 2m30.78s passed
performance data()[4] 4m30.39s passed
performancePOConstruction data()[5] 1m25.72s passed
applicationRestrictions data()[6] 58.382s passed
blockContracts data()[7] 2m35.45s passed
jmlAsserts data()[8] 1m48.28s passed
javaCard data()[9] 37.237s passed

Standard output

10:09:53,248 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:09:53,289 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:09:53,302 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:09:53,682 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:09:53,683 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:09:53,710 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:09:53,710 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:09:53,712 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:09:53,728 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:09:53,739 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:09:53,739 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@64bc21ac - End of configuration.
10:09:53,740 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@493dfb8e - Registering current configuration as safe fallback point

Running test newBook
10:09:54,160 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:09:54,195 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:09:54,214 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:09:54,426 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:09:54,427 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:09:54,448 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:09:54,448 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:09:54,450 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:09:54,482 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:09:54,495 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:09:54,496 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@1ff4931d - End of configuration.
10:09:54,497 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@65e98b1c - Registering current configuration as safe fallback point

493        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
10:11:02,276 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:11:02,304 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:11:02,330 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:11:02,540 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:11:02,540 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:11:02,576 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:11:02,576 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:11:02,577 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:11:02,599 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:11:02,604 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:11:02,605 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@1ff4931d - End of configuration.
10:11:02,606 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@65e98b1c - Registering current configuration as safe fallback point

462        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
10:11:23,231 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:11:23,262 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:11:23,283 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:11:23,503 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:11:23,504 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:11:23,520 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:11:23,520 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:11:23,521 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:11:23,543 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:11:23,549 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:11:23,549 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:11:23,550 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

440        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
10:12:40,064 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:12:40,105 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:12:40,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]
10:12:40,308 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:12:40,308 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:12:40,324 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:12:40,324 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:12:40,325 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:12:40,350 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:12:40,356 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:12:40,356 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:12:40,357 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

420        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
10:17:10,436 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:17:10,467 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:17:10,491 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:17:10,668 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:17:10,669 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:17:10,687 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:17:10,687 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:17:10,688 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:17:10,712 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:17:10,720 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:17:10,721 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:17:10,722 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

463        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
10:18:36,156 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:18:36,202 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:18:36,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]
10:18:36,415 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:18:36,415 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:18:36,441 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:18:36,441 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:18:36,442 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:18:36,484 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:18:36,500 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:18:36,501 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:18:36,502 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

518        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
10:19:34,557 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:19:34,603 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:19:34,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]
10:19:34,829 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:19:34,830 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:19:34,845 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:19:34,845 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:19:34,846 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:19:34,869 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:19:34,875 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:19:34,875 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:19:34,876 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

460        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
10:22:09,992 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:22:10,025 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:22:10,045 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:22:10,229 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:22:10,230 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:22:10,263 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:22:10,263 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:22:10,264 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:22:10,308 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:22:10,323 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:22:10,323 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:22:10,324 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

492        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
10:23:58,276 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:23:58,328 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:23:58,351 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:23:58,511 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:23:58,511 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:23:58,527 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:23:58,527 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:23:58,528 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:23:58,551 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:23:58,557 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:23:58,557 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:23:58,558 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

408        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
10:24:35,524 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:24:35,575 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:24:35,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]
10:24:35,815 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:24:35,815 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:24:35,830 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:24:35,830 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:24:35,835 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:24:35,868 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:24:35,876 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:24:35,876 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:24:35,877 |-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 project.key
Running test project.key#1
10:25:17,775 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:25:17,815 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:25:17,836 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:25:18,053 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:25:18,054 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:25:18,070 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:25:18,070 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:25:18,071 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:25:18,093 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:25:18,098 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:25:18,099 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:25:18,100 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

458        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
10:25:33,939 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:25:33,971 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:25:33,999 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:25:34,186 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:25:34,186 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:25:34,203 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:25:34,203 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:25:34,204 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:25:34,228 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:25:34,233 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:25:34,234 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:25:34,235 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

414        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
10:25:52,376 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:25:52,406 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:25:52,426 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:25:52,623 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:25:52,623 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:25:52,639 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:25:52,639 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:25:52,640 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:25:52,666 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:25:52,673 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:25:52,674 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:25:52,675 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

419        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
10:26:14,838 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:26:14,872 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:26:14,893 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:26:15,073 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:26:15,074 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:26:15,111 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:26:15,111 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:26:15,112 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:26:15,137 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:26:15,142 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:26:15,143 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:26:15,144 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

449        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
10:26:30,650 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:26:30,681 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:26:30,715 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:26:30,889 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:26:30,890 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:26:30,907 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:26:30,907 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:26:30,908 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:26:30,940 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:26:30,954 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:26:30,954 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:26:30,955 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

471        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
10:26:47,963 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:26:47,999 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:26:48,018 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:26:48,192 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:26:48,193 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:26:48,221 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:26:48,221 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:26:48,222 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:26:48,245 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:26:48,250 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:26:48,251 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:26:48,251 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

399        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
10:27:03,221 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:27:03,256 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:27:03,279 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:27:03,466 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:27:03,466 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:27:03,484 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:27:03,484 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:27:03,485 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:27:03,525 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:27:03,530 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:27:03,531 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:27:03,532 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

483        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
10:27:18,951 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:27:18,984 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:27:19,003 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:27:19,178 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:27:19,178 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:27:19,195 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:27:19,195 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:27:19,196 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:27:19,218 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:27:19,224 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:27:19,224 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:27:19,225 |-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 UpdateAbstraction_ex7_4_secure.key
Running test UpdateAbstraction_ex7_5_secure.key
10:27:34,572 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:27:34,624 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:27:34,647 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:27:34,843 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:27:34,843 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:27:34,859 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:27:34,859 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:27:34,860 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:27:34,883 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:27:34,889 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:27:34,889 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:27:34,890 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

431        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
10:27:49,545 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:27:49,582 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:27:49,612 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:27:49,840 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:27:49,840 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:27:49,856 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:27:49,856 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:27:49,857 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:27:49,881 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:27:49,886 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:27:49,887 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:27:49,887 |-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 UpdateAbstraction_ex7_6_secure.key
Running test UpdateAbstraction_ex9_secure.key
10:28:06,155 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:28:06,197 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:28:06,230 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:28:06,414 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:28:06,415 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:28:06,436 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:28:06,436 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:28:06,437 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:28:06,465 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:28:06,470 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:28:06,470 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:28:06,471 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

443        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
10:28:23,699 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:28:23,733 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:28:23,753 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:28:23,976 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:28:23,976 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:28:24,008 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:28:24,008 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:28:24,009 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:28:24,048 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:28:24,065 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:28:24,066 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:28:24,067 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

545        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
10:33:43,612 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:33:43,657 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:33:43,697 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:33:43,867 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:33:43,868 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:33:43,883 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:33:43,883 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:33:43,884 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:33:43,909 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:33:43,915 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:33:43,915 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:33:43,916 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

429        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
10:35:03,902 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:35:03,954 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:35:03,980 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:35:04,163 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:35:04,163 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:35:04,185 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:35:04,185 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:35:04,186 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:35:04,209 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:35:04,214 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:35:04,215 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:35:04,215 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

485        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
10:35:30,396 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:35:30,434 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:35:30,456 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:35:30,672 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:35:30,672 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:35:30,689 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:35:30,689 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:35:30,690 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:35:30,711 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:35:30,717 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:35:30,718 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:35:30,718 |-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 list_seq
Running test observer
10:38:33,160 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:38:33,194 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:38:33,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]
10:38:33,454 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:38:33,454 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:38:33,475 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:38:33,475 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:38:33,476 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:38:33,508 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:38:33,513 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:38:33,513 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:38:33,514 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

471        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
10:40:29,704 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:40:29,737 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:40:29,755 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:40:29,977 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:40:29,978 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:40:29,995 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:40:29,995 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:40:29,996 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:40:30,020 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:40:30,026 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:40:30,026 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:40:30,027 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

492        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
10:41:17,496 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:41:17,528 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:41:17,566 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:41:17,738 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:41:17,738 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:41:17,755 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:41:17,755 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:41:17,756 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:41:17,779 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:41:17,785 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:41:17,785 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:41:17,786 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

441        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
10:43:04,472 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:43:04,503 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:43:04,523 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:43:04,729 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:43:04,730 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:43:04,746 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:43:04,746 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:43:04,748 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:43:04,770 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:43:04,775 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:43:04,776 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:43:04,776 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

443        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
10:45:08,505 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:45:08,535 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:45:08,556 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:45:08,767 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:45:08,767 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:45:08,817 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:45:08,817 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:45:08,819 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:45:08,856 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:45:08,872 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:45:08,873 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:45:08,874 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

529        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
10:48:16,083 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:48:16,115 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:48:16,136 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:48:16,343 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:48:16,343 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:48:16,372 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:48:16,372 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:48:16,374 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:48:16,409 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:48:16,424 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:48:16,425 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:48:16,426 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

470        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
10:52:06,854 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:52:06,884 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:52:06,904 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:52:07,117 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:52:07,117 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:52:07,135 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:52:07,135 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:52:07,136 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:52:07,159 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:52:07,165 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:52:07,165 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:52:07,171 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

434        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
10:53:40,875 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:53:40,910 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:53:40,931 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:53:41,142 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:53:41,143 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:53:41,165 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:53:41,165 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:53:41,168 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:53:41,193 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:53:41,201 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:53:41,201 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:53:41,202 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

476        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
10:57:19,598 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:57:19,629 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:57:19,650 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:57:19,836 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:57:19,837 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:57:19,854 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:57:19,854 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:57:19,855 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:57:19,878 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:57:19,884 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:57:19,885 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:57:19,885 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

462        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
10:57:53,619 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
10:57:53,659 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
10:57:53,679 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
10:57:53,893 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
10:57:53,893 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
10:57:53,913 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
10:57:53,913 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
10:57:53,914 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
10:57:53,938 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
10:57:53,944 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
10:57:53,944 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
10:57:53,945 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

484        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
11:07:25,338 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:07:25,370 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:07:25,410 |-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]
11:07:25,601 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:07:25,601 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:07:25,619 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:07:25,619 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:07:25,620 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:07:25,657 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:07:25,675 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:07:25,676 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:07:25,677 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

519        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
11:08:32,817 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:08:32,851 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:08:32,872 |-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]
11:08:33,089 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:08:33,089 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:08:33,108 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:08:33,108 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:08:33,109 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:08:33,131 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:08:33,137 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:08:33,137 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:08:33,138 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

458        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
56314      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 
56314      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 
56314      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 
59800      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 
59800      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 
59801      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 
69080      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 
69081      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 
69082      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 
72343      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 
72344      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 
72344      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 
97355      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 
97355      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 
97355      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 
100539     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 
100539     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 
100540     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 
103440     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 
103441     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 
103442     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 
107099     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 
107099     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 
107099     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 
151436     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 
151436     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 
151438     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 
154800     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 
154801     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 
154802     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 
169792     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 
169792     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 
169792     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 
173162     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 
173163     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 
173163     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 
424753     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 
424753     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 
424754     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 
433484     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 
433484     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 
433484     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 
437107     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 
437107     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 
437107     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 
442249     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 
442249     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 
442249     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 
595670     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 
595670     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 
595670     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 
599603     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 
599605     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 
599607     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 
602459     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 
602459     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 
606860     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 
606861     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 
609819     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 
609819     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 
613347     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 
613348     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 
616208     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 
616208     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 
619628     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 
619628     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 
622410     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 
622411     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 
626068     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 
626069     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 
628866     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 
628867     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 
632622     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 
632622     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 
635382     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 
635382     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 
654119     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 
654119     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 
659475     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 
659475     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 
663432     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 
663432     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 
672471     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 
676114     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
11:19:58,971 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:19:59,004 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:19:59,023 |-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]
11:19:59,242 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:19:59,242 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:19:59,260 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:19:59,260 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:19:59,261 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:19:59,284 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:19:59,290 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:19:59,291 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:19:59,291 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

481        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
11:25:23,774 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:25:23,803 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:25:23,825 |-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]
11:25:24,030 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:25:24,030 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:25:24,047 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:25:24,047 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:25:24,048 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:25:24,070 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:25:24,075 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:25:24,076 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:25:24,077 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

453        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
11:28:26,336 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:28:26,364 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:28:26,386 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
11:28:26,569 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:28:26,569 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:28:26,610 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:28:26,610 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:28:26,611 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:28:26,653 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:28:26,667 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:28:26,667 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:28:26,669 |-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 simple_info_flow
Running test modelMethods
11:28:41,842 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:28:41,889 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:28:41,912 |-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]
11:28:42,091 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:28:42,091 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:28:42,109 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:28:42,109 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:28:42,110 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:28:42,135 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:28:42,149 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:28:42,150 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:28:42,151 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

471        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
11:32:19,023 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:32:19,053 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:32:19,072 |-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]
11:32:19,288 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:32:19,288 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:32:19,322 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:32:19,322 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:32:19,323 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:32:19,358 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:32:19,372 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:32:19,373 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:32:19,373 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

537        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
997532     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
997535     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
997546     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
997547     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
997548     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter 
997558     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
997560     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
997562     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
997564     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
997578     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
997579     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
997580     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
997581     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
997582     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
997583     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
997583     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
997590     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
997591     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
997592     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
997592     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
997593     WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
997594     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
11:48:58,082 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:48:58,120 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:48:58,140 |-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]
11:48:58,352 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:48:58,353 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:48:58,381 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:48:58,381 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:48:58,382 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:48:58,420 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:48:58,434 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:48:58,435 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:48:58,436 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

530        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
11:49:58,759 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:49:58,788 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:49:58,824 |-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]
11:49:59,025 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:49:59,025 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:49:59,041 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:49:59,041 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:49:59,042 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:49:59,065 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:49:59,070 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:49:59,071 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:49:59,072 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

437        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
11:50:51,275 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:50:51,305 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:50:51,325 |-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]
11:50:51,533 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:50:51,534 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:50:51,552 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:50:51,552 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:50:51,553 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:50:51,575 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:50:51,581 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:50:51,581 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:50:51,582 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

423        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
9565       WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft 
9567       WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right 
9573       WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close 
12968      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
11:51:13,148 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:51:13,178 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:51:13,199 |-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]
11:51:13,399 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:51:13,400 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:51:13,422 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:51:13,422 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:51:13,423 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:51:13,449 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:51:13,457 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:51:13,457 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:51:13,458 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

477        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
11:52:26,167 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
11:52:26,197 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
11:52:26,225 |-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]
11:52:26,408 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
11:52:26,409 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
11:52:26,427 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
11:52:26,427 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
11:52:26,428 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
11:52:26,452 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
11:52:26,457 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
11:52:26,458 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@710f4dc7 - End of configuration.
11:52:26,458 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@1ff4931d - Registering current configuration as safe fallback point

429        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 31, 2023 10:43:23 AM de.uka.ilkd.key.macros.scripts.ScriptCommand execute
INFO: Included script /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/sort.script
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
SMT Runtime, goal 17: 74 ms; valid
SMT Runtime, goal 27: 54 ms; valid