537 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting
349 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
356 WARN main d.u.i.k.s.ProofSettings No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
at java.base/java.io.FileInputStream.open0(Native Method)
364 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).JML normal_behavior operation contract.0.key
9281 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9427 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).JML normal_behavior operation contract.0.key
12373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12489 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__isValid(int)).JML normal_behavior operation contract.0.key
15297 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15413 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).JML normal_behavior operation contract.0.key
18138 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18256 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__inputVote()).JML normal_behavior operation contract.0.key
20988 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21139 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__secure_voting()).JML normal_behavior operation contract.0.key
24408 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25360 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting
25366 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential
330 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.
351 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ConditionalConfidential/CCExample(CCExample__hasAccessRight(CCExample.User)).JML normal_behavior operation contract.0.key
10452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10672 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ConditionalConfidential/CCExample(CCExample__getConfidentialData(CCExample.User)).JML normal_behavior operation contract.0.key
14072 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39746 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential
39748 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample
397 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
411 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
420 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/Sum/SumExample(SumExample__getSum()).JML normal_behavior operation contract.0.key
9351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49395 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample
49396 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking
336 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
342 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key
338 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
10416 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10544 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key
36551 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36765 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key
45221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45391 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key
48655 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48802 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).JML normal_behavior operation contract.0.key
51827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51962 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).JML normal_behavior operation contract.0.key
54967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55100 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).JML normal_behavior operation contract.0.key
64450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64655 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key
67875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68041 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key
91748 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91991 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key
99237 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
99433 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key
102407 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102564 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).JML normal_behavior operation contract.0.key
105383 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105537 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).JML normal_behavior operation contract.0.key
108343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108498 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.Bank(banking_example2.Bank__login(int,(C)).JML normal_behavior operation contract.0.key
114199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163941 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking
163945 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts
360 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
373 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
379 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).JML operation contract.0.key
8990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9127 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).JML operation contract.0.key
12584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12697 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).JML operation contract.0.key
15910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16039 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).JML operation contract.0.key
19182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19395 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).JML operation contract.0.key
22619 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22765 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).JML operation contract.0.key
26000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26152 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).JML operation contract.0.key
29348 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29504 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).JML operation contract.0.key
32676 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32877 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).JML operation contract.0.key
35985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36170 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).JML operation contract.0.key
39092 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39249 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).JML operation contract.0.key
42176 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42336 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).JML operation contract.0.key
45236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).JML operation contract.0.key
48345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48501 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).JML operation contract.0.key
51444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51619 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).JML operation contract.0.key
54519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54686 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).JML operation contract.0.key
58113 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58290 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).JML operation contract.0.key
61404 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
225784 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts
225787 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts
357 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
363 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
367 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).JML normal_behavior operation contract.0.key
9527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9641 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).JML normal_behavior operation contract.0.key
13024 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13140 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).JML operation contract.0.key
16276 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16398 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).JML normal_behavior operation contract.0.key
19305 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19422 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).JML operation contract.0.key
22296 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22423 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param_helper()).JML normal_behavior operation contract.0.key
25265 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25460 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).JML operation contract.0.key
28408 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28551 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n9()).JML normal_behavior operation contract.0.key
31365 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31492 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).JML operation contract.0.key
34311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34533 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).JML operation contract.0.key
37452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37645 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).JML normal_behavior operation contract.0.key
40484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40640 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).JML operation contract.0.key
43531 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43684 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).JML operation contract.0.key
46579 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46738 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).JML operation contract.0.key
49527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49677 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).JML normal_behavior operation contract.0.key
52463 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52615 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).JML normal_behavior operation contract.0.key
55393 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55547 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).JML operation contract.0.key
58306 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58517 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).JML operation contract.0.key
61245 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61460 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).JML operation contract.0.key
64215 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64381 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).JML normal_behavior operation contract.0.key
67119 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67317 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).JML normal_behavior operation contract.0.key
70107 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70279 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).JML operation contract.0.key
73032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
299169 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts
299171 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants
357 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
368 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
375 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key
10033 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10177 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).JML operation contract.0.key
14095 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14221 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).JML operation contract.0.key
17937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18058 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).JML operation contract.0.key
22216 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22374 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).JML operation contract.0.key
26373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26534 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).JML operation contract.0.key
30562 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30724 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).JML operation contract.0.key
34600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34799 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).JML operation contract.0.key
38339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38498 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).JML operation contract.0.key
41772 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41980 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).JML operation contract.0.key
45202 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45367 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).JML operation contract.0.key
48817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48985 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).JML operation contract.0.key
52408 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52569 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).JML operation contract.0.key
55982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56149 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).JML operation contract.0.key
59335 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59501 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).JML operation contract.0.key
62719 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62880 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).JML normal_behavior operation contract.0.key
65958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66122 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).JML normal_behavior operation contract.0.key
69508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
369010 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants
369011 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples
339 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.
350 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
9217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9325 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
12501 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12611 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).JML normal_behavior operation contract.0.key
15575 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15699 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).JML normal_behavior operation contract.0.key
18543 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18694 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).JML normal_behavior operation contract.0.key
21482 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21604 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).JML normal_behavior operation contract.0.key
24410 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24544 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).JML normal_behavior operation contract.0.key
27331 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27508 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).JML normal_behavior operation contract.0.key
30258 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30391 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.1.key
33282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33423 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.0.key
36302 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36441 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).JML normal_behavior operation contract.0.key
39179 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39332 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).JML operation contract.0.key
42092 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42248 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).JML normal_behavior operation contract.0.key
45036 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45193 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).JML normal_behavior operation contract.0.key
47938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48091 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).JML normal_behavior operation contract.0.key
50810 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50962 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).JML normal_behavior operation contract.0.key
53691 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53848 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).JML normal_behavior operation contract.0.key
56598 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56754 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).JML normal_behavior operation contract.0.key
59450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59611 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).JML normal_behavior operation contract.0.key
62310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62475 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).JML normal_behavior operation contract.0.key
65184 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).JML normal_behavior operation contract.0.key
68075 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68248 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).JML normal_behavior operation contract.0.key
70923 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71096 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).JML normal_behavior operation contract.0.key
73802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73983 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).JML normal_behavior operation contract.0.key
76654 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76843 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).JML normal_behavior operation contract.0.key
79507 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79696 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).JML normal_behavior operation contract.0.key
82348 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82539 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.1.key
85190 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85380 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.0.key
88017 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88212 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).JML normal_behavior operation contract.0.key
90866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91090 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).JML normal_behavior operation contract.0.key
93738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
463101 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples
463103 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects
355 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.
389 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).JML operation contract.0.key
9783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9904 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).JML normal_behavior operation contract.0.key
13665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13796 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.1.key
17175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17298 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.0.key
20460 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20589 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).JML normal_behavior operation contract.0.key
23600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23724 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).JML operation contract.0.key
28106 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28339 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).JML operation contract.0.key
31889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32077 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).JML operation contract.0.key
35031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35180 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.1.key
38916 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39093 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.0.key
42804 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42973 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).JML operation contract.0.key
46618 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46870 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).JML operation contract.0.key
50265 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50433 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).JML normal_behavior operation contract.0.key
53638 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53796 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.1.key
56677 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56840 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.0.key
59771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59935 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).JML operation contract.0.key
62935 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63110 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).JML operation contract.0.key
66128 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66302 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).JML operation contract.0.key
69288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69545 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML accessible clause.0.key
72445 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72620 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML normal_behavior operation contract.0.key
75528 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75768 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).JML normal_behavior operation contract.0.key
78834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
542369 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects
542371 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
379 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
392 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
396 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/PasswordFile/passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
8558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
551187 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
551189 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting
352 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
376 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
383 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).JML normal_behavior operation contract.0.key
10925 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11102 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage((B)).JML normal_behavior operation contract.0.key
15237 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15376 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).JML normal_behavior operation contract.0.key
19985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20187 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).JML normal_behavior operation contract.0.key
23620 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23814 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).JML normal_behavior operation contract.0.key
27182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
27314 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).JML normal_behavior operation contract.0.key
30677 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30815 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment___rep()).JML accessible clause.0.key
34115 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34257 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.1.key
46343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46546 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.0.key
57728 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57942 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Message(java.lang.Object___inv_()).JML accessible clause.0.key
61337 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61502 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML accessible clause.0.key
66074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66261 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML normal_behavior operation contract.0.key
70120 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70302 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onSendResult()).JML normal_behavior operation contract.0.key
73637 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73805 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.1.key
77149 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77321 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.0.key
81053 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81296 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Server(java.lang.Object___inv_()).JML accessible clause.0.key
84608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84793 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key
88227 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88425 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key
91658 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91841 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__publishResult()).JML normal_behavior operation contract.0.key
95549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95742 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).JML normal_behavior operation contract.0.key
131796 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
132074 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Setup(java.lang.Object___inv_()).JML accessible clause.0.key
138771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138994 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.1.key
146228 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146488 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.0.key
156495 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156751 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(java.lang.Object___inv_()).JML accessible clause.0.key
160003 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
711560 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting
711561 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro
322 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
328 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
334 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.key
20542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
20750 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.key
23882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24010 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.key
27165 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27308 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.key
30247 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30391 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.key
33215 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
745086 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro
745087 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro
745087 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro
745089 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro
347 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
351 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.key
10991 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
756400 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro
756401 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro
345 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
352 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
355 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.key
11930 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12081 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.key
16465 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16616 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.key
19965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20109 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.key
23369 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23514 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.key
64336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
64601 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.key
69007 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69180 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.key
72748 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72908 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.key
75876 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76038 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.key
79037 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
835752 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro
835753 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro
376 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
372 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
382 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.key
9872 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10022 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.key
13625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13821 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.key
18150 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18330 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.key
22316 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22491 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.key
26552 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26767 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.key
31444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31655 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.key
36175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36412 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.key
40824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41068 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.key
45780 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46046 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.key
49191 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.key
52352 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52530 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.key
55512 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55717 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.key
58810 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
59001 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.key
62171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62376 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.key
65710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65900 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.key
71209 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71432 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.key
76269 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
912398 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro
912401 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro
356 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
363 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
369 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.key
12444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12608 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.key
15992 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16121 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.key
19354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19482 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.key
22462 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22585 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.key
25539 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25672 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.key
29395 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29566 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.key
32514 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32664 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.key
36108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36305 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.key
39088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39237 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.key
43044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43215 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.key
46478 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46652 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.key
49524 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49682 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.key
52549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52704 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.key
55440 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55596 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.key
58536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58715 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.key
61580 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
61750 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.key
64616 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64833 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.key
67599 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67768 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.key
70507 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70677 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.key
73508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
986260 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro
986261 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro
323 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
334 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
340 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.key
11949 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
12142 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.key
17235 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17381 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.key
22107 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22268 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.key
34373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34609 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.key
45421 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45648 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.key
56066 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56280 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.key
64590 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64809 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.key
70832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71031 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.key
75088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
75275 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.key
78768 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
78922 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.key
83879 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
84064 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.key
89481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
89678 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.key
94514 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94705 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.key
98932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99128 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.key
103148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103337 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.key
106427 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106590 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.key
111501 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1098142 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro
1098144 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro
334 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.
348 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
8889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9013 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key
12216 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12335 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.key
15213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15365 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.key
18224 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18358 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.key
21141 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21304 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.key
24229 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24365 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.key
27269 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.key
30162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30340 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.key
33824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33981 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.key
38683 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
38854 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.key
41690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41889 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.key
44505 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44659 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.key
47479 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47637 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.key
50344 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
50506 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.key
53110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53305 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.key
56049 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56213 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.key
58921 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59101 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.key
61770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61930 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.key
64493 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64663 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.key
67233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67404 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.key
69986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
70177 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.key
72842 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73023 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.key
75801 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75986 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.key
78797 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79023 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.key
81682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81871 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.key
84651 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84867 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.key
87493 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87688 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.key
90340 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90550 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.key
93189 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
93436 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.key
95972 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1194504 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro
1194505 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro
338 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.
353 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.key
9369 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9484 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.key
13977 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14118 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.key
17876 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18010 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.key
21671 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21823 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.key
24970 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25098 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.key
37560 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37752 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.key
41205 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41350 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.key
63249 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
63462 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.key
84944 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
85154 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.key
101213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101428 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.key
112947 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
113145 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.key
116305 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
116519 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.key
119972 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120149 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.key
123385 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123553 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.key
127253 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127434 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.key
130434 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130604 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.key
135044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1329927 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro
1329928 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro
391 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
392 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
405 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.key
17350 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17634 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.key
21170 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21297 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.key
24796 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24953 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.key
28353 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
28489 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.key
58971 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59224 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.key
94492 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94750 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.key
100672 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100849 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.key
114228 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.key
130239 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1460560 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro
1460561 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro
336 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.
347 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.m.key
8218 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
34469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34671 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.m.key
37590 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37825 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38011 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.m.key
40848 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
41150 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41277 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.m.key
43964 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
44224 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44378 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.m.key
47131 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
47260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47399 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyVoting/Voter(Voter__secure_voting()).Non-interference contract.0.m.key
50076 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
58509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1519424 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro
1519425 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro
321 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
331 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
342 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.m.key
8427 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
10253 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1529953 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro
1529955 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro
389 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
400 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
404 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key
8873 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13426 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key
16613 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
67726 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68001 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.m.key
70902 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
71455 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71641 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.m.key
74790 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
74965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75111 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.m.key
77945 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
78084 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78232 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.m.key
81148 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
228694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
228992 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key
231656 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
233542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
233713 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key
236422 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
249181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
249396 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.m.key
252134 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
252660 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
252836 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.m.key
255524 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
255652 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
255811 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.m.key
258482 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
258608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1788898 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro
1788899 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_fullmacro
398 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
411 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/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.m.key
8630 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9675 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9796 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.m.key
12802 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13482 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13648 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.m.key
16460 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
17987 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
18144 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.m.key
20914 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
21992 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22166 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.m.key
24863 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25978 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26165 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.m.key
28828 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30245 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.m.key
33111 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
40098 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
40350 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.m.key
43005 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
44175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44422 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.m.key
47021 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48324 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48540 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.m.key
51126 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
51596 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51813 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.m.key
54446 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
54800 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54990 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.m.key
57578 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
57909 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58101 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.m.key
60671 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
61202 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
61410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.m.key
64009 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
64433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64627 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.m.key
67221 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
67726 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67916 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.m.key
70493 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
74938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75163 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.m.key
77687 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
79141 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1868433 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro
1868435 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro
354 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.
361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.m.key
8303 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
12465 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12595 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.m.key
15723 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
16358 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16496 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.m.key
19461 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19883 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.m.key
22864 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
23025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23151 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.m.key
26079 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
26301 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26456 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.m.key
29312 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31132 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.m.key
33934 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
34134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34274 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.m.key
37082 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37956 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.m.key
40710 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
40827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40974 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.m.key
43749 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
44608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44777 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.m.key
47557 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48037 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48222 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.m.key
50985 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
51188 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51340 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.m.key
54126 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
54268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54438 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.m.key
57175 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
57276 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57435 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.m.key
60170 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
60489 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60660 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.m.key
63375 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
63667 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
63836 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.m.key
66553 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
66880 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67044 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.m.key
69745 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
69859 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70028 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.m.key
72726 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
72817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72987 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.m.key
75727 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
75965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1944763 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro
1944764 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro
353 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
356 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
360 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.m.key
8812 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14095 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14222 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.m.key
17486 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18898 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19035 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.m.key
22174 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
23367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23510 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.m.key
26576 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
246377 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
246556 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.m.key
249600 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
254280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
254441 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.m.key
257483 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
261768 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
261912 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.m.key
264909 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
268312 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
268468 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.m.key
271494 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
273904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
274057 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.m.key
277050 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
279601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
279763 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.m.key
282713 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
284350 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
284517 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.m.key
287490 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
289164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
289319 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.m.key
292282 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
294435 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
294612 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.m.key
297536 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
298960 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
299129 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.m.key
302087 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
302992 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
303161 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.m.key
306140 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
306862 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
307024 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.m.key
309918 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
310000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
310163 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.m.key
313070 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
314325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2259409 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro
2259410 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro
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.
350 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
8329 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9681 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key
12617 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
12912 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13034 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.m.key
15807 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
15922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16042 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.m.key
18770 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19108 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.m.key
21799 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
21948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22117 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.m.key
24814 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
25269 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.m.key
27932 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
28121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28301 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.m.key
30905 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
31060 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31199 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.m.key
33834 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
34433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
34635 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.m.key
37239 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
38873 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
39024 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.m.key
41623 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
41866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42057 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.m.key
44602 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
44725 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44881 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.m.key
47435 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
47662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47822 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.m.key
50399 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
50648 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
50819 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.m.key
53356 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
53435 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53600 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.m.key
56118 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
56238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56401 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.m.key
58940 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
59065 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59233 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.m.key
61744 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
61841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62041 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.m.key
64537 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
64627 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64800 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.m.key
67354 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
67437 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67617 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.m.key
70105 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
70261 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
70435 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.m.key
72924 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
73062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73239 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.m.key
75713 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
75965 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76192 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.m.key
78667 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
78871 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79061 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.m.key
81545 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
81665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81854 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.m.key
84327 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
84549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84753 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.m.key
87229 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
87407 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87604 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.m.key
90056 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
90208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90417 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.m.key
92906 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
93171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
93405 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.m.key
95869 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
95997 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2355789 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro
2355790 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro
348 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.
360 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.m.key
8538 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
9370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9493 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.m.key
12707 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13709 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13847 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.m.key
16880 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
17483 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
17651 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.m.key
20557 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
20996 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21148 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.m.key
24063 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24314 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).Non-interference contract.0.m.key
27199 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
38721 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38923 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.m.key
41788 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
47437 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47624 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.m.key
50454 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
50875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51039 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.m.key
53886 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
82977 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
83200 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.0.m.key
86055 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
98147 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98349 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).Non-interference contract.0.m.key
101166 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
112927 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113134 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.m.key
115904 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
143816 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
144024 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.m.key
146776 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
156268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156477 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.m.key
159280 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
167445 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
167659 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.m.key
170431 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
170633 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
170805 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.m.key
173558 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
173968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
174146 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.m.key
176920 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
177183 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177375 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.m.key
180176 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
180526 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
180714 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.m.key
183516 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
183595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183865 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.m.key
186612 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
188071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2544271 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro
2544272 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro
386 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.
399 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.m.key
9072 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14261 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14403 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).Non-interference contract.0.m.key
18017 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
20694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20863 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.m.key
24237 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24309 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24500 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.m.key
27819 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
27926 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
28060 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.m.key
31388 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
31490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31632 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.m.key
34926 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
77052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77308 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.m.key
80525 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
124774 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125035 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).Non-interference contract.0.m.key
128259 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
129650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129809 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.m.key
133074 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
134123 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134304 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.m.key
137587 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
154413 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154621 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.m.key
157843 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
176800 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2721445 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro
2721485 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total rule apps.sum.properties is written
2721490 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total rule apps.avg.properties is written
2721491 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Nodes.sum.properties is written
2721493 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Nodes.avg.properties is written
2721493 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Branches.sum.properties is written
2721493 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Branches.avg.properties is written
2721493 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Overall time (ms).sum.properties is written
2721494 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Overall time (ms).avg.properties is written
2721494 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Automode time (ms).sum.properties is written
2721494 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Automode time (ms).avg.properties is written
2721494 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Closed.sum.properties is written
2721495 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Closed.avg.properties is written
2721495 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Time per step (ms).sum.properties is written
2721495 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Time per step (ms).avg.properties is written
2721495 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total Runtime Memory (kB).sum.properties is written
2721496 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/Total Runtime Memory (kB).avg.properties is written
2721497 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/../../key.core/build/reports/runallproofs/NumberTestFiles.properties is written