240 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting
351 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
364 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)
389 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
9294 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9432 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
12318 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12447 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
15312 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15441 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
18181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18308 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyVoting/Voter(Voter__inputVote()).JML normal_behavior operation contract.0.key
21066 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21192 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
24710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25365 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting
25383 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential
315 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
339 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
378 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
10057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10245 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
13625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39340 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential
39342 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample
327 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
345 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
371 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/Sum/SumExample(SumExample__getSum()).JML normal_behavior operation contract.0.key
10238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49889 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample
49891 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking
392 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
408 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
455 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
10056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10205 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
36551 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36798 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
45322 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45519 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
48848 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49009 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
52074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52222 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
55273 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55423 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
64811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65038 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
68268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68447 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key
92002 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92264 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
99588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
99798 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
102904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103099 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
105959 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106129 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
108984 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109160 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
114863 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
165138 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking
165139 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts
348 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
354 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
389 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).JML operation contract.0.key
9163 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9289 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
12577 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12730 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
16129 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16264 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
19398 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19552 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
22741 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22903 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
26065 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26232 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
29402 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29569 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
32798 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32977 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
36001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36232 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
39133 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39352 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
42196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42361 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
45240 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45420 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
48200 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48380 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
51221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51401 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
54278 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54458 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
57718 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57941 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
61013 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
226531 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts
226534 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts
336 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
347 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
382 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
9108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9240 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
12558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12702 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
15932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16114 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
19135 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19301 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
22308 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22452 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
25344 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25478 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
28413 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28558 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
31444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31588 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
34460 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34614 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
37613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37779 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
40644 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40842 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
43803 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43970 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
46882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47054 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
49875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50052 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
52878 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53055 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
55878 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56060 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
58895 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59074 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
61864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62046 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
64847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65031 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
67817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67998 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
70800 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70984 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
73781 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
300751 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts
300756 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants
337 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
344 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
366 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key
9955 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10121 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
13911 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14055 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
17591 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17733 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
21734 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21910 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
25811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25977 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
29815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30012 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
33776 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33943 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
37361 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37532 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
40785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40935 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
44061 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
44226 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
47520 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47709 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
50987 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51170 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
54453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54681 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
57764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57951 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
61032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61215 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
64220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64385 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
67535 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
368653 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants
368655 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples
389 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
396 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
427 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
8767 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
8897 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
12124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12243 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
15298 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15420 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
18424 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18550 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
21335 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21469 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
24275 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24412 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
27199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27336 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
30074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30213 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
33071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33221 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
36079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36245 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
38963 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39125 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
41853 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42009 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
44707 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44863 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
47564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47737 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
50420 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50588 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
53267 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53458 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
56139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56386 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
59043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59223 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
61873 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62050 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
64715 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64899 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
67575 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67765 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
70411 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70608 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
73278 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73486 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
76158 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76357 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
78991 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79226 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
81874 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82086 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
84736 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84946 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
87575 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87792 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
90442 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90656 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
93317 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
462373 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples
462374 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects
335 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
343 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
366 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
9240 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9365 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
13599 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13739 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
17244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17377 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
20630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20803 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
23943 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24079 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
28617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28817 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
32314 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32507 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
35665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35812 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
39693 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39918 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
43770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43972 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
47754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47958 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
51486 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51693 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
54983 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55174 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
58179 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58349 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
61344 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61529 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
64621 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64847 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
67948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68141 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
71215 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71416 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
74411 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74603 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
77579 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77772 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
80936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81210 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
84024 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
546799 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects
546801 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting
320 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
348 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
387 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).JML normal_behavior operation contract.0.key
11499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11689 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
16008 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16153 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
21055 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21233 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
24801 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24973 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
28523 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
28669 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
32145 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32298 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
35774 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35932 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
48256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48485 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
59909 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60137 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
63678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63853 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
68584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68793 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
72766 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72965 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
76450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76635 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
80081 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80278 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
84159 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84360 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
87817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88011 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
91599 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91813 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
95166 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95369 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
99222 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99449 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
136096 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
136405 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
143186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143545 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
150774 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151045 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
161126 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161405 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
164776 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
711969 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting
711970 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro
337 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
346 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
368 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
21760 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
21989 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
25203 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25457 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
28650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28801 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
31824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31967 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
34826 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
747097 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro
747098 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro
747099 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro
747102 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro
369 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
399 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
419 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
11930 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
759629 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro
759631 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro
335 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
347 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
381 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
12382 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12566 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
16715 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16949 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
20304 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20459 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
23772 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23970 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
63090 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
63384 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
67813 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68126 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
71713 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71886 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
74917 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75083 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
78167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
838141 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro
838142 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro
340 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
345 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
367 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.key
9734 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9876 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
13634 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13818 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
18316 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18492 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
22594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22790 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
27040 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27330 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
32142 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32376 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
37271 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37535 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
42144 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42425 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
47348 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47622 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
50944 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51180 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
54375 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54576 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
57722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58046 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
61259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
61470 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
64797 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65014 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
68431 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68684 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
74156 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74400 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
79420 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
917978 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro
917979 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro
324 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
332 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
354 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
11845 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12059 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
15494 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15627 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
18895 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19039 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
21980 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22120 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
25036 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25181 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
28800 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28956 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
31822 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31991 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
35476 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
35651 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
38439 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38605 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
42367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42561 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
45662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45831 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
48615 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48786 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
51579 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51754 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
54450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54636 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
57516 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57745 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
60555 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
60736 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
63504 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63776 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
66519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66699 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
69343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69526 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
72272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
990619 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro
990624 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro
332 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
341 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
381 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
12037 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
12255 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
17348 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17547 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
22200 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22362 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
34592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34823 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
45775 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
46128 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
56611 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56960 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
65162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65398 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
71377 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71589 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.key
75730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
75934 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
79286 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
79483 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
84342 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
84574 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
89825 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
90088 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
94861 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95153 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
99230 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99465 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
103365 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103569 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
106622 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106799 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
111642 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1102659 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro
1102660 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro
346 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
364 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
389 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
9233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9357 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
12768 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12898 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
15885 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16008 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
18954 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19098 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
22042 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22205 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
25196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
25340 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
28192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28343 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
31072 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31226 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
34681 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34890 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
39453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
39636 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
42526 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42739 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
45471 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45646 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
48529 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48747 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
51537 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
51718 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
54379 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54552 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
57335 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57516 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
60269 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/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.key
63115 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63300 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
65923 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66108 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
68769 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68958 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
71591 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
71793 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
74495 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74698 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
77539 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77746 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
80568 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80851 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
83455 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83664 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
86520 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86749 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
89447 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89659 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
92384 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92618 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
95319 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
95542 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
98208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1201259 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro
1201263 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro
379 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
390 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
427 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.key
10021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10173 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
14500 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14652 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
18250 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18405 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
21875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22033 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
24998 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25148 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
37897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38116 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
41462 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41623 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
62634 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
62885 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
83267 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
83583 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
98804 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99088 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
109903 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
110120 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
113136 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
113337 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
116627 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116826 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
119924 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120107 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
123687 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123884 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
126731 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126915 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
131173 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1332819 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro
1332820 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro
351 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
358 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
385 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.key
18743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18955 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
22956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23098 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
26782 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
26942 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
30499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30751 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
61978 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62264 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
99053 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99323 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
105563 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105761 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
119491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119708 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
136019 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1469280 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro
1469282 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro
367 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
381 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
419 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
34550 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34772 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
37770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38017 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
41019 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41178 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
44172 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44330 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
47110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47256 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
58382 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1528078 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro
1528080 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro
359 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
377 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
416 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
10745 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1539159 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro
1539160 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro
374 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
387 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
426 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
13603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13806 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
69601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69936 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.m.key
73561 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73827 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
76902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77066 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
80112 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80286 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.m.key
231294 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
231676 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
236307 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
236764 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
252349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
252637 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
255942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
256182 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
259085 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
259271 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
262176 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1801681 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro
1801682 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_fullmacro
357 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
361 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
384 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
9942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10122 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
13739 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13911 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
18208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18377 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
22311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22535 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
26575 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26784 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
30964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31198 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
41274 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41581 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
45458 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45747 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
49733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50009 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
53151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53387 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
56426 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56633 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
59677 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59902 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
63111 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
63329 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
66453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66697 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
69862 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70090 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.m.key
77352 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77636 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
81755 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1883877 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro
1883878 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro
369 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
377 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
404 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
13126 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13330 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
16907 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_catch_exception()).Non-interference contract.0.m.key
20258 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20424 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
23322 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23475 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
26346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26554 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
30662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30832 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
33599 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33794 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
37127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37395 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
40155 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40470 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
44372 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44597 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
47692 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47913 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
50668 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50871 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
53558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53750 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
56385 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56578 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
59438 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59669 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
62484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
62666 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
65449 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65721 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
68348 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68550 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
71160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71361 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
74070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1958364 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro
1958365 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro
336 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
357 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
396 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
14556 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14746 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
19415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19628 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
24022 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24210 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
259700 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
260001 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
267967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
268293 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
275695 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
275987 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
282499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
282779 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
288314 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
288528 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
294090 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
294311 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
298937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
299195 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
303922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
304183 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
309431 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
309698 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
314133 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
314420 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
318332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
318549 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
322208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
322441 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
325447 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
325642 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
329847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2288628 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro
2288629 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro
386 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
393 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
415 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
10000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
10208 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
13585 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13743 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
16783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16989 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
20000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20162 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
23091 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23250 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
26448 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
26707 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
29681 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29869 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
32751 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32914 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
36285 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36473 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
40765 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
40968 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
43872 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44077 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
46881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47065 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
49997 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50266 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
53198 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
53405 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
56146 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56366 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
59118 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59340 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
62134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62333 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
65076 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65277 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
67999 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68225 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
70902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71103 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
73840 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
74050 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
76785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77012 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
79856 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80073 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
82920 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83166 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
85847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86077 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
88973 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89260 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
92021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92273 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
95088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95341 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
98155 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
98420 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
101210 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2390281 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro
2390282 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro
382 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
388 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
414 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
9521 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9665 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
13979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14135 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
17678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
17841 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
21276 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21452 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
24481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24635 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
39543 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39795 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
48825 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49137 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
52479 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52664 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
85932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
86210 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
101629 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101970 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
116983 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117275 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
149454 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
149759 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
162453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
162785 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
174124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
174359 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
177311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
177563 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
180699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
180935 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
183962 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
184195 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
187291 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
187521 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
190319 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190531 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
194744 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2585478 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro
2585479 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro
388 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
405 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
428 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
14844 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15070 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
21515 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21724 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.m.key
25241 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25443 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
28871 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29027 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
32454 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32633 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
82529 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82918 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
134383 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134744 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
139453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139761 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
144295 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144515 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
166134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166446 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
190402 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2776411 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro