565 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting
348 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 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)
365 INFO 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
9428 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9571 INFO 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
12646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12762 INFO 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
15645 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15795 INFO 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
18589 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18712 INFO 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
21521 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21681 INFO 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
24959 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25881 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting
25900 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential
346 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.
366 INFO 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
10162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10315 INFO 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
13577 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39796 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential
39797 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample
374 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.
386 INFO 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
9331 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49423 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample
49424 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking
391 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
400 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
406 INFO 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
9817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9946 INFO 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
36049 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36261 INFO 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
44801 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44973 INFO 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
48192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48344 INFO 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
51330 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51463 INFO 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
54412 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54555 INFO 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
63810 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63997 INFO 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
67196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67369 INFO 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
91283 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91519 INFO 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
98852 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
99049 INFO 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
102067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102238 INFO 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
105040 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105201 INFO 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
108020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108177 INFO 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
113897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163703 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking
163704 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts
347 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
355 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
359 INFO 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
9373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9516 INFO 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
12941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13063 INFO 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
16475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16608 INFO 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
19897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20042 INFO 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
23269 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23409 INFO 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
26706 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26868 INFO 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
30179 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30336 INFO 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
33603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33756 INFO 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
36929 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37133 INFO 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
40211 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40423 INFO 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
43475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43636 INFO 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
46661 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46859 INFO 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
49895 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50057 INFO 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
53059 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53234 INFO 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
56247 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56419 INFO 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
59927 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60116 INFO 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
63379 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
227418 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts
227420 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts
373 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
398 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
406 INFO 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
9231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9359 INFO 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
12471 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12634 INFO 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
15662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15824 INFO 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
18691 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18814 INFO 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
21586 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21710 INFO 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
24506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24675 INFO 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
27419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27580 INFO 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
30288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30422 INFO 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
33127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33274 INFO 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
36065 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36228 INFO 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
38914 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39058 INFO 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
41907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42064 INFO 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
44831 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44983 INFO 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
47636 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47805 INFO 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
50450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50604 INFO 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
53246 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53405 INFO 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
56082 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56244 INFO 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
58906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59068 INFO 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
61709 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61873 INFO 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
64475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64645 INFO 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
67252 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67425 INFO 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
70044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
297809 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts
297812 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants
354 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.
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/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key
9745 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9874 INFO 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
13697 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13821 INFO 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
17462 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17604 INFO 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
21747 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21900 INFO 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
26014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26168 INFO 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
30038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30190 INFO 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
34038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34202 INFO 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
37673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37831 INFO 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
40921 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41068 INFO 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
44189 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
44339 INFO 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
47631 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47794 INFO 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
51110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51274 INFO 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
54592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54754 INFO 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
57853 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58014 INFO 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
61093 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61267 INFO 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
64321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64485 INFO 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
67796 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
365971 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants
365973 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples
378 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.
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/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
8228 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
8333 INFO 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
11336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11446 INFO 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
14242 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14362 INFO 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
17093 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17217 INFO 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
19899 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20020 INFO 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
22649 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22776 INFO 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
25428 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25594 INFO 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
28202 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28367 INFO 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
31101 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31235 INFO 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
34024 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34181 INFO 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
36821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37041 INFO 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
39669 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39819 INFO 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
42420 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42577 INFO 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
45169 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45322 INFO 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
47897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48063 INFO 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
50709 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50921 INFO 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
53509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53685 INFO 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
56233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56399 INFO 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
58959 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59125 INFO 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
61672 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61848 INFO 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
64409 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/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).JML normal_behavior operation contract.0.key
67174 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67355 INFO 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
69881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70065 INFO 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
72601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72856 INFO 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
75381 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75563 INFO 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
78121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78347 INFO 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
80873 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81071 INFO 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
83621 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83819 INFO 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
86317 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86531 INFO 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
89108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
455472 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples
455473 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects
419 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
428 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
432 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).JML operation contract.0.key
9426 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9533 INFO 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
13426 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13585 INFO 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
16763 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16890 INFO 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
20058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20189 INFO 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
23142 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23299 INFO 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
27493 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27665 INFO 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
31059 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31247 INFO 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
34121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34261 INFO 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
37972 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38134 INFO 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
41665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41835 INFO 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
45288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45473 INFO 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
48856 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49036 INFO 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
52196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52363 INFO 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
55172 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55329 INFO 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
58173 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58337 INFO 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
61242 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61412 INFO 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
64332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64502 INFO 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
67384 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67553 INFO 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
70399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70579 INFO 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
73343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73517 INFO 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
76520 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
532443 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects
532445 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
331 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
341 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
345 INFO 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
8953 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
541656 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
541659 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting
344 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
365 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
373 INFO 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
10851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10992 INFO 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
14981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15120 INFO 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
19920 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20125 INFO 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
23422 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23598 INFO 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
26832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
26995 INFO 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
30187 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30351 INFO 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
33518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33660 INFO 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
46223 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46427 INFO 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
57417 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57621 INFO 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
60842 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61008 INFO 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
65475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65655 INFO 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
69368 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69555 INFO 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
72751 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72922 INFO 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
76140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76323 INFO 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
80018 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80204 INFO 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
83394 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83579 INFO 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
86866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87050 INFO 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
90138 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90319 INFO 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
93886 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94087 INFO 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
130925 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
131210 INFO 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
137860 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138083 INFO 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
145250 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
145529 INFO 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
155839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156111 INFO 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
159315 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
701356 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting
701358 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro
363 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
382 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
385 INFO 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
21805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
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/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.key
25297 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25438 INFO 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
28787 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28958 INFO 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
32047 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32178 INFO 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
35085 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
736754 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro
736755 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro
736756 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro
736757 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro
343 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.
365 INFO 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
11543 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
748658 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro
748660 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro
410 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.
424 INFO 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
12653 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12812 INFO 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
17108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17253 INFO 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
20651 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20793 INFO 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
24143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24308 INFO 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
67782 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
68053 INFO 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
72490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72668 INFO 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
76233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76393 INFO 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
79469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79624 INFO 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
82646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
831653 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro
831655 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro
383 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
387 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
391 INFO 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
9982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10117 INFO 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
13776 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13926 INFO 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
18322 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18528 INFO 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
22498 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22682 INFO 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
26975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27177 INFO 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
31820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32045 INFO 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
36747 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37063 INFO 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
41600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41840 INFO 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
46732 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46976 INFO 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
50223 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50441 INFO 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
53421 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53653 INFO 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
56668 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56857 INFO 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
60018 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
60247 INFO 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
63438 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63639 INFO 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
66956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67156 INFO 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
72485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72731 INFO 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
77682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
909733 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro
909735 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro
374 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.
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/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.key
13108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13270 INFO 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
16579 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16712 INFO 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
19819 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19946 INFO 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
22846 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23014 INFO 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
25875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26012 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.key
29541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29687 INFO 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
32504 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32650 INFO 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
36043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36205 INFO 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
38879 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39028 INFO 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
42724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42893 INFO 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
46081 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46254 INFO 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
49029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49188 INFO 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
51982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52148 INFO 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
54785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54944 INFO 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
57783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57961 INFO 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
60647 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
60824 INFO 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
63595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63760 INFO 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
66340 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66539 INFO 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
69167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69336 INFO 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
72071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
982158 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro
982159 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro
362 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
362 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
371 INFO 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
11655 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
11870 INFO 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
16861 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17020 INFO 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
21559 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21716 INFO 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
33646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33861 INFO 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
44584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
44828 INFO 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
55214 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55429 INFO 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
63673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63885 INFO 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
69889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70090 INFO 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
74024 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
74210 INFO 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
77453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
77615 INFO 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
82344 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
82539 INFO 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
87635 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
87841 INFO 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
92462 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92676 INFO 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
96641 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96822 INFO 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
100632 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100812 INFO 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
103700 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103862 INFO 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
108517 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1091054 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro
1091056 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro
362 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
373 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/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
9112 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9240 INFO 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
12549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12673 INFO 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
15485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15620 INFO 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
18557 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18708 INFO 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
21443 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21571 INFO 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
24415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24550 INFO 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
27408 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27540 INFO 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
30220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30361 INFO 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
33774 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33936 INFO 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
38540 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
38711 INFO 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
41532 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41691 INFO 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
44395 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44549 INFO 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
47329 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47490 INFO 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
50163 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
50326 INFO 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
52867 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53066 INFO 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
55735 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55901 INFO 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
58556 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58727 INFO 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
61270 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61439 INFO 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
63983 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64212 INFO 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
66743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66928 INFO 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
69485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
69664 INFO 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
72351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72554 INFO 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
75291 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75485 INFO 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
78232 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78444 INFO 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
81067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81283 INFO 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
84047 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84250 INFO 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
86904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87166 INFO 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
89843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90146 INFO 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
92795 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
93013 INFO 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
95491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1186943 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro
1186944 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro
330 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
343 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
349 INFO 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
9190 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9314 INFO 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
13565 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13716 INFO 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
17279 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
17415 INFO 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
20789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20928 INFO 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
23968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24093 INFO 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
36390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36602 INFO 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
39883 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40037 INFO 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
60485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
60703 INFO 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
80609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
80809 INFO 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
95670 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95868 INFO 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
106608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
106797 INFO 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
109729 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
109894 INFO 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
113118 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113293 INFO 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
116283 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116446 INFO 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
119950 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120125 INFO 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
122919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123096 INFO 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
127461 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1314789 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro
1314790 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro
352 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.
367 INFO 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
17155 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17343 INFO 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
21028 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21180 INFO 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
24634 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24775 INFO 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
28181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
28332 INFO 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
60196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60443 INFO 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
97868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98114 INFO 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
104325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104512 INFO 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
118164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118369 INFO 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
134672 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1449861 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro
1449862 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro
367 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.
373 INFO 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
8699 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
34244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34463 INFO 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
37257 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37482 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37597 INFO 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
40273 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
40581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40760 INFO 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
43406 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
43710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43841 INFO 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
46608 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
46736 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46865 INFO 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
49465 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
58186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1508422 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro
1508423 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro
338 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
365 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/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.m.key
8208 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
10162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1518875 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro
1518876 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro
409 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
421 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/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key
8912 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13225 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13421 INFO 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
16686 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
68058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68314 INFO 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
71300 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
71911 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72095 INFO 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
75109 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
75275 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75414 INFO 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
78415 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
78583 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78718 INFO 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
81724 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
228783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
229106 INFO 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
231859 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
233721 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
233891 INFO 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
236672 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
249422 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
249633 INFO 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
252436 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
252962 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
253149 INFO 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
255933 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
256083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
256234 INFO 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
258975 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
259131 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1778342 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro
1778345 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.)
341 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
345 INFO 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
8751 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10108 INFO 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
13226 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13727 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13889 INFO 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
16793 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18230 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18386 INFO 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
21252 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22360 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22526 INFO 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
25291 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
26441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26632 INFO 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
29513 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30899 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31121 INFO 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
33877 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
41263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41514 INFO 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
44192 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
45381 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45622 INFO 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
48276 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49657 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49914 INFO 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
52587 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
53078 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53297 INFO 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
55960 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
56329 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56543 INFO 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
59206 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
59549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59778 INFO 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
62446 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
62999 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
63193 INFO 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
65846 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
66307 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66512 INFO 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
69183 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
69715 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69952 INFO 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
72599 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
77093 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77338 INFO 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
79971 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
81464 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1860179 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro
1860179 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro
349 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
357 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
361 INFO 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
8899 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
12804 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12942 INFO 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
15859 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
16510 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16685 INFO 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
19541 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19859 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19992 INFO 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
22693 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22845 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22968 INFO 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
25662 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26032 INFO 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
28666 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30285 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30435 INFO 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
33077 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
33285 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33428 INFO 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
36029 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
36783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36969 INFO 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
39565 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
39682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39852 INFO 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
42466 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
43300 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43545 INFO 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
46166 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
46638 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46873 INFO 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
49441 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49638 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49799 INFO 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
52379 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
52516 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52675 INFO 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
55251 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
55335 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55510 INFO 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
58102 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
58397 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58573 INFO 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
61120 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
61437 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
61610 INFO 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
64141 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
64441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64616 INFO 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
67147 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
67260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67456 INFO 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
70002 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
70093 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70278 INFO 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
72819 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
73056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1933582 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro
1933582 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro
354 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
379 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
8838 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14069 INFO 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
17496 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19022 INFO 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
22032 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
23382 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23512 INFO 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
26556 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
254255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
254437 INFO 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
257383 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
262321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
262482 INFO 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
265455 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
269994 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
270140 INFO 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
273165 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
276786 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
276943 INFO 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
279868 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
282390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
282549 INFO 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
285491 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
288125 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
288306 INFO 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
291236 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
292901 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
293064 INFO 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
295971 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
297696 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
297854 INFO 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
300721 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
303025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
303196 INFO 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
306029 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
307518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
307688 INFO 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
310575 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
311575 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
311748 INFO 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
314602 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
315354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
315539 INFO 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
318448 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
318539 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
318713 INFO 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
321592 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
322875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2256810 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro
2256814 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro
392 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.
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/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
8850 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
10062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
10173 INFO 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
13189 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13651 INFO 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
16561 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
16714 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16831 INFO 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
19599 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19777 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19907 INFO 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
22634 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22946 INFO 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
25627 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25934 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
26083 INFO 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
28827 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
29070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29238 INFO 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
31955 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
32098 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32265 INFO 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
34970 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
35578 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
35723 INFO 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
38444 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
40178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
40334 INFO 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
42974 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
43234 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43400 INFO 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
46138 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
46271 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46431 INFO 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
49074 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49488 INFO 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
52129 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
52422 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
52621 INFO 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
55237 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
55316 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55508 INFO 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
58117 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
58247 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58421 INFO 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
61022 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
61139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61311 INFO 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
63877 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
63990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64162 INFO 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
66721 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
66835 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67016 INFO 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
69585 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
69671 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69851 INFO 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
72409 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
72525 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
72715 INFO 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
75290 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
75408 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75596 INFO 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
78145 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
78382 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78578 INFO 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
81085 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
81296 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81485 INFO 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
84036 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
84153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84350 INFO 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
86963 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
87186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87391 INFO 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
89899 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
90052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90259 INFO 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
92803 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
92957 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93170 INFO 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
95694 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
95931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
96184 INFO 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
98688 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
98797 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2356000 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro
2356001 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro
358 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
363 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
369 INFO 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
9149 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9984 INFO 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
13294 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14471 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14642 INFO 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
17793 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18525 INFO 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
21559 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22085 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22219 INFO 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
25246 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25502 INFO 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
28470 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
39738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39928 INFO 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
42876 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48894 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49087 INFO 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
52008 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
52453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52623 INFO 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
55548 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
85654 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
85855 INFO 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
88726 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
101084 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101294 INFO 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
104166 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
116227 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116426 INFO 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
119250 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
147936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
148158 INFO 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
150997 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
160838 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161041 INFO 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
163870 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
172295 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
172499 INFO 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
175319 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
175545 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
175718 INFO 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
178536 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
178949 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
179123 INFO 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
181953 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
182241 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
182439 INFO 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
185249 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
185609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
185799 INFO 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
188628 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
188712 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
188896 INFO 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
191707 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
193199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2549617 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro
2549618 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro
361 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
369 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.m.key
9120 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14227 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14371 INFO 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
18425 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
21073 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21249 INFO 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
24557 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24627 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24795 INFO 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
28050 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
28143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
28296 INFO 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
31580 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
31656 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31799 INFO 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
35034 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
77182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77449 INFO 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
80629 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
125180 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125413 INFO 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
128588 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
129961 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130140 INFO 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
133398 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
134490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134671 INFO 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
137902 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
154877 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
155089 INFO 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
158198 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
177491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2727482 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro
2727505 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
2727506 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
2727507 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
2727507 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
2727507 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
2727508 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
2727508 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
2727508 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
2727508 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
2727509 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
2727509 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
2727509 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
2727509 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
2727509 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
2727510 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
2727510 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
2727510 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