RunAllProofsFunctional

47

tests

0

failures

0

ignored

1h55m41.96s

duration

100%

successful

Tests

Test Method name Duration Result
project.key data()[10] 44.751s passed
project.key#1 data()[11] 18.349s passed
lcp.key data()[12] 20.965s passed
project.key#2 data()[13] 22.405s passed
ArrayList_contains.key data()[14] 16.786s passed
ArrayList_get.key data()[15] 19.025s passed
ArrayList_size.key data()[16] 17.697s passed
UpdateAbstraction_ex7_3_secure.key data()[17] 17.685s passed
UpdateAbstraction_ex7_4_secure.key data()[18] 17.455s passed
UpdateAbstraction_ex7_5_secure.key data()[19] 17.002s passed
newBook data()[1] 1m16.16s passed
UpdateAbstraction_ex7_6_secure.key data()[20] 17.078s passed
UpdateAbstraction_ex9_secure.key data()[21] 19.508s passed
list data()[22] 5m46.98s passed
list_ghost data()[23] 1m30.22s passed
list_recursive data()[24] 30.353s passed
list_seq data()[25] 3m16.06s passed
observer data()[26] 2m8.67s passed
removeDups data()[27] 49.094s passed
Saddleback_search.key data()[28] 1m48.60s passed
quicksort data()[29] 2m7.27s passed
oldBook data()[2] 23.118s passed
simpleTests data()[30] 3m24.64s passed
SmansEtAl data()[31] 4m2.10s passed
VACID0 data()[32] 1m38.76s passed
VSTTE10 data()[33] 3m44.77s passed
WeideEtAl data()[34] 39.355s passed
arithmetic data()[35] 10m46.60s passed
arrays data()[36] 1m14.22s passed
javadl data()[37] 12m49.69s passed
FOL data()[38] 6m9.77s passed
strings data()[39] 3m26.22s passed
comprehensions data()[3] 1m26.14s passed
simple_info_flow data()[40] 17.882s passed
modelMethods data()[41] 3m59.85s passed
permissionHeap data()[42] 18m21.01s passed
completionScopes data()[43] 1m9.33s passed
reload_examples data()[44] 54.297s passed
proofLoadRepair data()[45] 23.946s passed
switch data()[46] 1m24.79s passed
redux data()[47] 2m44.83s passed
performance data()[4] 4m55.27s passed
performancePOConstruction data()[5] 1m42.43s passed
applicationRestrictions data()[6] 1m6.93s passed
blockContracts data()[7] 2m55.31s passed
jmlAsserts data()[8] 1m58.59s passed
javaCard data()[9] 40.021s passed

Standard output

21:02:16,098 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:02:16,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]
21:02:16,183 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:02:16,184 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:02:16,190 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:02:16,195 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:02:16,195 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:02:16,196 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:02:16,215 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:02:16,215 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:02:16,216 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:02:16,216 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@4fc5e095 - Registering current configuration as safe fallback point

Running test newBook
21:02:16,614 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:02:16,615 |-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:02:16,770 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:02:16,770 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:02:16,783 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:02:16,788 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:02:16,788 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:02:16,790 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:02:16,818 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:02:16,818 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:02:16,819 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:02:16,821 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

356        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:03:32,796 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:03:32,797 |-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:03:32,935 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:03:32,936 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:03:32,953 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:03:32,959 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:03:32,959 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:03:32,964 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:03:32,997 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:03:32,997 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:03:32,997 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:03:32,999 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

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

427        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:05:21,987 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:05:21,988 |-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:05:22,124 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:05:22,125 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:05:22,137 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:05:22,142 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:05:22,143 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:05:22,144 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:05:22,173 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:05:22,173 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:05:22,174 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:05:22,176 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

351        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:10:17,259 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:10:17,260 |-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:10:17,387 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:10:17,387 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:10:17,404 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:10:17,409 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:10:17,410 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:10:17,411 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:10:17,448 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:10:17,448 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:10:17,448 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:10:17,450 |-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 performancePOConstruction
Running test applicationRestrictions
21:11:59,690 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:11:59,691 |-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:11:59,828 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:11:59,828 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:11:59,842 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:11:59,847 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:11:59,847 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:11:59,848 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:11:59,874 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:11:59,874 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:11:59,875 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:11:59,877 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

346        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:13:06,628 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:13:06,629 |-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:13:06,755 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:13:06,756 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:13:06,768 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:13:06,773 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:13:06,774 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:13:06,775 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:13:06,808 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:13:06,808 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:13:06,808 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:13:06,812 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

349        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:16:01,933 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:16:01,934 |-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:16:02,077 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:16:02,078 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:16:02,093 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:16:02,105 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:16:02,106 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:16:02,109 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:16:02,160 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:16:02,160 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:16:02,160 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:16:02,162 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

394        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:18:00,518 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:18:00,520 |-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:18:00,639 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:18:00,640 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:18:00,654 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:18:00,660 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:18:00,661 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:18:00,662 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:18:00,695 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:18:00,696 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:18:00,696 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:18:00,698 |-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 javaCard
Running test project.key
21:18:40,521 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:18:40,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]
21:18:40,652 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:18:40,653 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:18:40,671 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:18:40,677 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:18:40,677 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:18:40,679 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:18:40,708 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:18:40,708 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:18:40,709 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:18:40,711 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

369        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:19:25,285 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:19:25,286 |-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:19:25,421 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:19:25,422 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:19:25,438 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:19:25,449 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:19:25,450 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:19:25,454 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:19:25,497 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:19:25,498 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:19:25,498 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:19:25,500 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

381        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:19:43,639 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:19:43,640 |-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:19:43,790 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:19:43,791 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:19:43,811 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:19:43,821 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:19:43,821 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:19:43,822 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:19:43,867 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:19:43,867 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:19:43,869 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:19:43,871 |-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 lcp.key
Running test project.key#2
21:20:04,579 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:20:04,580 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
21:20:04,703 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:20:04,703 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:20:04,719 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:20:04,724 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:20:04,724 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:20:04,725 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:20:04,749 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:20:04,749 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:20:04,749 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:20:04,751 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

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

340        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:20:43,773 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:20:43,774 |-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:20:43,917 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:20:43,918 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:20:43,932 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:20:43,938 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:20:43,938 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:20:43,939 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:20:43,964 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:20:43,965 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:20:43,965 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:20:43,967 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

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

338        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:21:20,515 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:21:20,516 |-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:21:20,660 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:21:20,661 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:21:20,678 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:21:20,689 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:21:20,689 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:21:20,690 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:21:20,733 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:21:20,733 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:21:20,734 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:21:20,737 |-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 UpdateAbstraction_ex7_3_secure.key
Running test UpdateAbstraction_ex7_4_secure.key
21:21:38,196 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:21:38,197 |-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:21:38,328 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:21:38,329 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:21:38,347 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:21:38,363 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:21:38,364 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:21:38,365 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:21:38,402 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:21:38,402 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:21:38,402 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:21:38,404 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

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

423        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test UpdateAbstraction_ex7_5_secure.key
Running test UpdateAbstraction_ex7_6_secure.key
21:22:12,649 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:22:12,651 |-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:22:12,786 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:22:12,786 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:22:12,805 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:22:12,815 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:22:12,815 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:22:12,817 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:22:12,855 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:22:12,855 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:22:12,856 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:22:12,858 |-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 UpdateAbstraction_ex7_6_secure.key
Running test UpdateAbstraction_ex9_secure.key
21:22:29,729 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:22:29,730 |-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:22:29,863 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:22:29,864 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:22:29,876 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:22:29,882 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:22:29,882 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:22:29,884 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:22:29,920 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:22:29,920 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:22:29,923 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:22:29,925 |-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 UpdateAbstraction_ex9_secure.key
Running test list
21:22:49,254 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:22:49,255 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
21:22:49,405 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:22:49,406 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:22:49,428 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:22:49,433 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:22:49,434 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:22:49,435 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:22:49,464 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:22:49,464 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:22:49,464 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:22:49,467 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - 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 list
Running test list_ghost
21:28:36,222 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:28:36,223 |-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:28:36,383 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:28:36,384 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:28:36,401 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:28:36,411 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:28:36,412 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:28:36,415 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:28:36,444 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:28:36,444 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:28:36,444 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:28:36,446 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

394        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
21:30:06,432 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:30:06,433 |-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:30:06,574 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:30:06,575 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:30:06,592 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:30:06,598 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:30:06,598 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:30:06,599 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:30:06,626 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:30:06,626 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:30:06,626 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:30:06,630 |-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
21:30:36,802 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:30:36,803 |-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:30:36,937 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:30:36,938 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:30:36,957 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:30:36,963 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:30:36,963 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:30:36,965 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:30:36,991 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:30:36,991 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:30:36,992 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:30:36,995 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

404        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
21:33:52,847 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:33:52,848 |-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:52,974 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:33:52,975 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:33:52,989 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:33:52,994 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:33:52,994 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:33:53,000 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:33:53,045 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:33:53,045 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:33:53,046 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:33:53,048 |-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 observer
Running test removeDups
21:36:01,524 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:36:01,526 |-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:01,668 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:36:01,669 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:36:01,684 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:36:01,698 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:36:01,698 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:36:01,702 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:36:01,739 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:36:01,739 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:36:01,739 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:36:01,741 |-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 removeDups
Running test Saddleback_search.key
21:36:50,599 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:36:50,600 |-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:50,732 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:36:50,733 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:36:50,748 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:36:50,758 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:36:50,759 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:36:50,760 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:36:50,784 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:36:50,784 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:36:50,785 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:36:50,787 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

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

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

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

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

354        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
21:49:51,972 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:49:51,973 |-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:52,140 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:49:52,141 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:49:52,162 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:49:52,173 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:49:52,176 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:49:52,179 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:49:52,219 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:49:52,219 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:49:52,220 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:49:52,223 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

443        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
Returning from test VSTTE10
Running test WeideEtAl
21:53:36,733 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:53:36,734 |-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:36,871 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:53:36,871 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:53:36,893 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:53:36,899 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:53:36,899 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:53:36,900 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:53:36,925 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:53:36,925 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:53:36,926 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:53:36,928 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

357        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
21:54:16,109 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
21:54:16,110 |-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:54:16,261 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
21:54:16,261 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
21:54:16,282 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
21:54:16,293 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
21:54:16,294 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
21:54:16,298 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
21:54:16,328 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
21:54:16,328 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
21:54:16,329 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
21:54:16,331 |-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 arithmetic
Running test arrays
22:05:02,688 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:05:02,689 |-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:05:02,839 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:05:02,839 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:05:02,856 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:05:02,861 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:05:02,863 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:05:02,865 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:05:02,891 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:05:02,891 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:05:02,892 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:05:02,894 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

379        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:06:16,916 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:06:16,917 |-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:17,052 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:06:17,053 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:06:17,069 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:06:17,078 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:06:17,078 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:06:17,079 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:06:17,123 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:06:17,123 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:06:17,123 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:06:17,125 |-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. 
65401      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 
65401      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 
65401      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 
69225      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 
69225      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 
69226      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 
79702      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 
79703      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 
79703      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 
83489      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 
83489      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 
83489      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 
111794     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 
111794     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 
111794     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 
115465     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 
115465     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 
115465     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 
118728     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 
118729     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 
118729     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 
122537     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 
122537     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 
122538     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 
173597     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 
173597     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 
173597     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 
177451     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 
177452     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 
177452     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 
194643     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 
194644     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 
194644     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 
198291     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 
198292     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 
198293     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 
479760     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 
479760     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 
479760     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 
488976     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 
488980     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 
488981     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 
493259     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 
493260     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 
493261     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 
498824     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 
498825     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 
498825     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 
668314     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 
668314     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 
668314     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 
672632     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 
672632     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 
672632     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 
675820     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 
675820     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 
680615     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 
680616     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 
683865     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 
683866     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 
687774     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 
687774     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 
690885     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 
690886     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 
694787     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 
694787     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 
697910     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 
697911     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 
702019     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 
702020     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 
705266     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 
705267     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 
709588     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 
709588     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 
713119     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 
713119     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 
732471     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 
732472     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 
739032     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 
739033     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 
743732     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 
743732     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 
754037     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 
758128     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:19:06,635 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:19:06,636 |-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:06,762 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:19:06,763 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:19:06,775 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:19:06,780 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:19:06,781 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:19:06,782 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:19:06,809 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:19:06,809 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:19:06,809 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:19:06,811 |-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 FOL
Running test strings
22:25:16,397 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:25:16,398 |-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:16,542 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:25:16,542 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:25:16,559 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:25:16,569 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:25:16,569 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:25:16,571 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:25:16,604 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:25:16,604 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:25:16,605 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:25:16,607 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

427        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
22:28:42,594 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:28:42,595 |-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:28:42,743 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:28:42,743 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:28:42,756 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:28:42,761 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:28:42,761 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:28:42,763 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:28:42,800 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:28:42,800 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:28:42,800 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:28:42,802 |-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
22:29:00,483 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:29:00,491 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
22:29:00,641 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:29:00,641 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:29:00,656 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:29:00,663 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:29:00,664 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:29:00,667 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:29:00,704 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:29:00,704 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:29:00,704 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:29:00,706 |-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 modelMethods
Running test permissionHeap
22:33:00,333 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:33:00,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:33:00,486 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:33:00,487 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:33:00,504 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:33:00,510 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:33:00,510 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:33:00,512 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:33:00,549 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:33:00,549 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:33:00,549 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:33:00,552 |-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. 
1100475    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
1100478    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter 
1100484    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
1100485    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
1100486    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter 
1100488    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
1100491    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
1100493    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter 
1100495    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter 
1100497    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
1100499    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter 
1100500    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
1100501    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter 
1100502    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
1100503    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler 
1100504    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1100505    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter 
1100506    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter 
1100508    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1100509    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1100510    WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler 
1100510    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
22:51:21,325 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:51:21,326 |-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:21,454 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:51:21,454 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:51:21,473 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:51:21,483 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:51:21,483 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:51:21,485 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:51:21,512 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:51:21,512 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:51:21,513 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:51:21,515 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

357        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
22:52:30,660 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:52:30,661 |-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:52:30,812 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:52:30,813 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:52:30,834 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:52:30,840 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:52:30,840 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:52:30,841 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:52:30,869 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:52:30,870 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:52:30,870 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:52:30,872 |-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 reload_examples
Running test proofLoadRepair
22:53:24,950 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:53:24,951 |-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:53:25,084 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:53:25,085 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:53:25,097 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:53:25,103 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:53:25,103 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:53:25,105 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:53:25,132 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:53:25,132 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:53:25,133 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:53:25,135 |-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. 
10317      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft 
10319      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right 
10327      WARN  main            d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close 
14018      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
22:53:48,907 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:53:48,908 |-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:53:49,037 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:53:49,038 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:53:49,049 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:53:49,054 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:53:49,054 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:53:49,055 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:53:49,082 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:53:49,082 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:53:49,083 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:53:49,085 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2f177a4b - Registering current configuration as safe fallback point

330        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
22:55:13,700 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
22:55:13,701 |-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:55:13,830 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - debug attribute not set
22:55:13,831 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
22:55:13,844 |-INFO in ch.qos.logback.core.joran.action.AppenderAction - Naming appender as [STDOUT]
22:55:13,849 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@3:15 - no applicable action for [file], current ElementPath  is [[configuration][appender][file]]
22:55:13,850 |-ERROR in ch.qos.logback.core.joran.spi.Interpreter@4:17 - no applicable action for [append], current ElementPath  is [[configuration][appender][append]]
22:55:13,851 |-INFO in ch.qos.logback.core.joran.action.NestedComplexPropertyIA - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
22:55:13,878 |-INFO in ch.qos.logback.classic.joran.action.RootLoggerAction - Setting level of ROOT logger to WARN
22:55:13,878 |-INFO in ch.qos.logback.core.joran.action.AppenderRefAction - Attaching appender named [STDOUT] to Logger[ROOT]
22:55:13,878 |-INFO in ch.qos.logback.classic.joran.action.ConfigurationAction - End of configuration.
22:55:13,883 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@29176cc1 - Registering current configuration as safe fallback point

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

Standard error

Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Timeout watcher launched (2000 secs.)
Mar 03, 2023 9:38:59 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: 91 ms; valid
SMT Runtime, goal 27: 42 ms; valid