687 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting
488 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
511 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)
567 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).JML normal_behavior operation contract.0.key
13124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13306 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).JML normal_behavior operation contract.0.key
17583 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17734 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__isValid(int)).JML normal_behavior operation contract.0.key
21849 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22031 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).JML normal_behavior operation contract.0.key
25907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26086 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__inputVote()).JML normal_behavior operation contract.0.key
29927 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30091 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__secure_voting()).JML normal_behavior operation contract.0.key
35116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36333 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting
36344 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential
531 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
555 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
602 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ConditionalConfidential/CCExample(CCExample__hasAccessRight(CCExample.User)).JML normal_behavior operation contract.0.key
15441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15658 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ConditionalConfidential/CCExample(CCExample__getConfidentialData(CCExample.User)).JML normal_behavior operation contract.0.key
20564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57322 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential
57329 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample
501 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
530 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
585 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/Sum/SumExample(SumExample__getSum()).JML normal_behavior operation contract.0.key
14612 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72345 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample
72346 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking
477 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
510 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
566 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key
14341 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14559 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key
51218 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51554 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key
63559 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63817 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key
68205 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68400 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).JML normal_behavior operation contract.0.key
72428 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72622 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).JML normal_behavior operation contract.0.key
76670 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76869 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).JML normal_behavior operation contract.0.key
90044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90307 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key
94598 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94833 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key
128892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129228 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key
139697 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
140023 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key
144108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144339 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).JML normal_behavior operation contract.0.key
148128 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
148342 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).JML normal_behavior operation contract.0.key
152147 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152357 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.Bank(banking_example2.Bank__login(int,(C)).JML normal_behavior operation contract.0.key
160054 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232926 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking
232929 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts
516 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
544 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
607 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).JML operation contract.0.key
13433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13582 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).JML operation contract.0.key
18205 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18385 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).JML operation contract.0.key
23186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23373 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).JML operation contract.0.key
27823 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28027 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).JML operation contract.0.key
32427 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32623 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).JML operation contract.0.key
37080 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37321 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).JML operation contract.0.key
41714 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41956 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).JML operation contract.0.key
46194 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46405 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).JML operation contract.0.key
50514 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50731 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).JML operation contract.0.key
54815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55056 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).JML operation contract.0.key
58919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59137 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).JML operation contract.0.key
62907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63124 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).JML operation contract.0.key
66872 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67109 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).JML operation contract.0.key
70793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71024 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).JML operation contract.0.key
74677 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74913 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).JML operation contract.0.key
79491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79774 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).JML operation contract.0.key
83958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
317402 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts
317406 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts
494 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
496 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
538 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).JML normal_behavior operation contract.0.key
12936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13106 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).JML normal_behavior operation contract.0.key
17687 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17861 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).JML operation contract.0.key
22095 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22273 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).JML normal_behavior operation contract.0.key
26252 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26476 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).JML operation contract.0.key
30199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30382 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param_helper()).JML normal_behavior operation contract.0.key
34121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34370 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).JML operation contract.0.key
38106 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38362 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n9()).JML normal_behavior operation contract.0.key
41986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42175 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).JML operation contract.0.key
45810 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45994 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).JML operation contract.0.key
49770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49962 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).JML normal_behavior operation contract.0.key
53637 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53838 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).JML operation contract.0.key
57759 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57997 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).JML operation contract.0.key
61919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62237 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).JML operation contract.0.key
66014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66249 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).JML normal_behavior operation contract.0.key
69954 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70161 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).JML normal_behavior operation contract.0.key
73902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74120 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).JML operation contract.0.key
77842 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78058 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).JML operation contract.0.key
81756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81979 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).JML operation contract.0.key
85660 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85893 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).JML normal_behavior operation contract.0.key
89598 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89830 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).JML normal_behavior operation contract.0.key
93499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93724 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).JML operation contract.0.key
97363 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
415332 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts
415337 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants
542 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
567 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
600 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key
14339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14513 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).JML operation contract.0.key
19788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19978 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).JML operation contract.0.key
24892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25086 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).JML operation contract.0.key
30701 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30931 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).JML operation contract.0.key
36418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36651 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).JML operation contract.0.key
41965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42184 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).JML operation contract.0.key
47655 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47864 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).JML operation contract.0.key
52655 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52866 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).JML operation contract.0.key
57171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57385 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).JML operation contract.0.key
61767 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
61985 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).JML operation contract.0.key
66486 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66733 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).JML operation contract.0.key
71318 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71621 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).JML operation contract.0.key
76192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76420 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).JML operation contract.0.key
80749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80996 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).JML operation contract.0.key
85281 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85567 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).JML normal_behavior operation contract.0.key
89653 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89875 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).JML normal_behavior operation contract.0.key
94325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
510149 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants
510151 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples
525 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
548 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
578 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
12928 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13065 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
17197 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17347 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).JML normal_behavior operation contract.0.key
21277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21447 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).JML normal_behavior operation contract.0.key
25252 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25466 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).JML normal_behavior operation contract.0.key
29151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29311 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).JML normal_behavior operation contract.0.key
33050 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33276 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).JML normal_behavior operation contract.0.key
37070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37247 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).JML normal_behavior operation contract.0.key
40931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41115 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.1.key
44779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44987 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.0.key
48542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48740 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).JML normal_behavior operation contract.0.key
52208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52455 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).JML operation contract.0.key
55866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56090 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).JML normal_behavior operation contract.0.key
59500 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59705 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).JML normal_behavior operation contract.0.key
63139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63350 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).JML normal_behavior operation contract.0.key
66781 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66990 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).JML normal_behavior operation contract.0.key
70386 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70603 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).JML normal_behavior operation contract.0.key
73986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74286 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).JML normal_behavior operation contract.0.key
77771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78002 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).JML normal_behavior operation contract.0.key
81384 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81605 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).JML normal_behavior operation contract.0.key
84989 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85218 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).JML normal_behavior operation contract.0.key
88497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88741 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).JML normal_behavior operation contract.0.key
92014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92259 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).JML normal_behavior operation contract.0.key
95703 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95959 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).JML normal_behavior operation contract.0.key
99220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99463 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).JML normal_behavior operation contract.0.key
102699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102943 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).JML normal_behavior operation contract.0.key
106286 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106542 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.1.key
109952 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110239 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.0.key
113550 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113835 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).JML normal_behavior operation contract.0.key
117126 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117394 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).JML normal_behavior operation contract.0.key
120775 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
631425 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples
631426 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects
464 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
478 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
525 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).JML operation contract.0.key
12865 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13013 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).JML normal_behavior operation contract.0.key
18443 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18624 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.1.key
23134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23316 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.0.key
27583 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27777 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).JML normal_behavior operation contract.0.key
31871 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32077 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).JML operation contract.0.key
38031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38246 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).JML operation contract.0.key
42935 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43158 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).JML operation contract.0.key
47077 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47271 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.1.key
52292 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52538 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.0.key
57440 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57723 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).JML operation contract.0.key
62679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62925 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).JML operation contract.0.key
67573 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67920 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).JML normal_behavior operation contract.0.key
72288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72542 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.1.key
76467 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76688 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.0.key
80555 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80785 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).JML operation contract.0.key
84754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85036 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).JML operation contract.0.key
89001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89240 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).JML operation contract.0.key
93349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93609 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML accessible clause.0.key
97557 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97858 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML normal_behavior operation contract.0.key
101743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101989 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).JML normal_behavior operation contract.0.key
106166 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106512 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/PasswordFile/passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
110102 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
742036 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects
742043 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting
504 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
526 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
552 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).JML normal_behavior operation contract.0.key
14246 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14445 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage((B)).JML normal_behavior operation contract.0.key
20045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20240 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).JML normal_behavior operation contract.0.key
27041 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27301 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).JML normal_behavior operation contract.0.key
31846 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32111 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).JML normal_behavior operation contract.0.key
36585 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36787 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).JML normal_behavior operation contract.0.key
41251 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41507 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment___rep()).JML accessible clause.0.key
45949 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46134 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.1.key
63445 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63752 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.0.key
79918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80202 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Message(java.lang.Object___inv_()).JML accessible clause.0.key
84516 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84723 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML accessible clause.0.key
90824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91090 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML normal_behavior operation contract.0.key
96125 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96366 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onSendResult()).JML normal_behavior operation contract.0.key
100730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100965 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.1.key
105490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105745 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.0.key
110875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111150 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Server(java.lang.Object___inv_()).JML accessible clause.0.key
115564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115803 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key
120346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120635 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key
125104 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125362 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__publishResult()).JML normal_behavior operation contract.0.key
130339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130617 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).JML normal_behavior operation contract.0.key
182296 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
182693 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Setup(java.lang.Object___inv_()).JML accessible clause.0.key
192016 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
192493 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.1.key
202558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
202897 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.0.key
217060 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
217429 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(java.lang.Object___inv_()).JML accessible clause.0.key
221695 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
964228 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting
964230 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro
513 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
548 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
608 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.key
29311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29605 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.key
33960 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34241 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.key
38466 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38656 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.key
42698 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42879 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.key
46652 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1011298 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro
1011299 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro
1011300 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro
1011301 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro
436 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
448 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
501 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.key
15811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1027521 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro
1027523 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro
527 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
549 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
579 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.key
17166 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.key
22976 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23152 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.key
27607 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27798 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.key
32008 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32195 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.key
91069 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
91440 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.key
97582 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98040 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.key
102772 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103013 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.key
107033 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107256 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.key
111329 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1139277 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro
1139279 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro
495 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
523 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
578 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.key
14255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14432 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.key
19508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19719 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.key
26078 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
26329 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.key
32037 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32295 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.key
38177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38453 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.key
44717 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45090 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.key
51614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
51961 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.key
58197 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58519 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.key
65083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65426 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.key
69902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70208 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.key
74523 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74768 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.key
79048 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79292 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.key
83701 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
83954 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.key
88417 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88698 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.key
93318 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93618 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.key
101140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101492 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.key
108409 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1248226 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro
1248229 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro
514 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
542 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
597 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.key
16809 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17096 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.key
21661 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21859 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.key
26019 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26200 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.key
30031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30211 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.key
33957 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34138 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.key
39140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39331 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.key
43157 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43349 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.key
47891 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
48112 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.key
51763 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51976 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.key
56904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57153 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.key
61262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61498 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.key
65048 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65251 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.key
68842 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69054 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.key
72466 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72685 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.key
76351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76624 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.key
80169 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
80395 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.key
83931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84165 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.key
87666 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88017 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.key
91342 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91598 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.key
95186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1343981 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro
1343983 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro
492 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
523 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
558 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.key
16357 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
16585 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.key
23521 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23799 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.key
30180 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30401 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.key
46941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47243 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.key
61867 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
62293 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.key
76552 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76998 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.key
88518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88799 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.key
96839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97134 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.key
102464 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
102731 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.key
107217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
107502 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.key
113892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
114183 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.key
121350 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
121694 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.key
128131 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128502 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.key
134208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134472 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.key
139735 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139985 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.key
144057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144305 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.key
151124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1495630 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro
1495631 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro
503 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
530 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
572 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
13127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
13311 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
17711 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17878 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.key
21803 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21978 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.key
26016 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26247 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.key
30074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30257 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.key
34314 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34503 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.key
38427 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38634 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.key
42493 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
42684 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.key
47387 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47669 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.key
53649 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
53894 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.key
57846 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58069 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.key
61718 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61926 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.key
65802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66034 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.key
69756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
69984 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.key
73600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73809 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.key
77508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77725 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.key
81380 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81618 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.key
85226 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85458 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.key
89027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89290 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.key
92825 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93085 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.key
96754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
97008 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.key
100646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100906 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.key
104722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104991 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.key
108853 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109225 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.key
112851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113114 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.key
116947 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117280 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.key
120860 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121216 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.key
124876 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125166 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.key
128821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
129110 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.key
132612 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1628770 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro
1628778 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro
535 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
581 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
639 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.key
13569 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13737 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.key
19678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19851 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.key
24746 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24949 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.key
29522 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29726 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.key
33788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33954 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.key
51990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52254 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.key
56683 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56885 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.key
86752 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
87058 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.key
116391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
116767 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.key
138242 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138602 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.key
153701 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
153995 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.key
157967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
158231 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.key
162580 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
162850 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.key
166992 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
167228 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.key
172009 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
172257 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.key
176078 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
176321 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.key
182166 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1811480 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro
1811481 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro
455 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
477 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
525 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.key
23261 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23510 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.key
28282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28463 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.key
33062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33239 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.key
37601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37791 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.key
85006 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85353 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.key
140267 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
140607 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.key
149116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
149362 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.key
168299 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
168572 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.key
191633 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2003651 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro
2003653 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro
456 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
482 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
512 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.m.key
47015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47319 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.m.key
51643 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51953 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.m.key
55991 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56217 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.m.key
60256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60464 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.m.key
64206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64404 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__secure_voting()).Non-interference contract.0.m.key
80183 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2084354 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro
2084356 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro
458 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
476 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
516 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.m.key
14145 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2098946 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro
2098947 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro
475 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
492 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
532 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key
17506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17754 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key
92237 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92664 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.m.key
97473 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97852 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.m.key
101890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102094 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.m.key
106172 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106390 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.m.key
321726 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
322219 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key
328757 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
329328 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key
351425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
351807 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.m.key
356195 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
356500 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.m.key
360382 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
360625 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.m.key
364446 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2463841 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro
2463842 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_fullmacro
517 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
524 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
574 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.m.key
13441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13650 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.m.key
18584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18790 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.m.key
24157 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24388 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.m.key
29564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29868 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.m.key
35192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35453 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.m.key
41089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41368 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.m.key
54917 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
55316 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.m.key
60418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60803 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.m.key
66524 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66869 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.m.key
71217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71551 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.m.key
75626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75884 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.m.key
79855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80133 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.m.key
84423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
84671 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.m.key
88791 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89111 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.m.key
93367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93674 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.m.key
103899 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104269 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.m.key
109815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2574334 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro
2574336 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro
507 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
528 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
556 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.m.key
18849 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19041 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.m.key
24138 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24349 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.m.key
28783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29103 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.m.key
33193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.m.key
37421 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37647 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.m.key
43581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43789 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.m.key
47789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48011 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.m.key
52752 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
52988 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.m.key
56755 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57023 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.m.key
61747 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62008 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.m.key
66135 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66382 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.m.key
70098 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70385 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.m.key
73964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74283 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.m.key
77967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78198 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.m.key
82059 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82313 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.m.key
86054 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
86311 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.m.key
90157 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90449 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.m.key
94090 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94343 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.m.key
97795 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98079 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.m.key
101773 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2676624 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro
2676625 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro
436 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
465 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
502 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.m.key
19894 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
20166 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.m.key
26423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26691 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.m.key
32594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32821 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.m.key
356025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
356417 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.m.key
367450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
367870 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.m.key
378134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
378509 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.m.key
387389 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
387737 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.m.key
395326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
395621 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.m.key
403595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
403874 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.m.key
410090 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
410392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.m.key
416721 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
417053 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.m.key
423974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
424325 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.m.key
430380 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
430734 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.m.key
435882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
436155 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.m.key
440947 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
441212 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.m.key
445164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
445421 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.m.key
451092 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3128274 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro
3128275 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro
453 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
491 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
546 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
14519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14689 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
19716 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19920 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.m.key
24110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24297 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.m.key
28506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28682 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.m.key
32746 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32941 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.m.key
37326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37583 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.m.key
41662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41905 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.m.key
45797 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
46011 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.m.key
50366 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
50593 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.m.key
56793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
57031 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.m.key
60832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61134 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.m.key
64878 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65112 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.m.key
69051 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69302 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.m.key
73262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
73520 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.m.key
77196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77432 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.m.key
81228 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81472 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.m.key
85204 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85464 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.m.key
89295 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89535 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.m.key
93209 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93475 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.m.key
97132 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97389 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.m.key
101000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
101265 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.m.key
104994 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105273 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.m.key
109050 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109354 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.m.key
113154 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113448 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.m.key
117193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117487 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.m.key
121469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121760 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.m.key
125630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126014 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.m.key
129991 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130310 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.m.key
134122 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
134427 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.m.key
138135 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3266966 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro
3266967 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro
564 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
617 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
672 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.m.key
14843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15017 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.m.key
21313 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21518 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.m.key
26457 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
26664 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.m.key
31550 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31791 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.m.key
36289 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36552 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).Non-interference contract.0.m.key
57646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57987 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.m.key
70802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71161 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.m.key
75851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76161 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.m.key
122486 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
123007 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.0.m.key
144228 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144664 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).Non-interference contract.0.m.key
165357 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
165727 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.m.key
209819 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
210219 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.m.key
227841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
228277 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.m.key
244343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
244633 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.m.key
248941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
249257 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.m.key
253715 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
254012 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.m.key
258286 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
258568 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.m.key
262978 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
263269 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.m.key
267328 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
267609 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.m.key
273553 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3541114 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro
3541117 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro
562 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
589 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
624 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.m.key
21740 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21978 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).Non-interference contract.0.m.key
31067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31350 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.m.key
36028 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36303 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.m.key
40781 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
40990 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.m.key
45528 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45728 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.m.key
111739 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112222 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.m.key
180953 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
181392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).Non-interference contract.0.m.key
187523 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
187936 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.m.key
193573 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
193872 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.m.key
222629 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
223043 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.m.key
254902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3796698 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro