464 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting
455 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
482 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)
490 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).JML normal_behavior operation contract.0.key
10788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10932 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).JML normal_behavior operation contract.0.key
14661 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14780 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__isValid(int)).JML normal_behavior operation contract.0.key
18386 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18527 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).JML normal_behavior operation contract.0.key
21881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22079 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__inputVote()).JML normal_behavior operation contract.0.key
25303 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25452 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__secure_voting()).JML normal_behavior operation contract.0.key
29760 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30745 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting
30754 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential
430 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
449 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
453 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ConditionalConfidential/CCExample(CCExample__hasAccessRight(CCExample.User)).JML normal_behavior operation contract.0.key
12275 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12457 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ConditionalConfidential/CCExample(CCExample__getConfidentialData(CCExample.User)).JML normal_behavior operation contract.0.key
16381 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47477 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential
47479 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample
373 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
393 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
401 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/Sum/SumExample(SumExample__getSum()).JML normal_behavior operation contract.0.key
10806 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58622 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample
58625 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking
421 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
432 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
441 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key
11616 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11837 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key
43701 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43971 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key
54268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54470 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key
58331 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58519 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).JML normal_behavior operation contract.0.key
62082 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62241 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).JML normal_behavior operation contract.0.key
65794 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65957 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).JML normal_behavior operation contract.0.key
76798 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77024 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key
80807 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80993 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key
109722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110015 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key
118887 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
119114 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key
122732 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122970 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).JML normal_behavior operation contract.0.key
126329 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126509 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).JML normal_behavior operation contract.0.key
129835 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130017 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.Bank(banking_example2.Bank__login(int,(C)).JML normal_behavior operation contract.0.key
136835 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
195885 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking
195891 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts
503 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
533 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/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).JML operation contract.0.key
11157 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11297 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).JML operation contract.0.key
15339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15501 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).JML operation contract.0.key
19633 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19799 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).JML operation contract.0.key
23567 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23726 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).JML operation contract.0.key
27594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27758 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).JML operation contract.0.key
31764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32016 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).JML operation contract.0.key
35880 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36069 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).JML operation contract.0.key
39893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40083 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).JML operation contract.0.key
43851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44044 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).JML operation contract.0.key
47682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47889 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).JML operation contract.0.key
51477 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51660 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).JML operation contract.0.key
55183 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55365 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).JML operation contract.0.key
58977 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59159 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).JML operation contract.0.key
62679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62887 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).JML operation contract.0.key
66458 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66648 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).JML operation contract.0.key
70824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71034 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).JML operation contract.0.key
74880 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
271307 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts
271316 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts
462 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.
481 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).JML normal_behavior operation contract.0.key
11178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11341 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).JML normal_behavior operation contract.0.key
15469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15608 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).JML operation contract.0.key
19251 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19397 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).JML normal_behavior operation contract.0.key
22897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23041 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).JML operation contract.0.key
26506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26649 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param_helper()).JML normal_behavior operation contract.0.key
30083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30298 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).JML operation contract.0.key
33743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33901 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n9()).JML normal_behavior operation contract.0.key
37284 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37449 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).JML operation contract.0.key
40801 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40999 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).JML operation contract.0.key
44472 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44643 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).JML normal_behavior operation contract.0.key
48015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48180 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).JML operation contract.0.key
51740 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51929 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).JML operation contract.0.key
55363 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55535 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).JML operation contract.0.key
58937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59117 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).JML normal_behavior operation contract.0.key
62480 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62668 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).JML normal_behavior operation contract.0.key
65969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66151 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).JML operation contract.0.key
69472 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69738 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).JML operation contract.0.key
73015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73283 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).JML operation contract.0.key
76556 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76796 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).JML normal_behavior operation contract.0.key
80066 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80286 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).JML normal_behavior operation contract.0.key
83592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83794 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).JML operation contract.0.key
87061 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
358771 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts
358776 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants
464 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.
485 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key
11536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11676 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).JML operation contract.0.key
16164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16309 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).JML operation contract.0.key
20575 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20739 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).JML operation contract.0.key
25627 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25800 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).JML operation contract.0.key
30463 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30649 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).JML operation contract.0.key
35263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35449 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).JML operation contract.0.key
39965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40135 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).JML operation contract.0.key
44089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44365 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).JML operation contract.0.key
48111 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48297 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).JML operation contract.0.key
52091 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
52298 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).JML operation contract.0.key
56222 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56418 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).JML operation contract.0.key
60320 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60561 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).JML operation contract.0.key
64505 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64691 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).JML operation contract.0.key
68436 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68679 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).JML operation contract.0.key
72410 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72608 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).JML normal_behavior operation contract.0.key
76087 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76271 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).JML normal_behavior operation contract.0.key
80083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
439267 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants
439268 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples
441 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
480 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
487 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
10791 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10920 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
14768 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14905 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).JML normal_behavior operation contract.0.key
18510 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18646 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).JML normal_behavior operation contract.0.key
22139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22282 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).JML normal_behavior operation contract.0.key
25713 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25862 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).JML normal_behavior operation contract.0.key
29279 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29435 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).JML normal_behavior operation contract.0.key
32833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33005 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).JML normal_behavior operation contract.0.key
36481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36665 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.1.key
40131 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40293 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.0.key
43727 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43896 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).JML normal_behavior operation contract.0.key
47361 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47566 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).JML operation contract.0.key
50859 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51058 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).JML normal_behavior operation contract.0.key
54499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54683 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).JML normal_behavior operation contract.0.key
58041 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58218 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).JML normal_behavior operation contract.0.key
61485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61663 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).JML normal_behavior operation contract.0.key
64958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65145 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).JML normal_behavior operation contract.0.key
68413 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68605 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).JML normal_behavior operation contract.0.key
71869 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72065 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).JML normal_behavior operation contract.0.key
75302 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75499 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).JML normal_behavior operation contract.0.key
78766 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78962 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).JML normal_behavior operation contract.0.key
82198 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82399 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).JML normal_behavior operation contract.0.key
85650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85857 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).JML normal_behavior operation contract.0.key
89209 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89422 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).JML normal_behavior operation contract.0.key
92649 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92869 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).JML normal_behavior operation contract.0.key
96109 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96325 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).JML normal_behavior operation contract.0.key
99700 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99946 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.1.key
103160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103394 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.0.key
106614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106842 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).JML normal_behavior operation contract.0.key
110086 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110315 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).JML normal_behavior operation contract.0.key
113560 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
553259 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples
553262 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects
439 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
454 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
462 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).JML operation contract.0.key
10976 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11116 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).JML normal_behavior operation contract.0.key
15582 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15738 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.1.key
19716 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19867 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.0.key
23662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23816 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).JML normal_behavior operation contract.0.key
27482 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27637 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).JML operation contract.0.key
33020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33224 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).JML operation contract.0.key
37399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37621 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).JML operation contract.0.key
41228 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41394 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.1.key
46042 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46326 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.0.key
50907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51154 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).JML operation contract.0.key
55568 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55781 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).JML operation contract.0.key
59915 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60195 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).JML normal_behavior operation contract.0.key
64052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64252 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.1.key
67727 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67913 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.0.key
71423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71621 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).JML operation contract.0.key
75227 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75428 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).JML operation contract.0.key
78971 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79205 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).JML operation contract.0.key
82787 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82997 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML accessible clause.0.key
86451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86650 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML normal_behavior operation contract.0.key
90102 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90317 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).JML normal_behavior operation contract.0.key
93989 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
647776 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects
647780 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
424 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
424 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
432 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/PasswordFile/passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
11297 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
659391 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
659393 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting
437 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.
454 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).JML normal_behavior operation contract.0.key
12184 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12357 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage((B)).JML normal_behavior operation contract.0.key
17501 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17669 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).JML normal_behavior operation contract.0.key
23263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23461 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).JML normal_behavior operation contract.0.key
27447 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27642 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).JML normal_behavior operation contract.0.key
31630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31789 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).JML normal_behavior operation contract.0.key
35741 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
35901 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment___rep()).JML accessible clause.0.key
39863 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40026 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.1.key
54399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54659 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.0.key
68280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68522 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Message(java.lang.Object___inv_()).JML accessible clause.0.key
72459 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72658 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML accessible clause.0.key
78171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78451 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML normal_behavior operation contract.0.key
82999 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83229 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onSendResult()).JML normal_behavior operation contract.0.key
87282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87486 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.1.key
91563 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91776 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.0.key
96345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96673 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(java.lang.Object___inv_()).JML accessible clause.0.key
100603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100820 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key
104949 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105168 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key
109103 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109327 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__publishResult()).JML normal_behavior operation contract.0.key
113735 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113972 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).JML normal_behavior operation contract.0.key
157669 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
158007 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Setup(java.lang.Object___inv_()).JML accessible clause.0.key
166018 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166291 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.1.key
175019 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
175331 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.0.key
187544 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
187859 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(java.lang.Object___inv_()).JML accessible clause.0.key
191682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
851509 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting
851510 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro
448 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
482 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/index/../InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.key
25886 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
26120 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.key
30077 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30227 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.key
34185 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34542 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.key
38509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38660 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.key
42165 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
894030 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro
894031 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro
894031 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro
894033 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro
467 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
486 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
494 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.key
13342 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
907781 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro
907783 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro
389 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
409 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
418 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.key
14901 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15092 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.key
20377 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20567 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.key
24741 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24924 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.key
28856 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29022 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.key
77812 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
78123 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.key
83548 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83756 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.key
88107 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88300 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.key
92002 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92191 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.key
95855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1004030 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro
1004031 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro
454 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
470 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
474 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.key
11942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12124 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.key
16409 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16572 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.key
21998 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
22183 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.key
27024 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27240 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.key
32370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32597 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.key
38214 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
38475 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.key
44132 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
44391 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.key
49883 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50175 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.key
56027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56397 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.key
60252 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60505 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.key
64148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64352 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.key
68052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68270 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.key
72038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
72260 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.key
76175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76407 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.key
80340 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80577 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.key
87068 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87388 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.key
93359 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1097899 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro
1097906 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro
435 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
443 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
446 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.key
15488 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15666 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.key
19870 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20025 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.key
23882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24031 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.key
27665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27812 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.key
31325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31490 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.key
36021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36190 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.key
39824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39998 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.key
44111 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
44301 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.key
47691 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47866 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.key
52389 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52588 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.key
56458 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56662 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.key
60037 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60283 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.key
63654 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63851 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.key
67069 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67262 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.key
70704 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70967 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.key
74389 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
74594 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.key
77981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78181 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.key
81497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81695 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.key
84876 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85090 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.key
88380 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1186727 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro
1186729 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro
414 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
416 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
430 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.key
13932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14107 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.key
19996 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20178 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.key
25646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25825 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.key
39855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
40133 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.key
52758 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
53003 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.key
65464 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65735 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.key
75798 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76028 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.key
83186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83404 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.key
88199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
88405 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.key
92437 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
92702 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.key
98594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
98807 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.key
105045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
105267 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.key
110960 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111180 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.key
116086 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116303 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.key
120892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121109 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.key
124616 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124807 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.key
130525 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1317683 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro
1317685 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro
427 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
464 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
473 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
11431 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
11578 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
15357 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15508 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.key
19020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19175 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.key
22706 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22853 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.key
26323 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26523 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.key
30103 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30369 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.key
33794 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34008 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.key
37261 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37443 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.key
41414 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41601 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.key
47310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47514 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.key
50868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51071 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.key
54318 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54500 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.key
58015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58200 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.key
61558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
61765 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.key
64894 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65108 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.key
68328 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68537 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.key
71751 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71968 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.key
75173 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75369 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.key
78468 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78668 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.key
81789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82042 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.key
85153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
85433 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.key
88606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88844 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.key
92265 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92490 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.key
95802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96021 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.key
99194 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.key
102696 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102933 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.key
106116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106345 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.key
109526 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109767 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.key
113018 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
113262 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.key
116362 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1434483 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro
1434491 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro
411 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
431 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
440 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.key
11673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11832 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.key
16919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17220 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.key
21477 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
21644 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.key
25750 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25903 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.key
29495 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29689 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.key
45406 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45653 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.key
49554 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49727 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.key
74684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
74934 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.key
99325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
99579 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.key
117827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118073 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.key
130997 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
131228 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.key
134735 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
134923 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.key
138731 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138926 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.key
142647 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142853 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.key
147148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
147366 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.key
150775 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150977 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.key
156137 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1591061 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro
1591062 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro
432 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
449 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
453 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.key
20332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20605 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.key
24927 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25091 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.key
29269 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29457 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.key
33560 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33717 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.key
72913 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73211 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.key
118925 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119238 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.key
126619 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126834 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.key
143094 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143348 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.key
163029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1754567 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro
1754569 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro
433 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
453 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
461 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.m.key
10188 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
41280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41494 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.m.key
44932 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
45166 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45317 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.m.key
48489 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48828 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48980 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.m.key
52184 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
52513 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52674 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.m.key
55782 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
55937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56095 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__secure_voting()).Non-interference contract.0.m.key
59183 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
69480 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1824480 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro
1824481 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro
433 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.
462 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.m.key
9681 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
11959 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1836837 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro
1836838 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro
440 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
460 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
468 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key
10822 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
15713 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15886 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key
19961 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
82347 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82646 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.m.key
86336 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
87001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87171 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.m.key
90809 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
90975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91144 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.m.key
94701 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
94876 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95058 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.m.key
98645 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
278651 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
278999 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key
282310 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
284547 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
284749 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key
288275 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
303653 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
303883 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.m.key
307203 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
307844 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
308029 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.m.key
311384 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
311537 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
311754 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.m.key
315126 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
315273 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2152525 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro
2152526 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_fullmacro
413 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.
438 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.m.key
10060 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
11596 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11736 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.m.key
15472 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
16221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16444 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.m.key
19934 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
21666 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
21851 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.m.key
25314 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
26708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26917 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.m.key
30236 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
31755 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31963 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.m.key
35332 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37183 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37418 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.m.key
40711 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
49906 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.m.key
53182 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
54568 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54844 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.m.key
58086 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
59732 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59989 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.m.key
63220 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
63800 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64039 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.m.key
67371 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
67827 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/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.m.key
71285 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
71737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71943 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.m.key
75233 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
75904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
76145 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.m.key
79346 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
79945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80163 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.m.key
83365 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
83995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84239 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.m.key
87408 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
92902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93162 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.m.key
96367 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
98222 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2251255 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro
2251256 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro
421 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
441 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
447 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.m.key
9957 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14778 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.m.key
18344 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19233 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.m.key
22601 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23161 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.m.key
26360 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
26537 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26692 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.m.key
29852 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30296 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.m.key
33374 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
35339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35515 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.m.key
38666 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
38941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39102 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.m.key
42168 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
43071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
43250 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.m.key
46402 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
46546 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46718 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.m.key
49778 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
50774 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50966 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.m.key
54122 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
54724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55008 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.m.key
58080 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
58301 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58502 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.m.key
61589 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
61752 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61965 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.m.key
64985 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
65082 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65306 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.m.key
68304 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
68675 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68881 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.m.key
71857 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
72200 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
72406 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.m.key
75376 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
75743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75988 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.m.key
79019 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
79163 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79367 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.m.key
82369 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
82484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82685 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.m.key
85667 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
85965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2337608 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro
2337609 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro
455 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
463 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/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.m.key
10394 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
17015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
17166 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.m.key
21262 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23124 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.m.key
26860 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
28349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28512 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.m.key
32250 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
307757 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
307968 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.m.key
311601 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
317299 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
317479 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.m.key
321050 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
326278 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
326455 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.m.key
330061 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
334181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
334361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.m.key
337925 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
340775 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
340952 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.m.key
344528 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
347497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
347690 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.m.key
351223 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
353143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
353335 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.m.key
356888 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
358866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
359056 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.m.key
362642 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
365295 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
365496 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.m.key
369028 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
370742 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
370937 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.m.key
374498 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
375636 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
375834 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.m.key
379331 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
380169 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
380372 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.m.key
383951 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
384055 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
384290 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.m.key
387780 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
389273 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2727271 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro
2727273 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro
412 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
436 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
445 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
9810 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
11064 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
11202 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
14904 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
15326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15466 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.m.key
18747 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19123 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.m.key
22379 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22641 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22837 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.m.key
26003 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
26234 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26448 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.m.key
29600 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30152 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30307 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.m.key
33436 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
33734 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33896 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.m.key
37007 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37222 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37390 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.m.key
40446 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
41347 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41530 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.m.key
44563 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
46882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47078 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.m.key
50129 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
50484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50657 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.m.key
53725 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
53944 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54122 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.m.key
57219 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
57549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57747 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.m.key
60775 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
61109 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
61301 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.m.key
64309 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
64411 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64674 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.m.key
67702 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
67865 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68084 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.m.key
71107 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
71262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71534 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.m.key
74502 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
74664 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74862 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.m.key
77829 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
77947 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78153 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.m.key
81126 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
81231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81516 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.m.key
84480 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
84676 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
84889 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.m.key
87941 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
88127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88344 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.m.key
91371 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
91675 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91903 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.m.key
94870 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
95149 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95382 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.m.key
98356 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
98496 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98739 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.m.key
101749 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
102038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102283 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.m.key
105253 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
105485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105726 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.m.key
108684 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
108895 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109257 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.m.key
112233 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
112538 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
112795 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.m.key
115729 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
115889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2843602 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro
2843603 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro
395 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
424 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
430 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.m.key
10500 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
11530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11695 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.m.key
15614 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
16846 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17046 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.m.key
20850 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
21536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
21690 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.m.key
25439 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26113 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.m.key
29737 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
29897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30054 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).Non-interference contract.0.m.key
33733 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48248 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.m.key
51855 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
59353 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59581 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.m.key
63178 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
63751 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63935 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.m.key
67462 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
104507 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
104769 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.0.m.key
108231 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
123518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123747 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).Non-interference contract.0.m.key
127236 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
142252 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142495 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.m.key
145991 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
181785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
182043 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.m.key
185552 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
197791 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
198020 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.m.key
201453 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
211904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
212156 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.m.key
215647 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
215903 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
216111 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.m.key
219550 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
220022 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
220255 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.m.key
223748 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
224101 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
224326 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.m.key
227776 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
228213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
228435 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.m.key
231902 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
231999 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232207 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.m.key
235610 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
237399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3081468 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro
3081469 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro
422 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
431 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
437 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.m.key
11235 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
17710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17909 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).Non-interference contract.0.m.key
22060 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25455 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25648 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.m.key
29494 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
29587 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29794 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.m.key
33705 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
33818 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33983 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.m.key
37778 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37872 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
38043 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.m.key
41785 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
93433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93819 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.m.key
97528 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
151794 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152077 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).Non-interference contract.0.m.key
155730 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
157381 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
157579 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.m.key
161314 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
162611 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
162842 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.m.key
166535 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
187188 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
187437 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.m.key
191083 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
214264 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3296173 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro
3296220 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total rule apps.sum.properties is written
3296221 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total rule apps.avg.properties is written
3296221 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Nodes.sum.properties is written
3296222 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Nodes.avg.properties is written
3296222 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Branches.sum.properties is written
3296222 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Branches.avg.properties is written
3296222 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Overall time (ms).sum.properties is written
3296222 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Overall time (ms).avg.properties is written
3296222 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Automode time (ms).sum.properties is written
3296222 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Automode time (ms).avg.properties is written
3296223 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Closed.sum.properties is written
3296223 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Closed.avg.properties is written
3296223 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Time per step (ms).sum.properties is written
3296223 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Time per step (ms).avg.properties is written
3296223 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total Runtime Memory (kB).sum.properties is written
3296223 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total Runtime Memory (kB).avg.properties is written
3296232 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/NumberTestFiles.properties is written