249 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting
330 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
334 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)
384 INFO 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
8846 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
8966 INFO 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
11918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12022 INFO 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
14901 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15013 INFO 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
17737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17845 INFO 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
20549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20681 INFO 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
24051 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24757 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting
24764 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential
399 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
414 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/ConditionalConfidential/CCExample(CCExample__hasAccessRight(CCExample.User)).JML normal_behavior operation contract.0.key
10236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10424 INFO 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
13694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38739 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential
38740 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample
363 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
380 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
427 INFO 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
9365 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48380 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample
48382 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking
343 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
347 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
374 INFO 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
9627 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9748 INFO 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
34602 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34847 INFO 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
43263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43439 INFO 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
46672 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46838 INFO 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
49897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50024 INFO 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
53060 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53189 INFO 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
62345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62521 INFO 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
65748 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65898 INFO 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
88822 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89029 INFO 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
96204 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
96387 INFO 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
99458 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99623 INFO 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
102500 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102645 INFO 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
105508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105657 INFO 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
111300 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
160059 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking
160060 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts
395 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
415 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/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).JML operation contract.0.key
9449 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9559 INFO 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
12926 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13048 INFO 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
16351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16473 INFO 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
19606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19768 INFO 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
22938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23063 INFO 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
26370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26505 INFO 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
29679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29876 INFO 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
33028 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33177 INFO 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
36198 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36351 INFO 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
39243 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39396 INFO 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
42287 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42433 INFO 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
45315 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45463 INFO 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
48362 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48508 INFO 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
51395 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51548 INFO 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
54491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54667 INFO 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
57916 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58109 INFO 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
61282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
221673 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts
221676 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts
350 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
356 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
383 INFO 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
9598 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9716 INFO 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
13011 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13120 INFO 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
16105 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16221 INFO 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
19031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19161 INFO 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
21895 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22014 INFO 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
24722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24837 INFO 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
27610 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27739 INFO 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
30449 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30582 INFO 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
33279 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33418 INFO 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
36221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36362 INFO 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
39029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39161 INFO 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
41981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42126 INFO 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
44903 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45042 INFO 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
47708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47864 INFO 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
50526 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50672 INFO 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
53301 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53448 INFO 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
56073 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56224 INFO 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
58894 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59041 INFO 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
61673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61826 INFO 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
64433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64593 INFO 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
67213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67390 INFO 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
70082 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
292105 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts
292108 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants
348 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
361 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
390 INFO 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
10074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10242 INFO 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
13963 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14086 INFO 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
17733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17864 INFO 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
21906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22058 INFO 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
25965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26106 INFO 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
29968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30113 INFO 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
33893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34038 INFO 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
37459 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37591 INFO 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
40749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40887 INFO 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
43979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
44130 INFO 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
47433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47597 INFO 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
50893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51054 INFO 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
54311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54492 INFO 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
57541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57687 INFO 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
60737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60883 INFO 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
63881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64038 INFO 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
67267 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
359700 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants
359706 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples
371 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
380 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
425 INFO 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
8609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
8706 INFO 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
11638 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11743 INFO 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
14534 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14649 INFO 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
17419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17560 INFO 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
20262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20377 INFO 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
23240 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23361 INFO 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
26016 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26139 INFO 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
28903 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29035 INFO 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
31782 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31912 INFO 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
34509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34642 INFO 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
37253 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37387 INFO 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
39964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40110 INFO 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
42710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42861 INFO 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
45466 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45612 INFO 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
48207 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48347 INFO 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
50953 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/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).JML normal_behavior operation contract.0.key
53722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53875 INFO 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
56449 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56601 INFO 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
59186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59345 INFO 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
61926 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62081 INFO 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
64652 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64813 INFO 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
67398 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67559 INFO 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
70106 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70273 INFO 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
72855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73032 INFO 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
75582 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75749 INFO 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
78290 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78463 INFO 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
81014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81192 INFO 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
83742 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83923 INFO 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
86493 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86683 INFO 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
89230 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
449280 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples
449281 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects
370 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
375 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
417 INFO 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
9232 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9332 INFO 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
12982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13100 INFO 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
16256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16379 INFO 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
19396 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19524 INFO 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
22390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22505 INFO 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
26612 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26764 INFO 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
30001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30177 INFO 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
32992 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33128 INFO 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
36754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36906 INFO 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
40514 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40689 INFO 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
44214 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44378 INFO 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
47671 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47827 INFO 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
50942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51089 INFO 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
53869 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54023 INFO 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
56779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56988 INFO 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
59836 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60049 INFO 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
62894 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63066 INFO 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
65906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66076 INFO 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
68834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69001 INFO 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
71742 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71914 INFO 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
74929 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
524622 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects
524623 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
373 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
380 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
417 INFO 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
9031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
533904 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
533905 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting
334 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
350 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
396 INFO 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
10489 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10626 INFO 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
14848 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15013 INFO 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
19817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19967 INFO 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
23368 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23532 INFO 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
26888 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
27021 INFO 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
30406 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30532 INFO 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
33868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34004 INFO 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
46194 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46399 INFO 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
57555 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57750 INFO 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
61088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61236 INFO 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
65778 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65947 INFO 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
69648 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69841 INFO 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
73160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73328 INFO 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
76664 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76831 INFO 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
80528 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80701 INFO 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
84027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84210 INFO 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
87626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87800 INFO 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
91014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91191 INFO 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
94882 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/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).JML normal_behavior operation contract.0.key
131815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
132081 INFO 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
138757 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139069 INFO 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
146178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146415 INFO 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
156450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156697 INFO 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
160005 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
694261 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting
694265 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro
351 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
370 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
412 INFO 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
20794 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
20994 INFO 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
24102 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24329 INFO 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
27193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27317 INFO 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
30079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30232 INFO 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
32882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
727440 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro
727442 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro
727442 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro
727443 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro
363 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
377 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
421 INFO 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
11301 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
739055 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro
739056 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro
353 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
378 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
427 INFO 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
12360 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12507 INFO 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
16675 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16807 INFO 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
20086 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20226 INFO 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
23358 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23488 INFO 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
66135 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
66397 INFO 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
70818 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71083 INFO 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
74499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74659 INFO 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
77519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77664 INFO 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
80531 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
819889 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro
819890 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro
397 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.
456 INFO 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
9984 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10105 INFO 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
13559 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13698 INFO 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
17990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18153 INFO 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
22152 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22331 INFO 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
26271 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26487 INFO 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
30950 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31236 INFO 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
35839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36046 INFO 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
40525 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40769 INFO 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
45543 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45763 INFO 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
48974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49189 INFO 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
52137 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52304 INFO 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
55267 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55433 INFO 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
58509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
58679 INFO 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
61806 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61983 INFO 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
65235 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65435 INFO 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
70651 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70929 INFO 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
75762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
896031 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro
896032 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro
334 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
346 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
389 INFO 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
11642 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11820 INFO 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
15151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15265 INFO 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
18288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18431 INFO 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
21288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21410 INFO 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
24255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24380 INFO 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
27893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28023 INFO 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
30839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30973 INFO 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
34326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34507 INFO 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
37194 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37367 INFO 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
41057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41284 INFO 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
44328 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44485 INFO 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
47218 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47366 INFO 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
50137 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50288 INFO 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
52940 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53087 INFO 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
55916 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56076 INFO 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
58814 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
59045 INFO 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
61784 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61974 INFO 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
64624 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64785 INFO 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
67390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67608 INFO 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
70327 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
966684 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro
966685 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro
363 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
371 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
399 INFO 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
12439 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
12600 INFO 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
17515 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17693 INFO 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
22218 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22394 INFO 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
34020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34222 INFO 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
44754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45035 INFO 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
55151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55446 INFO 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
63541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63736 INFO 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
69605 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69803 INFO 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
73802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
73977 INFO 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
77332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
77521 INFO 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
82371 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
82556 INFO 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
87747 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
87981 INFO 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
92607 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92866 INFO 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
96906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97094 INFO 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
101011 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101206 INFO 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
104190 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104349 INFO 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
109177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1076210 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro
1076211 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro
412 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.
478 INFO 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
8995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9104 INFO 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
12144 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12259 INFO 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
15097 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15208 INFO 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
17913 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18034 INFO 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
20728 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20893 INFO 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
23749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
23985 INFO 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
26754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26882 INFO 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
29495 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29624 INFO 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
32841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32997 INFO 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
37397 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37556 INFO 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
40260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40416 INFO 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
42961 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43103 INFO 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
45793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45945 INFO 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
48545 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
48700 INFO 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
51179 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51358 INFO 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
53965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54120 INFO 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
56610 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56772 INFO 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
59255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59483 INFO 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
62001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62173 INFO 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
64613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64774 INFO 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
67210 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
67376 INFO 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
69813 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69981 INFO 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
72605 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72783 INFO 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
75429 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75605 INFO 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
78121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78293 INFO 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
80919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81142 INFO 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
83699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83905 INFO 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
86401 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86589 INFO 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
89109 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
89305 INFO 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
91715 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1168271 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro
1168271 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro
327 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
329 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
372 INFO 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
9078 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9186 INFO 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
13481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13608 INFO 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
16949 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
17073 INFO 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
20399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20555 INFO 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
23453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23572 INFO 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
35771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35957 INFO 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
39399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39544 INFO 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
60139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
60339 INFO 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
80515 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
80788 INFO 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
96016 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96264 INFO 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
107502 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
107689 INFO 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
110581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
110757 INFO 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
113954 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114118 INFO 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
117105 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117268 INFO 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
120753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120921 INFO 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
123753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123926 INFO 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
128148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1296774 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro
1296775 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro
340 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
352 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
384 INFO 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
16511 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16683 INFO 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
20312 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20430 INFO 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
23922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24047 INFO 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
27399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
27525 INFO 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
58021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58263 INFO 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
94069 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94314 INFO 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
100402 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100579 INFO 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
113855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114046 INFO 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
129677 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1426817 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro
1426819 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro
346 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
353 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
380 INFO 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
8280 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
33263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33499 INFO 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
36287 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
36549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36781 INFO 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
39318 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
39615 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39744 INFO 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
42305 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
42565 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42715 INFO 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
45199 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
45322 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45448 INFO 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
47880 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
56372 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1483599 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro
1483600 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro
353 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
366 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
396 INFO 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
7866 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9872 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1493778 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro
1493778 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro
392 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
399 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
427 INFO 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
8539 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
12690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12859 INFO 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
15961 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
65171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65484 INFO 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
68401 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
68947 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69233 INFO 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
72074 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
72208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72352 INFO 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
75251 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
75396 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75545 INFO 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
78372 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
220229 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
220562 INFO 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
223203 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
224964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
225392 INFO 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
228102 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
240372 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
240643 INFO 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
243311 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
243827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
244023 INFO 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
246741 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
246864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
247028 INFO 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
249690 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
249837 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1743951 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro
1743954 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_fullmacro
336 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
349 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/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.m.key
8224 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9535 INFO 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
12562 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13227 INFO 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
15960 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
17150 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
17322 INFO 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
19937 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
20939 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21150 INFO 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
23819 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24952 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25125 INFO 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
27693 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
29050 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29266 INFO 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
31808 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
38760 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
39037 INFO 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
41619 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
42722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42970 INFO 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
45513 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
46767 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46995 INFO 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
49536 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49966 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50198 INFO 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
52713 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
53036 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53250 INFO 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
55799 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
56127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56317 INFO 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
58863 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
59381 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
59582 INFO 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
62077 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
62534 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62738 INFO 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
65274 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
65807 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66033 INFO 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
68560 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
72832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73072 INFO 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
75536 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
77020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1821404 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro
1821405 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro
381 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
395 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
436 INFO 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
8458 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
12498 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12644 INFO 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
15606 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
16162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16307 INFO 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
19037 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19330 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19475 INFO 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
22174 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22315 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22447 INFO 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
25109 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25475 INFO 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
28061 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
29597 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29758 INFO 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
32336 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
32552 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32688 INFO 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
35292 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
36021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36178 INFO 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
38692 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
38811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38990 INFO 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
41536 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
42403 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42575 INFO 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
45094 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
45559 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45722 INFO 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
48263 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48454 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48624 INFO 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
51152 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
51283 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51443 INFO 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
53911 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
54005 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54163 INFO 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
56625 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
56934 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57105 INFO 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
59597 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
59892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
60086 INFO 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
62541 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
62821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63008 INFO 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
65501 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
65609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65778 INFO 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
68250 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
68338 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68510 INFO 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
70957 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
71188 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1892966 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro
1892967 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro
345 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
352 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
387 INFO 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
9361 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14829 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14995 INFO 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
18228 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19478 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19667 INFO 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
22751 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
23908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24120 INFO 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
27164 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
246140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
246404 INFO 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
249339 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
253890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
254170 INFO 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
257043 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
261239 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
261464 INFO 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
264324 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
267678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
267905 INFO 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
270766 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
273103 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
273319 INFO 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
276204 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
278608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
278800 INFO 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
281684 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
283287 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
283510 INFO 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
286388 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
287988 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
288176 INFO 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
291045 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
293212 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
293440 INFO 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
296314 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
297700 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
297936 INFO 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
300735 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
301624 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
301812 INFO 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
304637 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
305336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
305523 INFO 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
308357 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
308438 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
308606 INFO 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
311419 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
312605 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2205955 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro
2205956 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro
378 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
388 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/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
8287 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9393 INFO 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
12211 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
12495 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12636 INFO 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
15403 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
15518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15663 INFO 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
18289 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18455 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18591 INFO 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
21157 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
21306 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21429 INFO 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
24006 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24284 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24426 INFO 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
26976 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
27171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27363 INFO 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
29927 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30206 INFO 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
32725 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
33272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33464 INFO 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
36019 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37900 INFO 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
40453 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
40672 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40866 INFO 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
43391 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
43515 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43671 INFO 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
46192 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
46416 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46571 INFO 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
49091 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49317 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
49484 INFO 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
51995 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
52087 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52268 INFO 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
54750 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
54892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55051 INFO 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
57561 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
57695 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57859 INFO 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
60383 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
60478 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60647 INFO 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
63118 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
63206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63375 INFO 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
65839 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
65918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66121 INFO 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
68586 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
68699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
68879 INFO 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
71328 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
71430 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71617 INFO 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
74080 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
74311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74532 INFO 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
76983 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
77187 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77375 INFO 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
79824 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
79925 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80125 INFO 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
82613 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
82808 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83043 INFO 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
85530 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
85710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85896 INFO 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
88360 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
88508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88712 INFO 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
91166 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
91402 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
91634 INFO 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
94079 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
94211 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2300582 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro
2300582 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro
332 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
337 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
375 INFO 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
8639 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9520 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9637 INFO 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
12800 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13797 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13959 INFO 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
16716 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
17285 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
17424 INFO 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
20189 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
20606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20771 INFO 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
23503 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
23637 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23779 INFO 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
26490 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
36981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37218 INFO 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
39867 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
45535 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45782 INFO 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
48427 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48913 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49089 INFO 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
51747 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
80347 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
80574 INFO 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
83185 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
95010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95303 INFO 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
97875 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
109418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109653 INFO 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
112306 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
139921 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
140166 INFO 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
142768 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
152134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152398 INFO 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
154936 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
163001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
163195 INFO 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
165772 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
165977 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
166184 INFO 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
168770 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
169164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169349 INFO 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
171951 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
172212 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
172406 INFO 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
174965 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
175310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
175500 INFO 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
178115 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
178195 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178389 INFO 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
180950 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
182351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2483349 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro
2483350 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro
410 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
420 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
451 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.m.key
9319 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14938 INFO 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
18381 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
21080 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21250 INFO 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
24546 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24784 INFO 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
28030 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
28146 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
28278 INFO 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
31497 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
31597 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31738 INFO 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
34870 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
78121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78436 INFO 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
81500 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
126435 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126739 INFO 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
129798 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
131165 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131439 INFO 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
134532 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
135572 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135759 INFO 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
138884 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
155981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156251 INFO 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
159341 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
178501 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2662298 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro
2662346 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
2662347 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
2662347 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
2662348 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
2662348 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
2662348 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
2662348 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
2662348 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
2662348 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
2662348 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
2662348 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
2662348 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
2662349 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
2662349 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
2662349 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
2662349 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
2662349 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