RunAllProofsInfFlow

29

tests

0

failures

0

ignored

58m25.36s

duration

100%

successful

Tests

Test Method name Duration Result
SimpleEvoting data()[10] 3m32.09s passed
ToyVoting_nomacro data()[11] 45.502s passed
ConditionalConfidential_nomacro data()[12] 0.001s passed
SumExample_nomacro data()[13] 14.793s passed
ToyBanking_nomacro data()[14] 1m44.78s passed
BlockContracts_nomacro data()[15] 1m41.17s passed
MethodContracts_nomacro data()[16] 1m35.16s passed
LoopInvariants_nomacro data()[17] 2m21.58s passed
MiniExamples_nomacro data()[18] 2m3.70s passed
NewObjects_nomacro data()[19] 2m48.35s passed
ToyVoting data()[1] 32.646s passed
SimpleEvoting_nomacro data()[20] 2m50.17s passed
ToyVoting_fullmacro data()[21] 1m16.12s passed
SumExample_fullmacro data()[22] 14.364s passed
ToyBanking_fullmacro data()[23] 5m27.56s passed
BlockContracts_fullmacro data()[24] 1m46.88s passed
MethodContracts_fullmacro data()[25] 1m33.20s passed
InformationFlow_fullmacro data()[26] 7m1.13s passed
MiniExamples_fullmacro data()[27] 2m8.01s passed
NewObjects_fullmacro data()[28] 3m56.71s passed
SimpleEvoting_fullmacro data()[29] 3m55.26s passed
ConditionalConfidential data()[2] 18.014s passed
SumExample data()[3] 12.360s passed
ToyBanking data()[4] 2m28.76s passed
BlockContracts data()[5] 1m17.10s passed
MethodContracts data()[6] 1m29.60s passed
LoopInvariants data()[7] 1m29.02s passed
MiniExamples data()[8] 1m58.19s passed
NewObjects data()[9] 1m43.17s passed

Standard output

597        INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting 
398        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
427        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)

475        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).JML normal_behavior operation contract.0.key 
12386      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
12553      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).JML normal_behavior operation contract.0.key 
16593      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16740      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__isValid(int)).JML normal_behavior operation contract.0.key 
20292      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
20450      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).JML normal_behavior operation contract.0.key 
23984      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
24139      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__inputVote()).JML normal_behavior operation contract.0.key 
27575      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
27731      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__secure_voting()).JML normal_behavior operation contract.0.key 
32068      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
33234      INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting 
33242      INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential 
414        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
434        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
466        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ConditionalConfidential/CCExample(CCExample__hasAccessRight(CCExample.User)).JML normal_behavior operation contract.0.key 
12966      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
13171      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ConditionalConfidential/CCExample(CCExample__getConfidentialData(CCExample.User)).JML normal_behavior operation contract.0.key 
17619      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
51254      INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential 
51256      INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample 
446        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
466        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
514        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/Sum/SumExample(SumExample__getSum()).JML normal_behavior operation contract.0.key 
11973      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
63615      INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample 
63617      INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking 
454        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
487        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
535        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key 
13465      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
13644      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key 
47713      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
47999      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key 
58995      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
59251      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key 
63321      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
63519      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).JML normal_behavior operation contract.0.key 
67249      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
67430      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).JML normal_behavior operation contract.0.key 
71194      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
71371      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).JML normal_behavior operation contract.0.key 
83670      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
83921      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key 
87909      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
88171      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key 
119229     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
119544     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key 
129126     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
129389     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key 
133192     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
133414     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).JML normal_behavior operation contract.0.key 
136920     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
137128     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).JML normal_behavior operation contract.0.key 
140623     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
140827     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.Bank(banking_example2.Bank__login(int,(C)).JML normal_behavior operation contract.0.key 
148255     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
212380     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking 
212384     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts 
477        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
506        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
544        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).JML operation contract.0.key 
12071      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
12232      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).JML operation contract.0.key 
16302      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16462      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).JML operation contract.0.key 
20621      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
20809      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).JML operation contract.0.key 
24775      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
24961      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).JML operation contract.0.key 
28836      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
29037      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).JML operation contract.0.key 
33144      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
33353      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).JML operation contract.0.key 
37413      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
37630      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).JML operation contract.0.key 
41597      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
41812      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).JML operation contract.0.key 
45608      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
45824      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).JML operation contract.0.key 
49523      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
49722      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).JML operation contract.0.key 
53262      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
53464      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).JML operation contract.0.key 
57007      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
57211      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).JML operation contract.0.key 
60725      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
60939      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).JML operation contract.0.key 
64469      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
64736      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).JML operation contract.0.key 
68245      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
68447      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).JML operation contract.0.key 
72544      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
72801      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).JML operation contract.0.key 
76650      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
289482     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts 
289484     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts 
503        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
537        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
591        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).JML normal_behavior operation contract.0.key 
11838      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
11994      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).JML normal_behavior operation contract.0.key 
16266      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16421      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).JML operation contract.0.key 
20229      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
20400      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).JML normal_behavior operation contract.0.key 
23994      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
24155      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).JML operation contract.0.key 
27685      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
27841      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param_helper()).JML normal_behavior operation contract.0.key 
31279      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
31440      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).JML operation contract.0.key 
34942      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
35107      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n9()).JML normal_behavior operation contract.0.key 
38640      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
38818      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).JML operation contract.0.key 
42338      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
42548      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).JML operation contract.0.key 
46078      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
46265      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).JML normal_behavior operation contract.0.key 
49660      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
49840      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).JML operation contract.0.key 
53416      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
53673      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).JML operation contract.0.key 
57130      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
57398      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).JML operation contract.0.key 
60742      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
60934      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).JML normal_behavior operation contract.0.key 
64310      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
64513      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).JML normal_behavior operation contract.0.key 
67849      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
68062      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).JML operation contract.0.key 
71382      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
71589      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).JML operation contract.0.key 
74858      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
75074      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).JML operation contract.0.key 
78472      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
78688      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).JML normal_behavior operation contract.0.key 
81988      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
82251      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).JML normal_behavior operation contract.0.key 
85514      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
85725      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).JML operation contract.0.key 
89082      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
379078     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts 
379083     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants 
429        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
458        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
517        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key 
12885      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
13080      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).JML operation contract.0.key 
18157      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
18308      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).JML operation contract.0.key 
22907      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
23078      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).JML operation contract.0.key 
28525      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
28722      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).JML operation contract.0.key 
33946      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
34145      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).JML operation contract.0.key 
39115      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
39332      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).JML operation contract.0.key 
44441      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
44638      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).JML operation contract.0.key 
49103      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
49293      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).JML operation contract.0.key 
53417      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
53641      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).JML operation contract.0.key 
57803      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
57997      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).JML operation contract.0.key 
62438      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
62640      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).JML operation contract.0.key 
66931      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
67169      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).JML operation contract.0.key 
71423      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
71626      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).JML operation contract.0.key 
75745      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
75956      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).JML operation contract.0.key 
80100      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
80301      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).JML normal_behavior operation contract.0.key 
84185      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
84389      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).JML normal_behavior operation contract.0.key 
88581      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
468101     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants 
468103     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples 
438        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
456        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
503        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key 
11660      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
11793      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key 
15975      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16127      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).JML normal_behavior operation contract.0.key 
19869      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
20015      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).JML normal_behavior operation contract.0.key 
23642      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
23794      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).JML normal_behavior operation contract.0.key 
27318      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
27487      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).JML normal_behavior operation contract.0.key 
31094      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
31297      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).JML normal_behavior operation contract.0.key 
34869      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
35038      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).JML normal_behavior operation contract.0.key 
38522      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
38715      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.1.key 
42235      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
42445      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.0.key 
45946      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
46130      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).JML normal_behavior operation contract.0.key 
49684      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
49887      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).JML operation contract.0.key 
53342      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
53532      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).JML normal_behavior operation contract.0.key 
56927      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
57129      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).JML normal_behavior operation contract.0.key 
60509      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
60709      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).JML normal_behavior operation contract.0.key 
64095      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
64298      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).JML normal_behavior operation contract.0.key 
67698      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
67917      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).JML normal_behavior operation contract.0.key 
71262      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
71476      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).JML normal_behavior operation contract.0.key 
74789      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
75020      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).JML normal_behavior operation contract.0.key 
78348      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
78555      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).JML normal_behavior operation contract.0.key 
81877      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
82092      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).JML normal_behavior operation contract.0.key 
85390      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
85608      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).JML normal_behavior operation contract.0.key 
88934      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
89162      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).JML normal_behavior operation contract.0.key 
92590      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
92833      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).JML normal_behavior operation contract.0.key 
96092      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
96347      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).JML normal_behavior operation contract.0.key 
99665      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
99900      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).JML normal_behavior operation contract.0.key 
103232     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
103571     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.1.key 
106964     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
107221     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.0.key 
110563     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
110823     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).JML normal_behavior operation contract.0.key 
114115     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
114373     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).JML normal_behavior operation contract.0.key 
117715     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
586290     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples 
586293     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects 
499        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
521        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
550        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).JML operation contract.0.key 
12283      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
12442      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).JML normal_behavior operation contract.0.key 
17336      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
17508      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.1.key 
21699      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
21877      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.0.key 
25993      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
26169      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).JML normal_behavior operation contract.0.key 
29986      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
30195      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).JML operation contract.0.key 
35864      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
36088      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).JML operation contract.0.key 
40375      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
40683      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).JML operation contract.0.key 
44540      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
44737      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.1.key 
49496      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
49702      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.0.key 
54384      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
54612      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).JML operation contract.0.key 
59070      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
59293      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).JML operation contract.0.key 
63665      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
63895      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).JML normal_behavior operation contract.0.key 
67921      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
68154      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.1.key 
71739      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
71946      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.0.key 
75510      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
75715      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).JML operation contract.0.key 
79497      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
79731      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).JML operation contract.0.key 
83435      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
83722      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).JML operation contract.0.key 
87391      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
87620      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML accessible clause.0.key 
91163      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
91389      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML normal_behavior operation contract.0.key 
94897      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
95127      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).JML normal_behavior operation contract.0.key 
98955      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
99293      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/PasswordFile/passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key 
102685     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
689456     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects 
689459     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting 
453        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
478        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
534        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).JML normal_behavior operation contract.0.key 
14170      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
14357      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage((B)).JML normal_behavior operation contract.0.key 
19734      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
19904      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).JML normal_behavior operation contract.0.key 
26111      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
26338      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).JML normal_behavior operation contract.0.key 
30728      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
30958      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).JML normal_behavior operation contract.0.key 
35292      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
35478      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).JML normal_behavior operation contract.0.key 
39831      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
40008      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment___rep()).JML accessible clause.0.key 
44321      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
44558      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.1.key 
60867      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
61156      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.0.key 
76200      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
76476      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Message(java.lang.Object___inv_()).JML accessible clause.0.key 
80853      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
81055      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML accessible clause.0.key 
87051      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
87306      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML normal_behavior operation contract.0.key 
92140      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
92404      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onSendResult()).JML normal_behavior operation contract.0.key 
96789      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
97006      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.1.key 
101414     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
101629     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.0.key 
106470     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
106727     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(java.lang.Object___inv_()).JML accessible clause.0.key 
110990     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
111225     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key 
115649     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
115896     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key 
120219     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
120465     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__publishResult()).JML normal_behavior operation contract.0.key 
125307     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
125554     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).JML normal_behavior operation contract.0.key 
174415     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
174790     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Setup(java.lang.Object___inv_()).JML accessible clause.0.key 
183650     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
184074     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.1.key 
193394     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
193716     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.0.key 
207040     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
207394     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(java.lang.Object___inv_()).JML accessible clause.0.key 
211614     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
901550     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting 
901553     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro 
498        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
518        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
569        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.key 
28989      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
29243      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.key 
33311      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
33584      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.key 
37546      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
37755      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.key 
41447      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
41665      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.key 
45128      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
947054     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro 
947056     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro 
947056     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro 
947057     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro 
489        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
506        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
548        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.key 
14358      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
961849     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro 
961851     INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro 
431        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
468        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
511        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.key 
15461      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
15685      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.key 
21253      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
21460      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.key 
25850      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
26035      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.key 
30149      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
30377      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.key 
85286      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
85625      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.key 
91417      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
91785      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.key 
96372      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
96568      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.key 
100401     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
100604     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.key 
104342     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1066627    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro 
1066631    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro 
404        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
437        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
492        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.key 
13650      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
13819      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.key 
18675      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
18863      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.key 
24534      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
24762      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.key 
29871      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
30123      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.key 
35593      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
35843      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.key 
42025      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
42325      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.key 
48547      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
48842      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.key 
54541      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
54846      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.key 
60948      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
61325      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.key 
65449      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
65728      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.key 
69645      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
69936      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.key 
73946      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
74163      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.key 
78211      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
78448      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.key 
82499      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
82833      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.key 
86948      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
87216      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.key 
93982      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
94291      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.key 
100645     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1167795    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro 
1167797    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro 
514        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
540        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
567        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.key 
16290      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16528      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.key 
21122      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
21362      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.key 
25556      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
25758      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.key 
29519      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
29691      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.key 
33356      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
33559      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.key 
38380      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
38563      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.key 
42331      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
42517      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.key 
47027      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
47241      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.key 
50921      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
51118      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.key 
56029      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
56248      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.key 
60453      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
60655      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.key 
64277      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
64500      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.key 
68052      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
68326      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.key 
71810      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
72049      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.key 
75789      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
76003      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.key 
79631      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
79878      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.key 
83477      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
83693      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.key 
87232      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
87453      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.key 
90843      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
91137      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.key 
94684      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1262952    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro 
1262953    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro 
420        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
446        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
486        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.key 
15570      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
15765      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.key 
21965      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
22202      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.key 
28228      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
28428      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.key 
44015      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
44316      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.key 
58108      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
58513      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.key 
71811      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
72221      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.key 
82963      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
83253      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.key 
90921      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
91187      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.key 
96305      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
96548      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.key 
100669     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
100902     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.key 
107149     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
107418     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.key 
114046     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
114384     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.key 
120365     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
120696     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.key 
125772     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
126013     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.key 
130919     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
131147     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.key 
134811     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
135027     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.key 
141097     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1404529    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro 
1404531    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro 
487        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
514        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
543        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key 
12378      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
12556      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key 
16749      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16896      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.key 
20604      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
20819      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.key 
24523      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
24685      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.key 
28280      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
28445      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.key 
32249      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
32541      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.key 
36151      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
36344      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.key 
39950      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
40140      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.key 
44642      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
44850      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.key 
50462      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
50677      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.key 
54337      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
54561      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.key 
57946      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
58135      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.key 
61612      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
61814      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.key 
65281      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
65503      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.key 
68852      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
69069      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.key 
72487      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
72704      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.key 
76119      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
76334      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.key 
79715      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
79960      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.key 
83217      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
83435      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.key 
86730      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
86973      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.key 
90213      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
90439      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.key 
93809      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
94069      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.key 
97696      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
97942      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.key 
101353     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
101607     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.key 
104963     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
105225     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.key 
108702     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
109026     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.key 
112381     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
112654     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.key 
115926     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
116194     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.key 
119604     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
119944     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.key 
123164     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
1528226    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro 
1528229    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro 
402        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
419        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
451        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.key 
12081      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
12269      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.key 
18052      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
18249      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.key 
22927      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
23097      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.key 
27388      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
27567      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.key 
31493      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
31662      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.key 
48104      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
48375      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.key 
52791      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
52999      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.key 
80158      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
80429      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.key 
106607     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
106973     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.key 
126339     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
126686     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.key 
140741     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
141015     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.key 
144786     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
145019     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.key 
149202     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
149427     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.key 
153313     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
153535     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.key 
158051     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
158277     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.key 
161942     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
162237     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.key 
167833     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1696576    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro 
1696579    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro 
421        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
439        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
467        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.key 
22359      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
22603      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.key 
27371      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
27582      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.key 
32244      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
32418      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.key 
36979      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
37180      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.key 
77091      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
77425      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.key 
124325     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
124647     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.key 
132475     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
132723     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.key 
149355     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
149642     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.key 
169680     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1866750    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro 
1866751    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro 
463        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
484        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
541        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.m.key 
44939      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
45210      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.m.key 
49286      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
49580      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.m.key 
53558      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
53720      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.m.key 
57555      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
57723      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.m.key 
61304      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
61488      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__secure_voting()).Non-interference contract.0.m.key 
75620      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1942869    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro 
1942870    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro 
457        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
496        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
558        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.m.key 
13982      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
1957232    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro 
1957233    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro 
429        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
451        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
488        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key 
16638      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16952      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key 
89480      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
89931      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.m.key 
94102      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
94414      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.m.key 
98133      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
98411      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.m.key 
102048     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
102248     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.m.key 
289918     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
290388     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key 
296037     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
296564     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key 
315352     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
315692     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.m.key 
319601     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
319951     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.m.key 
323463     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
323692     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.m.key 
327115     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
2284788    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro 
2284792    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_fullmacro 
500        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
528        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
565        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.m.key 
11962      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
12126      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.m.key 
16886      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
17069      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.m.key 
22990      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
23202      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.m.key 
28483      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
28744      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.m.key 
34135      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
34387      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.m.key 
40060      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
40365      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.m.key 
53620      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
53979      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.m.key 
59020      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
59397      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.m.key 
64811      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
65111      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.m.key 
69215      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
69518      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.m.key 
73578      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
73864      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.m.key 
77836      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
78130      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.m.key 
82378      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
82687      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.m.key 
86635      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
86917      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.m.key 
91040      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
91310      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.m.key 
100604     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
100921     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.m.key 
106375     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
2391672    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro 
2391674    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro 
527        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
555        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
590        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.m.key 
16621      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
16833      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.m.key 
21511      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
21724      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.m.key 
25822      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
26012      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.m.key 
29780      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
29964      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.m.key 
33736      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
33931      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.m.key 
39656      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
39868      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.m.key 
43565      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
43758      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.m.key 
47938      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
48136      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.m.key 
51445      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
51672      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.m.key 
55968      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
56211      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.m.key 
60143      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
60423      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.m.key 
63891      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
64118      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.m.key 
67425      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
67647      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.m.key 
70901      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
71118      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.m.key 
74683      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
74944      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.m.key 
78508      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
78743      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.m.key 
82200      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
82438      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.m.key 
85643      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
85876      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.m.key 
89121      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
89339      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.m.key 
92739      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
2484868    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro 
2484869    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro 
430        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
451        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
498        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.m.key 
18196      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
18431      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.m.key 
24230      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
24475      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.m.key 
29818      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
30056      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.m.key 
330512     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
330859     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.m.key 
341241     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
341631     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.m.key 
351333     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
351679     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.m.key 
360322     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
360633     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.m.key 
367679     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
368018     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.m.key 
375379     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
375655     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.m.key 
381592     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
381913     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.m.key 
387917     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
388232     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.m.key 
395050     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
395365     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.m.key 
401025     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
401356     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.m.key 
406283     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
406539     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.m.key 
411117     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
411377     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.m.key 
415103     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
415336     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.m.key 
420611     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
2906002    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro 
2906003    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro 
494        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
510        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
546        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key 
12842      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
13003      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key 
17307      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
17503      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.m.key 
21333      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
21505      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.m.key 
25303      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
25514      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.m.key 
29134      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
29324      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.m.key 
33159      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
33358      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.m.key 
36980      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
37176      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.m.key 
40721      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
40914      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.m.key 
45156      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
45372      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.m.key 
51512      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
51741      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.m.key 
55515      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
55765      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.m.key 
59394      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
59625      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.m.key 
63379      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
63756      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.m.key 
67476      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
67715      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.m.key 
71192      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
71426      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.m.key 
75022      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
75277      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.m.key 
78818      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
79053      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.m.key 
82461      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
82704      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.m.key 
86210      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
86457      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.m.key 
89903      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
90151      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.m.key 
93540      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
93846      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.m.key 
97249      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
97529      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.m.key 
101094     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
101385     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.m.key 
104945     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
105209     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.m.key 
108626     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
108895     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.m.key 
112460     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
112740     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.m.key 
116151     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
116432     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.m.key 
119956     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
120232     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.m.key 
123777     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
124080     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.m.key 
127489     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
3034013    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro 
3034014    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro 
447        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
477        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
517        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.m.key 
12301      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
12461      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.m.key 
18030      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
18215      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.m.key 
22737      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
22958      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.m.key 
27172      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
27375      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.m.key 
31112      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
31288      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).Non-interference contract.0.m.key 
49220      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
49524      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.m.key 
60908      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
61248      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.m.key 
65289      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
65500      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.m.key 
105127     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
105444     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.0.m.key 
123673     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
124062     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).Non-interference contract.0.m.key 
141859     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
142187     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.m.key 
180586     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
180943     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.m.key 
196248     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
196607     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.m.key 
210367     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
210644     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.m.key 
214321     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
214592     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.m.key 
218524     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
218784     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.m.key 
222442     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
222712     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.m.key 
226589     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
226843     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.m.key 
230368     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
230618     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.m.key 
236193     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
3270720    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro 
3270722    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro 
465        INFO  Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.) 
500        WARN  main            d.u.i.k.s.ProofSettings   The settings in /home/runner/.key/proof-settings.props are *not* read. 
550        INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.m.key 
19610      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
19862      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).Non-interference contract.0.m.key 
27936      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
28178      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.m.key 
32667      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
32897      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.m.key 
37397      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
37577      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.m.key 
41910      INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: open goal(s) 
42113      INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.m.key 
102670     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
103118     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.m.key 
167362     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
167790     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).Non-interference contract.0.m.key 
173777     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
174152     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.m.key 
179536     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
179793     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.m.key 
205731     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
206104     INFO  main            d.u.i.k.p.r.p.TestFile    Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.m.key 
234603     INFO  main            d.u.i.k.p.r.p.TestFile    ... finished proof: closed. 
3505976    INFO  Test worker     d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro