RunAllProofsFunctional

47

tests

0

failures

0

ignored

1h55m49.29s

duration

100%

successful

Tests

Test Method name Duration Result
project.key data()[10] 39.115s passed
project.key#1 data()[11] 18.987s passed
lcp.key data()[12] 21.320s passed
project.key#2 data()[13] 25.165s passed
ArrayList_contains.key data()[14] 18.105s passed
ArrayList_get.key data()[15] 19.178s passed
ArrayList_size.key data()[16] 18.312s passed
UpdateAbstraction_ex7_3_secure.key data()[17] 16.699s passed
UpdateAbstraction_ex7_4_secure.key data()[18] 18.177s passed
UpdateAbstraction_ex7_5_secure.key data()[19] 16.191s passed
newBook data()[1] 53.514s passed
UpdateAbstraction_ex7_6_secure.key data()[20] 18.998s passed
UpdateAbstraction_ex9_secure.key data()[21] 19.403s passed
list data()[22] 5m33.93s passed
list_ghost data()[23] 1m25.20s passed
list_recursive data()[24] 59.485s passed
list_seq data()[25] 3m7.67s passed
observer data()[26] 2m7.44s passed
removeDups data()[27] 49.659s passed
Saddleback_search.key data()[28] 1m47.19s passed
quicksort data()[29] 2m19.72s passed
oldBook data()[2] 21.911s passed
simpleTests data()[30] 3m31.51s passed
SmansEtAl data()[31] 4m8.22s passed
VACID0 data()[32] 1m40.13s passed
VSTTE10 data()[33] 3m49.21s passed
WeideEtAl data()[34] 37.689s passed
arithmetic data()[35] 10m42.21s passed
arrays data()[36] 1m16.47s passed
javadl data()[37] 13m33.88s passed
FOL data()[38] 6m12.71s passed
strings data()[39] 3m16.94s passed
comprehensions data()[3] 1m24.70s passed
simple_info_flow data()[40] 17.856s passed
modelMethods data()[41] 3m59.88s passed
permissionHeap data()[42] 17m58.85s passed
completionScopes data()[43] 1m6.12s passed
reload_examples data()[44] 54.755s passed
proofLoadRepair data()[45] 24.159s passed
switch data()[46] 1m22.09s passed
redux data()[47] 2m49.61s passed
performance data()[4] 4m45.16s passed
performancePOConstruction data()[5] 1m41.53s passed
applicationRestrictions data()[6] 1m3.54s passed
blockContracts data()[7] 2m58.22s passed
jmlAsserts data()[8] 1m55.56s passed
javaCard data()[9] 42.943s passed

Standard output

21:33:46,530 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:33:46,537 |-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]
21:33:46,635 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:33:46,635 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:33:46,641 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:33:46,645 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:33:46,645 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:33:46,647 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:33:46,665 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:33:46,666 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:33:46,666 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:33:46,666 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@19fb8826 - Registering current configuration as safe fallback point

Running test newBook
21:33:47,039 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:33:47,040 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
21:33:47,168 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:33:47,169 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:33:47,193 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:33:47,198 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:33:47,199 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:33:47,200 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:33:47,240 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:33:47,240 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:33:47,240 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:33:47,242 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

376        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
21:34:40,620 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:34:40,622 |-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]
21:34:40,764 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:34:40,764 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:34:40,775 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:34:40,780 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:34:40,781 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:34:40,782 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:34:40,809 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:34:40,809 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:34:40,809 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:34:40,811 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

439        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
21:35:02,414 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:35:02,415 |-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]
21:35:02,547 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:35:02,547 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:35:02,565 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:35:02,570 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:35:02,571 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:35:02,572 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:35:02,598 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:35:02,598 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:35:02,599 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:35:02,600 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

377        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
21:36:27,106 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:36:27,107 |-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]
21:36:27,253 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:36:27,253 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:36:27,266 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:36:27,271 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:36:27,271 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:36:27,272 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:36:27,315 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:36:27,315 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:36:27,315 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:36:27,317 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

372        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
21:41:12,255 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:41:12,256 |-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]
21:41:12,395 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:41:12,396 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:41:12,409 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:41:12,415 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:41:12,415 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:41:12,417 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:41:12,449 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:41:12,449 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:41:12,449 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:41:12,452 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

360        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
21:42:53,784 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:42:53,785 |-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]
21:42:53,935 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:42:53,936 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:42:53,950 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:42:53,956 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:42:53,956 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:42:53,958 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:42:53,985 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:42:53,985 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:42:53,986 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:42:53,987 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

358        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
21:43:57,330 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:43:57,331 |-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]
21:43:57,454 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:43:57,454 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:43:57,468 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:43:57,482 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:43:57,483 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:43:57,487 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:43:57,515 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:43:57,515 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:43:57,515 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:43:57,518 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

365        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
21:46:55,558 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:46:55,562 |-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]
21:46:55,695 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:46:55,695 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:46:55,708 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:46:55,716 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:46:55,717 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:46:55,718 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:46:55,746 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:46:55,746 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:46:55,746 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:46:55,748 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

382        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
21:48:51,131 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:48:51,132 |-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]
21:48:51,284 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:48:51,285 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:48:51,302 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:48:51,307 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:48:51,308 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:48:51,314 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:48:51,343 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:48:51,343 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:48:51,344 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:48:51,345 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

375        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
21:49:34,073 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:49:34,074 |-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]
21:49:34,201 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:49:34,202 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:49:34,217 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:49:34,223 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:49:34,224 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:49:34,225 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:49:34,255 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:49:34,256 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:49:34,256 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:49:34,258 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

359        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
21:50:13,183 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:50:13,184 |-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]
21:50:13,329 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:50:13,330 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:50:13,342 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:50:13,348 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:50:13,349 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:50:13,350 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:50:13,376 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:50:13,376 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:50:13,376 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:50:13,378 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

382        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
21:50:32,164 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:50:32,165 |-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]
21:50:32,291 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:50:32,292 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:50:32,309 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:50:32,315 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:50:32,315 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:50:32,316 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:50:32,343 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:50:32,343 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:50:32,343 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:50:32,345 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

360        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
21:50:53,478 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:50:53,479 |-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]
21:50:53,633 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:50:53,633 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:50:53,647 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:50:53,653 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:50:53,653 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:50:53,654 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:50:53,685 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:50:53,685 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:50:53,685 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:50:53,687 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

368        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
21:51:18,648 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:51:18,649 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
21:51:18,797 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:51:18,798 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:51:18,810 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:51:18,821 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:51:18,822 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:51:18,826 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:51:18,857 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:51:18,857 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:51:18,858 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:51:18,859 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

373        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test ArrayList_contains.key
Running test ArrayList_get.key
21:51:36,755 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:51:36,756 |-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]
21:51:36,936 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:51:36,936 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:51:36,950 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:51:36,956 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:51:36,956 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:51:36,958 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:51:36,985 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:51:36,985 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:51:36,986 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:51:36,988 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

377        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
21:51:55,935 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:51:55,936 |-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]
21:51:56,070 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:51:56,071 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:51:56,086 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:51:56,093 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:51:56,093 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:51:56,094 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:51:56,121 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:51:56,121 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:51:56,122 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:51:56,124 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

355        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
21:52:14,251 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:52:14,253 |-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]
21:52:14,385 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:52:14,385 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:52:14,401 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:52:14,407 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:52:14,407 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:52:14,408 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:52:14,435 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:52:14,435 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:52:14,436 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:52:14,438 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

352        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
21:52:30,945 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:52:30,946 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
21:52:31,085 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:52:31,086 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:52:31,099 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:52:31,105 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:52:31,105 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:52:31,107 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:52:31,134 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:52:31,134 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:52:31,134 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:52:31,136 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

350        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
21:52:49,121 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:52:49,122 |-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]
21:52:49,248 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:52:49,249 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:52:49,259 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:52:49,265 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:52:49,265 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:52:49,267 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:52:49,294 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:52:49,294 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:52:49,294 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:52:49,296 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

329        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
21:53:05,307 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:53:05,307 |-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]
21:53:05,453 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:53:05,453 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:53:05,465 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:53:05,474 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:53:05,475 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:53:05,476 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:53:05,502 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:53:05,502 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:53:05,503 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:53:05,505 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

378        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
21:53:24,302 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:53:24,305 |-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]
21:53:24,433 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:53:24,434 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:53:24,450 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:53:24,456 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:53:24,456 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:53:24,457 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:53:24,485 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:53:24,485 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:53:24,485 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:53:24,487 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

364        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
21:53:43,720 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:53:43,721 |-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]
21:53:43,862 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:53:43,863 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:53:43,878 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:53:43,883 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:53:43,884 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:53:43,885 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:53:43,913 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:53:43,914 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:53:43,914 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:53:43,916 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

366        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
21:59:17,641 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:59:17,642 |-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]
21:59:17,764 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:59:17,764 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:59:17,779 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:59:17,792 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:59:17,792 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:59:17,797 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:59:17,834 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:59:17,834 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:59:17,835 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:59:17,837 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

364        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
22:00:42,850 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:00:42,851 |-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]
22:00:43,002 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:00:43,003 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:00:43,017 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:00:43,024 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:00:43,025 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:00:43,026 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:00:43,055 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:00:43,055 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:00:43,056 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:00:43,059 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

365        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
22:01:42,320 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:01:42,321 |-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]
22:01:42,459 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:01:42,459 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:01:42,474 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:01:42,479 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:01:42,480 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:01:42,484 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:01:42,528 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:01:42,528 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:01:42,530 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:01:42,532 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - 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 list_seq
Running test observer
22:04:50,002 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:04:50,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]
22:04:50,156 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:04:50,157 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:04:50,170 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:04:50,175 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:04:50,175 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:04:50,177 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:04:50,205 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:04:50,206 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:04:50,206 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:04:50,208 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

380        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
22:06:57,427 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:06:57,428 |-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]
22:06:57,577 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:06:57,578 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:06:57,589 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:06:57,595 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:06:57,595 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:06:57,597 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:06:57,630 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:06:57,630 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:06:57,631 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:06:57,633 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

347        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
22:07:47,087 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:07:47,088 |-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]
22:07:47,220 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:07:47,221 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:07:47,239 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:07:47,248 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:07:47,248 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:07:47,251 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:07:47,277 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:07:47,277 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:07:47,278 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:07:47,280 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

374        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
22:09:34,300 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:09:34,301 |-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]
22:09:34,449 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:09:34,450 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:09:34,465 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:09:34,472 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:09:34,473 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:09:34,474 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:09:34,517 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:09:34,517 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:09:34,518 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:09:34,520 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

395        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
22:11:54,019 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:11:54,020 |-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]
22:11:54,157 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:11:54,159 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:11:54,172 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:11:54,178 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:11:54,179 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:11:54,180 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:11:54,209 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:11:54,209 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:11:54,210 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:11:54,212 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

367        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
22:15:25,518 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:15:25,521 |-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]
22:15:25,657 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:15:25,658 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:15:25,671 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:15:25,678 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:15:25,678 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:15:25,679 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:15:25,710 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:15:25,710 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:15:25,710 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:15:25,715 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

371        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
22:19:33,726 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:19:33,727 |-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]
22:19:33,874 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:19:33,875 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:19:33,891 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:19:33,898 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:19:33,898 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:19:33,900 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:19:33,941 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:19:33,941 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:19:33,942 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:19:33,944 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

390        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
22:21:13,860 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:21:13,861 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
22:21:13,996 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:21:13,997 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:21:14,011 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:21:14,023 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:21:14,024 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:21:14,025 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:21:14,055 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:21:14,055 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:21:14,055 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:21:14,058 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

368        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
22:25:03,087 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:25:03,098 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
22:25:03,239 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:25:03,239 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:25:03,263 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:25:03,269 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:25:03,269 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:25:03,270 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:25:03,295 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:25:03,296 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:25:03,296 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:25:03,299 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

373        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
22:25:40,775 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:25:40,776 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
22:25:40,926 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:25:40,926 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:25:40,939 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:25:40,945 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:25:40,945 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:25:40,947 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:25:40,974 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:25:40,974 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:25:40,975 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:25:40,977 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

393        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
22:36:22,992 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:36:22,997 |-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]
22:36:23,130 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:36:23,130 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:36:23,146 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:36:23,156 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:36:23,158 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:36:23,166 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:36:23,213 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:36:23,213 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:36:23,214 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:36:23,216 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

428        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
22:37:39,453 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:37:39,454 |-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]
22:37:39,577 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:37:39,577 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:37:39,591 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:37:39,597 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:37:39,597 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:37:39,598 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:37:39,625 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:37:39,625 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:37:39,626 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:37:39,628 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

375        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
64379      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 
64379      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 
64379      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 
68256      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 
68256      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 
68256      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 
78807      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 
78808      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 
78808      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 
82521      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 
82529      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 
82532      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 
111171     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 
111171     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 
111171     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 
114910     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 
114910     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 
114911     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 
118103     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 
118104     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 
118104     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 
121854     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 
121854     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 
121854     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 
170384     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 
170385     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 
170387     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 
174107     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 
174107     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 
174107     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 
191049     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 
191049     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 
191050     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 
194617     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 
194617     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 
194617     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 
515810     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 
515811     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 
515811     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 
525301     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 
525302     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 
525302     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 
529510     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 
529510     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 
529511     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 
535501     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 
535501     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 
535501     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 
710788     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 
710788     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 
710789     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 
715329     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 
715330     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 
715330     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 
718784     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 
718785     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 
723645     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 
723645     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 
727216     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 
727216     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 
731388     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 
731389     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 
734802     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 
734803     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 
738915     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 
738915     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 
742254     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 
742254     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 
746529     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 
746530     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 
749968     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 
749968     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 
754242     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 
754242     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 
757508     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 
757508     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 
776914     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 
776914     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 
783209     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 
783209     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 
787808     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 
787808     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 
798203     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 
802371     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
22:51:13,333 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:51:13,334 |-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]
22:51:13,473 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:51:13,473 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:51:13,485 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:51:13,491 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:51:13,491 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:51:13,493 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:51:13,533 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:51:13,533 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:51:13,533 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:51:13,535 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - 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 FOL
Running test strings
22:57:26,039 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:57:26,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]
22:57:26,200 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:57:26,201 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:57:26,220 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:57:26,231 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:57:26,232 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:57:26,236 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:57:26,265 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:57:26,265 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:57:26,265 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:57:26,267 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

391        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
23:00:42,965 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:00:42,966 |-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]
23:00:43,101 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:00:43,101 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:00:43,114 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:00:43,121 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:00:43,122 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:00:43,123 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:00:43,152 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:00:43,152 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:00:43,153 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:00:43,155 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

366        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
23:01:00,845 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:01:00,846 |-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]
23:01:00,987 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:01:00,987 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:01:01,006 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:01:01,014 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:01:01,015 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:01:01,019 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:01:01,053 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:01:01,053 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:01:01,054 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:01:01,056 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

384        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
23:05:00,702 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:05:00,703 |-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]
23:05:00,855 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:05:00,855 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:05:00,871 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:05:00,878 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:05:00,878 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:05:00,881 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:05:00,910 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:05:00,910 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:05:00,911 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:05:00,913 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

409        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
1078401    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
1078405    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
1078408    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
1078410    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
1078411    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter 
1078413    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
1078415    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
1078417    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
1078420    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
1078427    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
1078428    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
1078428    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
1078430    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
1078430    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
1078432    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
1078433    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1078434    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
1078435    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
1078436    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1078436    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1078437    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1078438    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
23:22:59,567 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:22:59,568 |-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]
23:22:59,703 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:22:59,704 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:22:59,720 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:22:59,726 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:22:59,729 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:22:59,734 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:22:59,767 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:22:59,767 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:22:59,768 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:22:59,770 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

368        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
23:24:05,696 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:24:05,698 |-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]
23:24:05,844 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:24:05,845 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:24:05,856 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:24:05,862 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:24:05,862 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:24:05,863 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:24:05,890 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:24:05,890 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:24:05,891 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:24:05,893 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

356        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
49251      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Class_invariant_axiom_for_DoubleLinkedList 
49982      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Class_invariant_axiom_for_DoubleLinkedList 
Returning from test reload_examples
Running test proofLoadRepair
23:25:00,433 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:25:00,434 |-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]
23:25:00,577 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:25:00,578 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:25:00,591 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:25:00,601 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:25:00,601 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:25:00,603 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:25:00,630 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:25:00,630 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:25:00,630 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:25:00,633 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

358        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
10430      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft 
10431      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right 
10435      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close 
13990      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
23:25:24,590 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:25:24,591 |-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]
23:25:24,710 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:25:24,710 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:25:24,722 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:25:24,728 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:25:24,728 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:25:24,729 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:25:24,774 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:25:24,774 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:25:24,775 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:25:24,776 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

371        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
23:26:46,701 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:26:46,702 |-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]
23:26:46,853 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
23:26:46,854 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:26:46,867 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
23:26:46,874 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
23:26:46,874 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
23:26:46,875 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:26:46,916 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
23:26:46,916 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
23:26:46,917 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
23:26:46,919 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

384        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.)
Feb 02, 2023 10:09:57 PM de.uka.ilkd.key.macros.scripts.ScriptCommand execute
INFO: Included script /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/sort.script
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
SMT Runtime, goal 17: 61 ms; valid
SMT Runtime, goal 28: 51 ms; valid