735 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting
529 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
564 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)
585 INFO 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
11210 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11377 INFO 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
15295 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15484 INFO 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
19427 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19588 INFO 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
23276 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23473 INFO 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
26959 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27116 INFO 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
31842 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33067 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting
33077 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential
502 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
526 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
539 INFO 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
13988 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14207 INFO 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
18342 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51800 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential
51802 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample
468 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
501 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
509 INFO 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
11682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63870 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample
63873 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking
433 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
450 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
455 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key
12938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13112 INFO 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
44083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44358 INFO 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
54807 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55035 INFO 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
58972 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59131 INFO 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
62789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62970 INFO 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
66556 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66719 INFO 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
77769 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78013 INFO 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
81995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82200 INFO 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
110396 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110689 INFO 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
119969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
120206 INFO 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
123694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123926 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).JML normal_behavior operation contract.0.key
127299 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127480 INFO 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
130908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131111 INFO 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
137910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
202249 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking
202254 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts
525 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
564 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
573 INFO 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
11737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11879 INFO 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
16099 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16261 INFO 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
20405 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20585 INFO 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
24617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24818 INFO 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
28646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28825 INFO 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
32851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33044 INFO 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
37072 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37341 INFO 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
41372 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41589 INFO 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
45460 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45679 INFO 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
49125 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49313 INFO 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
52452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52642 INFO 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
55762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55940 INFO 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
59140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59373 INFO 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
62708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62915 INFO 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
66164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66359 INFO 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
70161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70377 INFO 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
74043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
276730 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts
276736 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts
385 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
401 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
407 INFO 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
11017 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11169 INFO 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
15048 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15195 INFO 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
18975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19152 INFO 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
22483 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22637 INFO 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
26111 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26283 INFO 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
29661 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29861 INFO 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
33631 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33801 INFO 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
37539 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37732 INFO 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
41479 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41680 INFO 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
45477 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45665 INFO 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
49400 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49618 INFO 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
53537 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53756 INFO 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
57434 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57661 INFO 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
61332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61538 INFO 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
65133 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65335 INFO 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
68886 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69094 INFO 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
72689 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72906 INFO 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
76456 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76687 INFO 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
80199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80425 INFO 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
84032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84272 INFO 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
87730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87955 INFO 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
91487 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
368666 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts
368669 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants
523 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
541 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
552 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key
13759 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13965 INFO 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
19272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19446 INFO 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
24414 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24602 INFO 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
29956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30149 INFO 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
35155 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35361 INFO 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
40487 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40690 INFO 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
45572 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45844 INFO 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
50373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50565 INFO 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
54699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54872 INFO 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
58991 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
59185 INFO 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
63525 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63766 INFO 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
68022 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68238 INFO 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
72663 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72891 INFO 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
76941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77161 INFO 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
81375 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81603 INFO 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
85670 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85892 INFO 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
90365 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
459518 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants
459520 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples
585 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
594 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
607 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key
13418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13587 INFO main d.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
17860 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18031 INFO main d.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
22088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22239 INFO main d.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
26268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26424 INFO main d.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
30171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30363 INFO main d.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
34077 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34250 INFO main d.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
38187 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38367 INFO main d.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
42025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42194 INFO main d.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
45971 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46153 INFO main d.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
49917 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50103 INFO main d.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
53711 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53899 INFO main d.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
57490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57698 INFO main d.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
61250 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61452 INFO main d.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
64893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65093 INFO main d.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
68441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68681 INFO main d.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
72089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72308 INFO main d.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
75741 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75985 INFO main d.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
79417 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79636 INFO main d.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
83144 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83368 INFO main d.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
86855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87084 INFO main d.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
90553 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90789 INFO main d.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
94161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94390 INFO main d.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
97893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98130 INFO main d.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
101773 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102080 INFO main d.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
105659 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105918 INFO main d.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
109537 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109773 INFO main d.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
113209 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113472 INFO main d.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
117034 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117318 INFO main d.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
120779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121040 INFO main d.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
124523 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
584518 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples
584520 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects
513 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
542 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
552 INFO 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
13095 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13249 INFO 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
18478 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18646 INFO 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
22870 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23035 INFO 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
26990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27162 INFO 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
30890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31056 INFO 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
36887 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37252 INFO 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
41863 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42098 INFO 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
45953 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46147 INFO 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
50889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51138 INFO 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
55778 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56013 INFO 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
60577 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60883 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).JML operation contract.0.key
65384 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65638 INFO 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
69788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70039 INFO 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
73695 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73931 INFO 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
77563 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77820 INFO 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
81762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82076 INFO 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
86032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86270 INFO 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
90007 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90264 INFO 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
93870 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94103 INFO 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
97764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98018 INFO 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
102053 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
687131 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects
687133 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
570 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
590 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
604 INFO 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
12105 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
699639 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key
699640 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting
503 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
518 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
522 INFO 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
14354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14557 INFO 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
20391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20574 INFO 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
27195 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27421 INFO 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
32092 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32366 INFO 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
36813 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37023 INFO 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
41571 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41770 INFO 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
46537 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46776 INFO 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
64256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64551 INFO 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
80678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80947 INFO 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
85484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85684 INFO 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
91986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92216 INFO 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
97341 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97597 INFO 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
101997 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102209 INFO 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
106738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106975 INFO 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
112122 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112402 INFO 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
116900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117157 INFO 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
121749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121986 INFO 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
126296 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126558 INFO 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
131592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131915 INFO 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
181610 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
181984 INFO 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
191192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
191503 INFO 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
201215 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
201564 INFO 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
215436 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
215770 INFO 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
220190 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
920322 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting
920324 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_nomacro
466 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
519 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
530 INFO 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
28778 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29051 INFO 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
33423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33578 INFO 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
37753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37946 INFO 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
41847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42023 INFO 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
45869 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
966599 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_nomacro
966601 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ConditionalConfidential_nomacro
966601 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ConditionalConfidential_nomacro
966605 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_nomacro
452 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
472 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
477 INFO 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
15580 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
982618 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_nomacro
982620 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_nomacro
469 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
493 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
499 INFO 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
17680 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17938 INFO 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
23968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24180 INFO 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
28722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28909 INFO 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
33314 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33503 INFO 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
92153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
92497 INFO 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
98532 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98765 INFO 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
103607 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103844 INFO 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
107921 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108181 INFO 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
112196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1095279 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_nomacro
1095280 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_nomacro
499 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
511 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
523 INFO 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
13753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13952 INFO 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
18834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19114 INFO 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
24844 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
25136 INFO 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
30613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30848 INFO 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
36426 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36688 INFO 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
43033 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
43346 INFO 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
49742 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
50106 INFO 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
56157 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56468 INFO 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
63029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63365 INFO 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
67843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68164 INFO 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
72444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72687 INFO 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
76808 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77056 INFO 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
81386 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
81623 INFO 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
86021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86339 INFO 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
90814 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/BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.key
98283 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98596 INFO 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
105117 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1200926 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_nomacro
1200927 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_nomacro
448 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
460 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
464 INFO 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
16488 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16680 INFO 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
21052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21226 INFO 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
25483 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25658 INFO 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
29469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29638 INFO 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
33239 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33412 INFO 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
38289 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38486 INFO 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
42188 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42384 INFO 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
46664 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
46888 INFO 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
50423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50608 INFO 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
55303 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55538 INFO 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
59415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59670 INFO 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
63167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63387 INFO 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
66896 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67092 INFO 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
70444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70641 INFO 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
74302 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74505 INFO 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
78079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
78325 INFO 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
81868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82091 INFO 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
85517 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85731 INFO 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
89131 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89348 INFO 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
92969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1294355 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_nomacro
1294357 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test LoopInvariants_nomacro
492 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
504 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
508 INFO 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
15465 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
15670 INFO 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
22105 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22314 INFO 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
28296 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28481 INFO 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
43437 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
43708 INFO 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
56907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
57176 INFO 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
69802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70072 INFO 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
80334 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80618 INFO 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
88810 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89077 INFO 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
94426 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
94651 INFO 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
98744 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
98932 INFO 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
104960 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
105189 INFO 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
111610 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
111879 INFO 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
117738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118017 INFO 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
123167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123410 INFO 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
128330 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128573 INFO 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
132372 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
132583 INFO 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
139047 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1433928 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test LoopInvariants_nomacro
1433930 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_nomacro
460 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
498 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
508 INFO main d.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
12709 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
12862 INFO main d.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
17236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17408 INFO main d.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
21068 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21268 INFO main d.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
24985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25209 INFO main d.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
28911 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29150 INFO main d.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
33100 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
33315 INFO main d.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
37057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37282 INFO main d.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
40809 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41006 INFO main d.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
45316 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45566 INFO main d.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
50901 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
51125 INFO main d.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
54865 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55076 INFO main d.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
58607 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58818 INFO main d.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
62504 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62704 INFO main d.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
66186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
66391 INFO main d.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
69829 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70030 INFO main d.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
73387 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73618 INFO main d.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
76905 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77123 INFO main d.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
80307 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80571 INFO main d.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
83767 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84046 INFO main d.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
87239 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87476 INFO main d.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
90603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
90833 INFO main d.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
94177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94409 INFO main d.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
98000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98259 INFO main d.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
101710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102044 INFO main d.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
105287 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105598 INFO main d.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
108942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109188 INFO main d.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
112411 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112671 INFO main d.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
115910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116169 INFO main d.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
119569 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
119848 INFO main d.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
123051 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1557476 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_nomacro
1557478 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_nomacro
497 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
503 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
506 INFO 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
13333 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13478 INFO 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
19151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19331 INFO 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
24007 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24256 INFO 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
28714 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28912 INFO 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
32883 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33056 INFO 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
50442 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50723 INFO 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
55039 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55246 INFO 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
83362 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
83634 INFO 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
110984 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
111257 INFO 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
131910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
132165 INFO 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
146974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
147228 INFO 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
151025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
151244 INFO 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
155402 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
155627 INFO 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
159515 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
159737 INFO 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
164359 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
164602 INFO 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
168175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
168406 INFO 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
173874 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1731854 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_nomacro
1731855 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_nomacro
457 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
487 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
496 INFO 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
22351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22606 INFO 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
27454 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27618 INFO 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
32039 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32255 INFO 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
36634 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
36805 INFO 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
77724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78025 INFO 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
125023 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125366 INFO 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
133108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133350 INFO 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
149824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150104 INFO 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
169690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1902030 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_nomacro
1902032 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyVoting_fullmacro
512 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
537 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
542 INFO 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
10881 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
44776 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45004 INFO 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
48678 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49009 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49156 INFO 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
52479 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
52859 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53112 INFO 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
56303 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
56612 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56791 INFO 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
59974 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
60187 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60362 INFO 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
63534 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
74487 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1976996 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyVoting_fullmacro
1976997 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SumExample_fullmacro
484 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
511 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
516 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/Sum/SumExample(SumExample__getSum()).Non-interference contract.0.m.key
11428 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
14020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1991366 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SumExample_fullmacro
1991368 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ToyBanking_fullmacro
451 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
476 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
487 INFO 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
12033 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
17786 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17986 INFO 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
22155 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
86548 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86846 INFO 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
90565 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
91280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91542 INFO 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
95171 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
95347 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95525 INFO 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
99128 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
99303 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99475 INFO 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
103071 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
284520 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
284893 INFO 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
288263 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
290679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
290893 INFO 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
294403 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
310698 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
310965 INFO 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
314348 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
314953 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
315179 INFO 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
318620 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
318826 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
319026 INFO 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
322514 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
322680 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2314470 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ToyBanking_fullmacro
2314471 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test BlockContracts_fullmacro
526 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
540 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
548 INFO 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
11491 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
13079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13303 INFO 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
16965 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18107 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18431 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.m.key
22525 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24299 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
24512 INFO 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
28063 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
29497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29724 INFO 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
33032 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
34454 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34678 INFO 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
37956 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
39769 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
40034 INFO 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
43341 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
52597 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
52910 INFO 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
56074 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
57531 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57866 INFO 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
61038 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
62754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63034 INFO 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
66194 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
66834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67120 INFO 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
70240 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
70682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70922 INFO 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
74107 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
74566 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74833 INFO 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
77996 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
78749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
78967 INFO 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
82111 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
82696 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82974 INFO 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
86085 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
86834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87099 INFO 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
90269 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
95967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96262 INFO 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
99297 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
101185 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2416164 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test BlockContracts_fullmacro
2416165 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MethodContracts_fullmacro
454 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
479 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
484 INFO 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
10340 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
15587 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15752 INFO 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
19677 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
20527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20698 INFO 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
24233 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
24645 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24814 INFO 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
28204 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
28380 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28546 INFO 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
31872 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
32158 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32326 INFO 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
35599 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37691 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37871 INFO 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
41123 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
41432 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41615 INFO 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
44870 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
45956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
46158 INFO 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
49357 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49698 INFO 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
52853 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
53881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54142 INFO 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
57252 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
57878 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58083 INFO 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
61348 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
61608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61830 INFO 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
64983 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
65192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65398 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../InformationFlow/MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.m.key
68563 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
68670 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68883 INFO 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
72029 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
72423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72706 INFO 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
75902 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
76343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
76586 INFO 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
79864 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
80269 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80545 INFO 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
83603 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
83753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83982 INFO 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
87118 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
87272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87486 INFO 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
90719 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
91020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2507624 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MethodContracts_fullmacro
2507627 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test InformationFlow_fullmacro
451 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
460 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
470 INFO 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
12073 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18899 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
19055 INFO 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
23391 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
25304 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25491 INFO 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
29494 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
31233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31418 INFO 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
35231 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
321606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
321827 INFO 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
325530 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
331757 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
331945 INFO 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
335630 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
341192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
341381 INFO 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
345013 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
349298 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
349495 INFO 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
353028 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
356066 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
356242 INFO 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
359736 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
362905 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
363119 INFO 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
366571 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
368524 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
368727 INFO 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
372187 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
374439 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
374657 INFO 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
378286 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
381058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
381272 INFO 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
384583 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
386346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
386561 INFO 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
389844 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
390982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
391178 INFO 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
394468 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
395347 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
395545 INFO 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
398812 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
398925 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
399125 INFO 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
402409 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
403909 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2911930 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test InformationFlow_fullmacro
2911931 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test MiniExamples_fullmacro
434 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
466 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
474 INFO main d.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
10606 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
11832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
11971 INFO main d.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
15768 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
16274 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16427 INFO main d.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
19800 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19926 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20077 INFO main d.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
23657 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
23902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24052 INFO main d.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
27484 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
27686 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27862 INFO main d.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
31236 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
31680 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31854 INFO main d.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
35159 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
35385 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35547 INFO main d.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
38754 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
38940 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
39201 INFO main d.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
42365 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
43137 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
43318 INFO main d.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
46549 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
48404 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
48591 INFO main d.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
51675 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
51980 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52183 INFO main d.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
55433 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
55625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55828 INFO main d.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
59012 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
59321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59523 INFO main d.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
62691 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
62988 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
63197 INFO main d.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
66372 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
66479 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66675 INFO main d.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
69742 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
69917 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70116 INFO main d.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
73147 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
73296 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73502 INFO main d.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
76604 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
76734 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76934 INFO main d.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
80033 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
80152 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80365 INFO main d.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
83445 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
83561 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83775 INFO main d.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
86772 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
86932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
87203 INFO main d.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
90317 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
90488 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90723 INFO main d.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
93779 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
94075 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94374 INFO main d.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
97471 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
97739 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97971 INFO main d.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
100953 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
101078 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101318 INFO main d.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
104359 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
104631 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104883 INFO main d.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
107944 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
108151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108399 INFO main d.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
111579 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
111799 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112138 INFO main d.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
115318 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
115663 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
115933 INFO main d.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
119189 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
119371 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3031792 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test MiniExamples_fullmacro
3031793 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test NewObjects_fullmacro
489 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
500 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
511 INFO 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
11479 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
12588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12736 INFO 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
16755 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
18258 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18427 INFO 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
22018 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
22638 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
22813 INFO 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
26169 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
26701 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26873 INFO 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
30340 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
30506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30665 INFO 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
34319 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
49658 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49920 INFO 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
53293 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
60859 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61096 INFO 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
64568 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
65171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65396 INFO 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
68899 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
107038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
107310 INFO 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
111013 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
127675 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127943 INFO 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
131584 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
147168 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
147440 INFO 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
151121 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
188716 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
189009 INFO 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
192682 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
205708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
205981 INFO 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
209662 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
220776 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
221054 INFO 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
224600 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
224906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
225141 INFO 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
228750 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
229298 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
229556 INFO 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
233174 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
233559 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
233816 INFO 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
237427 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
237904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238174 INFO 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
241649 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
241756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
242004 INFO 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
245400 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
247342 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3279666 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test NewObjects_fullmacro
3279667 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SimpleEvoting_fullmacro
452 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (1000 secs.)
458 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
474 INFO 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
12655 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
19567 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19746 INFO 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
24668 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
28414 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28643 INFO 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
33099 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
33208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33453 INFO 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
37813 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
37940 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
38122 INFO 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
42278 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
42391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
42593 INFO 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
46883 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
104143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104488 INFO 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
108445 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
166468 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166796 INFO 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
170809 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
172719 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
172931 INFO 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
176977 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
178349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178589 INFO 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
182551 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
204608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
204878 INFO 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
208808 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro 'infflow-autopilot''
233702 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3513859 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SimpleEvoting_fullmacro
3513907 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
3513909 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
3513909 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
3513909 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
3513909 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
3513910 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
3513910 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
3513910 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
3513910 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
3513910 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
3513911 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
3513911 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
3513911 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
3513911 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
3513911 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
3513911 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
3513912 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