333 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test newBook
430 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
453 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)
485 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././newBook/09.list_modelfield/ArrayList.add.key
28217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././newBook/09.list_modelfield/ArrayList.remFirst.key
41120 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45075 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././newBook/09.list_modelfield/ArrayList.empty.key
49393 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52722 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././newBook/09.list_modelfield/ArrayList.size.key
56450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59948 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././newBook/09.list_modelfield/ArrayList.get.key
64133 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68260 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test newBook
68269 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test oldBook
394 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
400 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
427 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/BookExamples/02FirstOrderLogic/Ex2.58.key
9376 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12744 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/BookExamples/03DynamicLogic/Sect3.3.1.key
16152 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87555 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test oldBook
87556 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test comprehensions
480 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
497 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
514 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/general_sum.key
9724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13068 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/sum0.key
16963 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20145 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/sum1.key
23776 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27041 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/sum2.key
30420 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33859 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/sum3.key
37452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40762 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/segsum.key
44164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47455 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/bsum_negative.key
50309 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53335 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/bsum_neg2.key
56233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59075 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/bsumSplit.key
61832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64998 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/bprodSplit.key
67973 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71111 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/bsumSplitInvalid.key
74122 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
162064 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test comprehensions
162066 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performance
420 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
428 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
443 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Disjoint(Disjoint__disjoint_08()).JML_operation_contract.0.key
22129 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34786 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Disjoint(Disjoint__disjoint2_08()).JML_operation_contract.0.key
47024 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58377 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/AccessChain1(AccessChain1__foo_08()).JML_operation_contract.0.key
72173 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84223 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/AccessChain4(AccessChain4__foo_08()).JML_operation_contract.0.key
101453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113143 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Disjoint(Disjoint__xZero_08()).JML_operation_contract.0.key
125008 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
136842 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Dynamic(Dynamic__foo_08()).JML_operation_contract.0.key
154394 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166118 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/DynamicGhost(DynamicGhost__dynamicGhost_08()).JML_normal_behavior_operation_contract.0.key
182174 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
193913 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/GhostFrame(GhostFrame__foo_08()).JML_operation_contract.0.key
206993 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
218546 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Modelfield(Modelfield__foo_08()).JML_operation_contract.0.key
233313 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
407755 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performance
407756 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performancePOConstruction
381 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
401 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
429 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Test(Test__a0(int)).JML_normal_behavior_operation_contract.0.key
22033 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35833 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Test(Test__a1(int)).JML_normal_behavior_operation_contract.0.key
48829 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61518 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Test(Test__f1(int)).JML_normal_behavior_operation_contract.0.key
73365 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
493169 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performancePOConstruction
493170 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test applicationRestrictions
454 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
463 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
485 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed1.key
8447 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed2.key
14401 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14530 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed3.key
17540 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20575 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed4.key
23521 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
23652 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed5.key
26669 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29715 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed6.key
32749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
32893 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed7.key
35728 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38558 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed8.key
41274 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
41426 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed9.key
44357 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47278 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed10.key
50073 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
50241 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/polarity_tests/wellformed11.key
53137 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
546644 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test applicationRestrictions
546646 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test blockContracts
403 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
419 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
450 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__add.key
11385 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15456 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__addAbsoluteValues.key
20108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23954 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__addWithJump.key
27465 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/.././heap/block_contracts/Simple__addWithTwoBlockContracts.key
34841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38466 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__generateByteArray.key
44280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48063 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__getLength.key
51527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54922 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__square.key
58425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61973 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__unnecessaryBlockContract.key
65163 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68415 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__unnecessaryLoopInvariant.key
71613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74862 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert.key
77945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81068 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert_assume_order.key
84073 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87233 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/SimpleVariants/sum_onBlock_external.key
90785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94551 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/SimpleVariants/sum_onBlock_internal.key
98722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102715 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/SimpleVariants/sum_onBlock_loop.key
107083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110958 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/SimpleVariants/sum_onLoop_external.key
114405 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118080 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/SimpleVariants/sum_onLoop_internal.key
121937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125587 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/SimpleVariants/sum_onLoop_loop.key
129637 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133327 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/Free/blockContracts0.key
136171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139058 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/Free/blockContracts1.key
141745 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144574 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/Finally/block_finally.key
147750 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
148106 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/Finally/loop_finally.key
151381 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
698558 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test blockContracts
698562 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test jmlAsserts
476 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
477 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
505 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert.key
9880 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13614 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/Free/assertions0.key
16805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20087 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/Free/assertions1.key
23162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26158 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/recursion-assert.key
29277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32492 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/recursion-assume.key
35798 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38986 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/quantor-assert.key
42111 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45187 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/quantor-assume.key
48279 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51521 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/model-methods-static-static.key
54641 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57741 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/model-methods-instance-static.key
60863 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64076 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/model-methods-instance-instance.key
67276 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70697 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/model-methods-static-instance.key
74355 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77897 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert-old/inc-field.key
81249 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84799 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert-old/inc-parameter.key
87996 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91363 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert-old/inc-parameter-field.key
94723 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98014 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert-old/inc-ghost-field.key
101356 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
803372 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test jmlAsserts
803376 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javaCard
458 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
492 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
520 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/javacard/updateBalance0.key
10231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13069 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/javacard/updateBalance1.key
16022 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18350 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/javacard/setArray1.key
21659 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24122 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/javacard/setArray2.key
27206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29443 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/javacard/arrayFillNonAtomic.key
35827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
842601 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javaCard
842602 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key
413 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
427 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
442 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/coincidence_count/project.key
33173 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
881240 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key
881243 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#1
471 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
479 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/.././heap/verifyThis11_1_Maximum/project.key
11930 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
897403 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#1
897404 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test lcp.key
395 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
405 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
419 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/fm12_01_LRS/lcp.key
12918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
915826 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test lcp.key
915828 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#2
464 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
470 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
486 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SemanticSlicing/project.key
17679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
939249 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#2
939251 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_contains.key
421 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
438 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
457 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/ArrayList_contains.key
11351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
954513 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_contains.key
954514 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_get.key
398 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
415 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
448 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/ArrayList_get.key
12057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
970945 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_get.key
970949 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_size.key
400 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
414 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
438 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/ArrayList_size.key
10820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
985907 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_size.key
985910 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_3_secure.key
470 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
513 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
546 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_3_secure.key
11708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1001840 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_3_secure.key
1001841 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_4_secure.key
432 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
450 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
481 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_4_secure.key
11067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1017383 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_4_secure.key
1017385 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_5_secure.key
403 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
416 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
445 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_5_secure.key
10311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1031539 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_5_secure.key
1031540 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_6_secure.key
405 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
424 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
438 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_6_secure.key
10561 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1046179 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_6_secure.key
1046180 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex9_secure.key
412 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
433 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
462 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex9_secure.key
12684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1063452 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex9_secure.key
1063453 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list
364 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
374 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
394 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_add.key
16570 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22040 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_ArrayList.key
27775 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32266 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_concatenate.key
64963 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71403 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_contains_dep.key
78178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82600 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_enlarge.key
88834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93278 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_footprint.key
97018 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100785 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_get_dep.key
104955 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108856 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_get_exceptional.key
113652 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117820 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_get_normal.key
122071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126047 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_inv.key
130079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134143 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_iterator.key
138392 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142242 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_size_dep.key
146048 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
149873 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_size.key
153836 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
157799 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_ArrayListIterator.key
162168 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166039 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_hasNext_dep.key
170123 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
174087 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_hasNext.key
178193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
182181 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_inv.key
186868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190908 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_list.key
194595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
198510 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_next_exceptional.key
202975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
207051 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_next_normal.key
211770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
215812 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList.ArrayListIterator_pos.key
219491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
223278 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/Client_m.key
226958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
230865 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/Client_n.key
234518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238403 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/LinkedList_get_exceptional.key
244604 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
248861 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/LinkedList_get_normal.key
259203 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
263801 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/LinkedList_LinkedList.key
267884 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
271844 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/LinkedList_size_dep.key
275945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
279787 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/LinkedList_size.key
283910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
287835 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/MySet_footprint.key
291656 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
295535 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/MySet_MySet.key
302043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1370120 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list
1370121 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_ghost
432 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
444 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
475 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_add.key
15537 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20408 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_ArrayList.key
25497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29458 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_enlarge.key
35712 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39800 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_get_dep.key
43456 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47055 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_get_exceptional.key
51237 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54683 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_get_normal.key
58031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61414 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_inv.key
64510 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67844 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_size_dep.key
70972 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74172 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_size.key
77374 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1451041 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_ghost
1451042 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_recursive
428 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
442 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/.././heap/list_recursiveSpec/ListOperationsNonNull_getNextNN_normal_behavior.key
12931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17158 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_recursiveSpec/ListOperationsNonNull_setValueAt_normal_behavior.key
20890 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
23843 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'macro simp-upd'
23851 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'rule observerDependencyEQ'
23876 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'tryclose'
23904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1478982 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_recursive
1478983 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_seq
514 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
539 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
560 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/SimplifiedLinkedList.remove.key
78733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86847 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.ArrayList.key
91732 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96086 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.add.key
103475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107618 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.contains.key
112625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116561 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.enlarge.key
122195 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126271 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.get.key
130433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134161 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.newArray.key
138099 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142151 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.remove.0.key
148083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152378 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/ArrayList.remove.1.key
169458 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1653990 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_seq
1653991 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test observer
437 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
437 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
467 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_ExampleObserver.key
10737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14643 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_inv.key
18139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21625 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_subject.key
24979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28165 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_update.key
31483 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34995 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_upToDate.key
38352 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41933 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_value.key
45280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48831 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_addObserver.key
58830 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63214 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_change.key
66969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70459 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_ExampleSubject.key
74568 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77937 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_footprint.key
80925 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84213 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_inv.key
88730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92064 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_notifyObservers.key
95057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98155 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_value_dep.key
101338 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104623 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_value.key
107659 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1765077 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test observer
1765078 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test removeDups
437 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
454 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/.././heap/removeDups/arrayPart.key
12419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16380 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/removeDups/contains.key
20382 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23925 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/removeDups/removeDup.key
40009 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1810329 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test removeDups
1810331 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test Saddleback_search.key
402 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
429 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
459 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/saddleback_search/Saddleback_search.key
96605 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1915662 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test Saddleback_search.key
1915663 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test quicksort
444 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
476 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/.././heap/quicksort/toplevel.key
10606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14626 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/sort.key
18093 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'script 'sort.script''
18098 INFO main d.u.i.k.m.s.ProofScriptCommand Included script /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/sort.script
18099 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
19412 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'select formula="{heapAtPre:=heap || exc:=null || heap:=heapAfter_sort_0}
seq ...'
19420 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
19432 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'let @seqPre="seqDef{int u;}(0, array.length, array[u])"
@seqSplit="seqDef ...'
19435 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule seqPermSym
formula="seqPerm(@seqSplit, @seqPre)"'
19455 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'rule seqPermSym
formula="seqPerm(@seqSort, @seqSplit)"'
19458 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'rule seqPermSym
formula="seqPerm(@seqSort0, @seqSort)"'
19459 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSplit)"'
19460 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSort)"'
19462 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'rule seqPermSym
formula="seqPerm(@seqPre, @seqSort0)"'
19463 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose'
48022 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54414 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/split.key
57719 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
58981 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'tryclose'
97129 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
97236 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'rule seqPermFromSwap'
97252 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule andRight'
97254 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'auto'
97282 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'instantiate hide var=iv with=i_0'
97286 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'instantiate hide var=jv with=j_0'
97288 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'auto'
104403 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'macro simp-upd'
104491 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'rule seqPermFromSwap'
104495 INFO main d.u.i.k.m.s.ProofScriptEngine 12: 'rule andRight'
104497 INFO main d.u.i.k.m.s.ProofScriptEngine 13: 'auto'
104516 INFO main d.u.i.k.m.s.ProofScriptEngine 14: 'instantiate hide var=iv with=i_0'
104519 INFO main d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate hide var=jv with=to'
104521 INFO main d.u.i.k.m.s.ProofScriptEngine 16: 'auto'
109772 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2033508 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test quicksort
2033509 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simpleTests
386 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
394 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
411 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/anonymise_datagroup.key
9287 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12322 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/array_creation.key
15877 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19094 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/arrays_with_disjoint_sorts.key
22160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25135 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/arrays.key
28101 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31020 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/attributes.key
33719 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36563 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/constructor_contracts.key
40411 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43760 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/dependencies.key
46459 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49224 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/dependency_contracts.key
53456 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56884 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/invariant_preservation.key
60050 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63167 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/locsets.key
65833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68606 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/loop1.key
71707 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74860 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/loop2.key
78159 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81346 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/modifies_datagroup.key
84129 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87213 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/modifies.key
90162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92944 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/object_creation.key
95912 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98983 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/operation_contracts.key
103279 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106744 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/select_store.key
109504 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112513 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/selection_sort.key
119725 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123897 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/seq.key
127104 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130154 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/oldForParams.key
133394 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
136689 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/parse_lmtd.key
139921 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143316 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/strictly_pure/strictlyPureMethod.key
146178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
149258 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/strictly_pure/useStrictlyPureMethod.key
152179 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
155367 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/Wellfounded/ackermann.key
158552 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161938 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/unicode_test.key
164696 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
167485 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/strictlyModular/mayExpand.key
170457 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173509 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/strictlyModular/modularOnly.key
176428 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2210435 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simpleTests
2210437 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SmansEtAl
432 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
445 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
461 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_add.key
18168 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23766 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_ArrayList.key
28391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32165 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_footprint.key
35670 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39103 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_get_dep.key
42626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45993 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_get.key
49420 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52775 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_inv.key
56064 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59555 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_size_dep.key
62889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66525 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_size.key
70065 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73444 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Cell_Cell.key
77076 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80619 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Cell_footprint.key
83888 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87327 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Cell_getX_dep.key
90665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93972 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Cell_getX.key
97209 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100542 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Cell_inv.key
103764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107043 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Cell_setX.key
110353 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113789 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/CellClient_m.key
117505 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120925 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_footprint.key
124105 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127309 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_hasNext_dep.key
131213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134708 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_hasNext.key
138485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141925 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_inv.key
145229 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
148532 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_Iterator.key
153130 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156777 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_list_dep.key
159980 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163300 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_list.key
166441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169716 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Iterator_next.key
175877 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
179627 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Stack_footprint.key
182924 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
186286 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Stack_inv.key
189385 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
192620 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Stack_push.key
196530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
199974 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Stack_size.key
203171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
206673 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Stack_Stack.key
211074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
214738 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/Stack_switchContents.key
222789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2437527 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SmansEtAl
2437529 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VACID0
412 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
440 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
456 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/Harness_sparseArrayTestHarness1.key
11529 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15588 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/Harness_sparseArrayTestHarness2.key
30490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35327 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/MemoryAllocator_alloc_unsigned.key
39591 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43456 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/MemoryAllocator_alloc.key
47390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50931 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/SparseArray_get_dep.key
57678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61472 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/SparseArray_get.key
67110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70814 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/SparseArray_inv.key
76058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79571 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vacid0_01_SparseArray/SparseArray_SparseArray.key
86704 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2528534 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VACID0
2528535 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VSTTE10
390 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
397 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
413 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_01_SumAndMax/SumAndMax_sumAndMax.key
15252 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19666 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_03_LinkedList/Node_cons.key
24690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28296 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_03_LinkedList/Node_inv.key
31732 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35027 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_03_LinkedList/Node_search.key
44654 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48620 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_04_Queens/Queens_isConsistent.key
54276 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58007 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_04_Queens/Queens_nQueens.key
75230 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79772 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/AmortizedQueue_AmortizedQueue.key
84730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88488 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/AmortizedQueue_front.key
91941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95314 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_concat.key
107370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111490 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_cons.key
116900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120277 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_head.key
123169 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126334 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_inv.key
129608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
132802 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_length.key
135761 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139037 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_LinkedList1.key
144247 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
147768 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_LinkedList2.key
152907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156639 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_LinkedList3.key
174578 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
179467 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_reverse.key
192609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196866 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_05_Queue/LinkedList_tail.key
200762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2732776 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VSTTE10
2732777 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test WeideEtAl
398 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
411 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/WeideEtAl_01_AddAndMultiply/AddAndMultiply_add.key
11689 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15590 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/WeideEtAl_01_AddAndMultiply/AddAndMultiply_mul.key
19504 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22797 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/WeideEtAl_02_BinarySearch/BinarySearch_search.key
29200 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2765884 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test WeideEtAl
2765885 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arithmetic
443 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
461 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/.././standard_key/arith/binomial1.key
8834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12196 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/binomial2.key
15246 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18379 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/check_jdiv.key
27158 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30500 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/check_jdiv_concrete.key
33256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35995 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/check_jdiv_instantiated.key
42323 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45342 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/check_jmod.key
48519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51238 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/complexExpressions.key
53837 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56592 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/compound_unaryMinus.key
59478 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62295 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/computation.key
66649 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69687 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/cubicSum.key
73852 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77043 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/divByZero.key
79826 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82842 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/divisionAssoc.key
86357 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89262 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/divisionBy2.key
92126 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95117 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/euclidean/gcdHelp-post.key
101698 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104907 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/gemplusDecimal/add.key
154415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161794 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/jdivevenodd.key
164515 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
167397 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/median.key
186927 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
191198 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/mod1.key
193855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196929 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/mod2.key
199779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
202684 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/mod7.key
205355 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
208142 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/overflow_hija.key
216263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
219665 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/poly_division0.key
222366 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
225355 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/poly_division1.key
228188 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
231164 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/division.key
236081 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
239062 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/inequations0.key
241769 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
244735 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/inequations1.key
247423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
250324 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/inequations2.key
252970 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
255679 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/linApprox.key
258154 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
260954 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/nonLinInEqExample0.key
263511 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
266221 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/nonLinInEqExample2.key
268950 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
271674 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/nonLinInEqExample3.key
274315 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
277290 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/nonLinInEqExample4.key
279924 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
282684 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq.key
285487 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
288558 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq10.key
291476 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
294393 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq13.key
297192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
300130 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq14.key
303193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
306280 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq2.key
309054 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
311969 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq3.key
314639 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
317620 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq4.key
320291 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
323185 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq5.key
325857 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
328694 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq6.key
331433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
334501 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq7.key
337276 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
340303 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/quadraticInEq8.key
342942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
345868 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/simplify0.key
348572 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
351470 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/simplify1.key
354145 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
357166 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/simplify2.key
359831 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
362872 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/simplify3.key
365595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
368557 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/simplify4.key
371311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
374338 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/simplify5.key
377510 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
380670 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/inEqSimp/subsumptionExample.key
383335 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
386355 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify0.key
389122 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
392221 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify1.key
395272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
398380 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify10.key
401186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
404194 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify11.key
406858 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
409871 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify12.key
412451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
415424 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify13.key
418109 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
421214 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify14.key
423855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
427032 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify15.key
429805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432887 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify16.key
435446 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
438393 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify17.key
441008 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
443931 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify18.key
446645 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
449714 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify19.key
455555 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
459277 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify2.key
462161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
465372 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify20.key
468620 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
471883 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify21.key
475080 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
478315 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify22.key
480987 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
484046 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify23.key
486786 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
489856 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify24.key
492531 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
495661 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify25.key
498235 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
501294 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify3.key
504029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
507324 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify4.key
509948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
513199 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify5.key
515886 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
519046 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify6.key
521639 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
524673 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify7.key
527287 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
530336 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify8.key
537099 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
540410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/polySimp/simplify9.key
543270 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3312482 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arithmetic
3312489 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arrays
413 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
426 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/.././standard_key/arrays/arrayStoreException/array2DimPrim.key
14271 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18638 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/arrayStoreKnownDynType.key
21931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25199 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/reverseArray.key
28868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32175 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/throwArrayStoreException.key
35615 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39028 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/creation/arrayCreation1.key
42181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45347 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/array2Dim.key
51777 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
52082 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/array2DimClose.key
57371 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
57804 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/throwASEForPrim.key
65389 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3378449 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arrays
3378450 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javadl
417 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
430 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
445 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/instanceCreation/instanceCreation1.key
10156 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13853 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/instanceCreation/instanceCreation2.key
17760 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21086 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/instanceCreation/interfacesAndAbstractClassesHaveNoInstances.key
24238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27436 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/instanceCreation/successiveCreatedObjectsAreDistinct.key
30770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34228 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/instanceCreation/testOverloadingConstructors.key
37656 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40984 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/SimpleAttributes.key
44193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47403 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/arrayMax.key
52277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56100 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/arrayUpdateSimp.key
56134 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
56135 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
56135 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
59294 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59577 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
59577 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
59578 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
62849 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/attributes.key
66120 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69415 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/break.key
69442 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
69443 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
69443 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
72770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73037 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
73037 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
73038 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
75930 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/char.key
78861 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81825 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/compileTimeConstants.key
84724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87742 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/constructorException/test.key
90994 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94221 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/constructorException/regressionTestBug1333.key
97143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
97362 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/continue1.key
97388 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
97388 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
97388 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
100360 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100616 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
100617 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
100617 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
103394 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/continue2.key
103419 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
103419 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
103419 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
106681 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106950 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
106950 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
106951 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
109882 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/complexAssignment.key
112828 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115847 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/danglingElseSolution1.key
118750 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121729 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/danglingElseSolution2.key
124511 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127486 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/deepNonNull/deepNonNull0.key
130617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133835 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/deepNonNull/deepNonNull1.key
137374 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
140736 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/deepNonNull/deepNonNull2.key
143837 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
144134 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/deepNonNull/deepNonNull3.key
148045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151442 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/exceptions.key
151467 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
151468 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
151468 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
154596 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154992 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
154992 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
154992 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
157903 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/exceptions1.key
160969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
164244 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/exceptions2.key
167464 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170828 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/exceptions3.key
170858 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
170859 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
170859 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
173837 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
174192 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
174192 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
174192 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
177218 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/exchange.key
180142 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183283 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/if.key
186324 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
189433 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/incrementcounter.key
192256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
195417 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/danglingElse.key
198241 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
198585 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/iteratedAssignment.key
201796 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
205101 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/assert/assert1.key
208163 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
208513 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/assert/assert2.key
211453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
214560 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/assert/assert3.key
217463 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
217814 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/java5/vararg.key
222295 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
226205 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/java5/for_Array.key
229631 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
233297 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/java5/for_Iterable.key
236664 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
240157 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/java5/for_ReferenceArray.key
243516 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
246968 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-bigint/cast.key
249821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
252862 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-free/loopInvFree.key
255717 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
258758 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-free/ensuresFree.key
261520 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
264601 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-information-flow.key
398957 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
406266 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-min/min-unprovable1.key
409483 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
410115 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-min/min-unprovable2.key
413110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
413543 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/methodCall.key
416413 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
419558 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/methodCall1.key
422642 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
425997 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/methodCall1box.key
429001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432352 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/methodCall3.key
435227 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
438401 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/polishFlagSort.key
443547 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
447182 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/postConditionTaclets1.key
449985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
453115 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/postConditionTaclets2.key
455767 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
458797 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/quantifiedQuery.key
461519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
464640 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/recursion/triangular.key
467508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
470669 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/reverseArray.key
470692 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
470692 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
470692 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/./classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
478219 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
478767 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
478768 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
478768 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
482230 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/reverseArray2.key
482254 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
482254 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
482254 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
486588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
487219 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
487219 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
487220 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
490471 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/simpleAssignment.key
493261 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
496499 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/simpleAssignment2.key
499361 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
502563 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/splittingWithQueries.key
505473 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
508871 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/strassen/strassen.key
517593 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
521975 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/symmArray.key
631277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
636121 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/testcontext.key
636143 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
636144 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
636144 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
639360 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
640114 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
640115 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.InputStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/InputStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/InputStream.java
640115 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
643064 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/cascadeStaticInitialisation.key
643090 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
643090 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
646913 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
647607 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
647607 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
650663 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/erroneousClassImpliesErroneousSubclass.key
650687 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
650687 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
653621 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
654272 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
654272 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
657067 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/initializedSubclassImpliesInitializedSuperclass.key
657090 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
657090 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
660091 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
660703 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
660703 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
663681 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/localDeclared.key
663705 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
663706 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
666970 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
667619 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
667620 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
670623 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/localDeclaredMethod.key
670646 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
670646 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
673769 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
674464 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
674464 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
677550 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/objectOfErroneousClass.key
677585 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
677585 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
694979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
695700 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
695701 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
700961 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/staticInitialisersAreNonSimple.key
700983 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
700983 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
704309 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
705027 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.io.PrintStream declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/PrintStream.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java
705027 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype java.lang.System declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/staticInitialisation/classpath/System.java and once in URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java, Keeping one from URL:file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/System.java
707904 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/types/disjoint.key
710806 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
714127 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath.key
714152 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype cp.C declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.class and once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml, Keeping one from FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml
717169 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
717845 WARN main d.u.i.k.j.r.KeYCrossReferenceNameInfo Datatype cp.C declared twice: Once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.class and once in FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml, Keeping one from FILE:/home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/classpath/classpath/C.jml
720816 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/inconsistent_represents/MyClass_m.key
723876 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
724530 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/inconsistent_represents/MyClass_n.key
727581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
4106934 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javadl
4106936 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test FOL
442 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
445 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
468 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/count.key
9546 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12780 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/count2.key
15918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
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/.././standard_key/pred_log/count3.key
22025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25065 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/equalities.key
27945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30728 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/equalities2.key
33533 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36358 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/equalities3.key
39113 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42022 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/functions.key
44890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47973 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/mv1.key
50790 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53690 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/mv2.key
56603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59628 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/quantifiers.key
62573 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65582 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/simpleEps.key
68465 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71451 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/steam1.key
74581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77605 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/PUZ/PUZ001p1.key
83753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86854 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/PUZ/PUZ001p1-eq.key
89561 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92414 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/PUZ/PUZ031p1.key
104479 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107444 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/SET/SET027p3.key
110181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112939 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/SET/SET043p1.key
115572 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118452 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/SET/SET045p1.key
121217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124076 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/SET/SET062p3.key
126880 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129765 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/SET/SET063p3.key
132485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135430 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/SYN/SYN036p2.key
138433 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141452 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/SYN/SYN550p1.key
147425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150456 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/prop_log/reallySimple.key
153181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
153471 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/sameName1.key
156124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
156388 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/jbyteIfEx.key
159141 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
162065 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/prop_log/allClausesLength4.key
164867 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
167838 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/prop_log/allClausesLength5.key
170809 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173875 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/prop_log/doubleNeg.key
176635 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
179576 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/prop_log/liarsville.key
182346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
185345 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/prop_log/simplest.key
188026 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190984 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/prop_log/contraposition.key
193785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196772 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/elimination0.key
199467 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
202405 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/heuristic_PUZ001p1-eq.key
205161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
208116 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/heuristic_PUZ001p1.key
212226 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
215179 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/heuristic_PUZ031p1.key
223309 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
226490 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/heuristic_SYN036p2.key
229389 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232486 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/injectivity.key
235245 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238198 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation0.key
240958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
243813 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation1.key
246598 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
249783 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation2.key
252671 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
255800 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation3.key
258558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
261653 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation4.key
264511 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
267595 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation5.key
270441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
273605 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation6.key
276425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
279602 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation7.key
282365 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
285626 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation8.key
288529 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
291612 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation9.key
294476 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
297688 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation10.key
300509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
303705 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation12.key
306481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
309439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/normalisation13.key
312177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
315182 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/quantifiers/triggers0.key
317799 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4427905 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test FOL
4427906 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test strings
467 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
475 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/.././standard_key/strings/charAt0.key
9393 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12702 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/charAt1.key
15874 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19162 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/concat1.key
22196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25674 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/concat2.key
28839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32105 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/deriveLength1.key
35357 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38670 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/emptyStringLengthZero.key
41925 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45422 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/implicitBooleanStringConversion.key
49650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53090 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/implicitBooleanStringConversion2.key
56664 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59983 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/implicitIntStringConversion.key
63764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67139 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/implicitNullStringConversion.key
70568 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73870 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/implicitNullStringConversion2.key
77120 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80436 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/implicitObjectStringConversion.key
84170 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87655 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/literalEquality.key
90695 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93800 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/replace0.key
96701 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99829 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/replace1.key
102832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105968 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/simpleAssignment.key
108939 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111908 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/simpleLengthComp.key
114994 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118248 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/stringCompileTimeConstant1.key
121396 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124719 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/stringCompileTimeConstant2.key
131040 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134821 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/stringEquality1.key
137924 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141221 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/stringEquality2.key
144514 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
147827 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/substring0.key
150919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154085 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/substring1.key
157306 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
160463 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/substring2.key
163444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166546 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/substring3.key
169507 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
172658 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/substring4.key
175668 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178739 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/substring5.key
181740 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4612815 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test strings
4612816 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simple_info_flow
399 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
419 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
446 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_1_insecure.key
10607 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
10788 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_2_insecure.key
15108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
4628273 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simple_info_flow
4628274 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test modelMethods
462 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
482 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/.././heap/model_methods/Cell_footprint_acc.key
10474 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14665 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Cell_footprint.key
18278 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21924 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Cell_get_acc.key
25818 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29662 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Cell_get.key
33245 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36773 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Cell_post_set.key
40374 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44001 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Cell_set.key
54220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58515 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/CellTest_callSet.key
62060 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65643 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/CellTest_test2.key
69262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72866 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/CellTest_test.key
79188 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83309 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll1_add.key
86710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90235 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll1_Coll1_add_pre.key
93632 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96969 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll1_Coll_add_pre.key
100288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103745 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll2_add.key
107046 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110435 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll2_Coll2_add_pre.key
113748 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117108 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll2_Coll_add_pre.key
120490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123932 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll_add.key
127222 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130622 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Coll_add_pre.key
133787 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
137164 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Indirect_callAdd.key
140438 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143745 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Indirect_test.key
146978 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_Cell_footprint.key
153607 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156975 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_Cell_post_set.key
160270 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163455 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_footprint_acc.key
166529 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169774 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_get_acc.key
173121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
176601 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_get.key
179778 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_Recell_footprint.key
186782 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190267 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_Recell_post_set.key
193527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
197059 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_set.key
207713 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
211826 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Recell_undo.key
215193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4847233 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test modelMethods
4847234 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test permissionHeap
550 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
555 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
583 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/permissions_method0.key
11759 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15810 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/permissions_method1.key
19687 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23416 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/permissions_method3.key
28436 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/.././heap/permissions/permissions_setAB.key
37421 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41110 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/permissionProperties.key
45243 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48219 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_AFilter.key
56346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62075 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_initPost_accessible.key
67397 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73183 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_inv_accessible1.key
78929 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84923 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_inv_accessible2.key
90685 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96640 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_joinTransfer_accessible.key
103435 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109442 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_joinTransfer_contract.key
114834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120543 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_postJoin_accessible.key
126117 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131475 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_preStart_accessible.key
137000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142580 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_startTransfer_accessible.key
158458 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
165323 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_startTransfer_contract.key
171478 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177388 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_stateInv_accessible.key
183444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
189362 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_staticPermissions_accessible.key
194934 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
200438 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/AFilter_workingPermissions_accessible.key
205945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
211686 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_BFilter.key
218231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
224196 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_initPost_accessible.key
229786 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
235587 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_inv_accessible1.key
241066 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
246799 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_inv_accessible2.key
252280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
257886 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_joinTransfer_accessible.key
264592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
270644 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_joinTransfer_contract.key
276362 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
282342 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_postJoin_accessible.key
287794 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
293504 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_preStart_accessible.key
299340 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
305351 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_startTransfer_accessible.key
322196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
329282 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_startTransfer_contract.key
336040 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
342114 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_stateInv_accessible.key
348010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
353916 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_staticPermissions_accessible.key
359581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
365318 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/BFilter_workingPermissions_accessible.key
370900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
376737 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_Fib.key
382916 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
388806 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_initPost_accessible.key
394408 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
400265 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_inv1_accessible.key
405891 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
411795 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_inv2_accessible.key
417345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
423069 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_joinTransfer_accessible.key
428728 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
434705 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_joinTransfer_contract.key
440266 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
446184 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_postJoin_accessible.key
451800 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
457792 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_preStart_accessible.key
463436 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
469356 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_startTransfer_accessible.key
474961 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
480811 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_startTransfer_contract.key
486154 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
491901 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Fib_workingPermissions_accessible.key
497403 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
503148 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_initPost_accessible.key
508759 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
514729 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_inv_accessible1.key
520616 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
526727 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_inv_accessible2.key
532575 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
539039 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_joinTransfer_contract.key
545247 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
551230 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_Plotter.key
558339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
564620 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_postJoin_accessible.key
570136 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
576058 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_preStart_accessible.key
582281 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
588077 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_stateInv_accessible.key
601224 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
607668 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_staticPermissions_accessible.key
614033 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
620065 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_workingPermissions_accessible.key
625921 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
631937 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_initPost_accessible.key
637562 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
643307 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_inv_accessible1.key
648789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
654719 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_inv_accessible2.key
660244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
666277 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_joinTransfer_accessible.key
675324 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
682051 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_joinTransfer_contract.key
687629 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
693572 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_postJoin_accessible.key
699128 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
705166 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_preStart_accessible.key
710793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
716961 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_run.key
722821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
729156 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_Sampler.key
735390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
741595 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_startTransfer_accessible.key
751984 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
759184 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_startTransfer_contract.key
764931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
771188 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_stateInv_accessible.key
776634 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
782676 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_staticPermissions_accessible.key
788086 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
793891 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Sampler_workingPermissions_accessible.key
799402 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
805271 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/mulleretal/ReadWrite_doRead_contract.key
810220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
814619 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/mulleretal/ReadWrite_doWrite_contract.key
820311 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
824753 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/mulleretal/ReadWrite_read_contract.key
828089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
831931 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/mulleretal/ReadWrite_write_contract.key
835345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
839447 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/mulleretal/ReadWrite_inv1_accessible.key
842746 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
846413 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/mulleretal/ReadWrite_inv2_accessible.key
849625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
853536 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_lockConsistent_contract.key
858775 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
863525 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_increase_contract.key
869144 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
873947 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_fp_accessible.key
877865 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
882144 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_fpLock_accessible.key
886069 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
890396 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_fpPerm_accessible.key
894404 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
898746 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_inv_accessible1.key
902532 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
906932 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_inv_accessible2.key
910773 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
915139 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_lockRef_accessible.key
918986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
923325 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_lockRef_contract1.key
926918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
931226 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_lockRef_contract2.key
935049 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
939429 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_lockState_accessible.key
943606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
948174 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_lockStatus_accessible.key
951901 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
956357 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_lockTransfer_accessible.key
960338 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
964827 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/lockspec/Counter_unlockTransfer_accessible.key
968927 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
973472 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_startTransfer_contract.proof
979055 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
979056 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_startTransfer_accessible.proof
984990 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
984997 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/threads/Plotter_joinTransfer_accessible.proof
991052 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
991055 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
991057 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
991058 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
991059 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
991061 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
991063 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
991065 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
991067 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
991069 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
991070 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
991071 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
991073 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
991073 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
991075 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
991076 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
991076 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
991078 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
991079 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
991079 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
991080 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
991081 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
991175 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
5838616 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test permissionHeap
5838616 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test completionScopes
408 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
422 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
441 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testCcatchReturnVal.key
10929 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14872 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testMultCcatchClauses.key
18634 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22286 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testNestedExec.key
25839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29225 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testCcatchBreakLabel.key
32535 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35992 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testCcatchContinueLabel.key
39281 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42645 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testCcatchBreakLabelWildcard.key
45824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49024 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testCcatchContinueLabelWildcard.key
52211 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55578 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testCcatchBreakLabelNonmatchingNested.key
58805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5900882 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test completionScopes
5900883 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test reload_examples
416 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
420 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
443 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././firstTouch/05-ReverseArray/reverseArray.key
22274 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27394 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/saveProofTest.key.proof
30332 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
30333 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permutedSum/perm.proof
34928 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
34930 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././firstTouch/05-ReverseArray/reverseArray.proof
39409 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
39410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/verifyThis15_1_RelaxedPrefix/relax.proof
42897 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
42898 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/verifyThis15_3_DLL/doUndo.proof
47010 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
47011 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/verifyThis15_2_ParallelGcd/parallelGcd.proof
50813 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
5951896 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test reload_examples
5951897 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test proofLoadRepair
388 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
394 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././proofLoadRepair/disjConj-manipulated.proof
8669 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft
8671 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right
8676 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close
8682 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
8691 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././proofLoadRepair/insufficient-manipulated.proof
11905 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for applyEq
11917 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
11918 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/issues/1716/incorrectPolarity.proof
15072 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
15073 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/issues/1716/incorrectPolarity2.proof
17986 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
17987 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/src/test/resources/testcase/issues/1716/incorrectPolarity3.proof
20885 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
5972967 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test proofLoadRepair
5972968 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test switch
390 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
402 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
425 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/labeled_case.key
9730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13427 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/empty_switch.key
16513 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19478 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/empty_switch_null.key
22500 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25496 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/empty_switch_null_catch.key
28456 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31456 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/empty_switch_array_out_of_bounds.key
34512 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37515 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/empty_switch_array_out_of_bounds_catch.key
40496 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43430 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/switch_in_switch.key
51322 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55104 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/while_and_switch.key
58737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61935 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/large_switch.key
66330 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
6042825 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test switch
6042826 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test redux
438 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
444 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
468 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOf.key
15213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19930 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOf.float.key
23683 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
28601 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
28705 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 17 in 74ms, result is valid
28706 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
30651 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35337 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOfRange.key
44306 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48912 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.copyOfRange.float.key
52606 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
59408 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
59454 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 27 in 38ms, result is valid
59454 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
63399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68482 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.equals.key
72834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76719 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.fill.key
80509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84317 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.fill.float.key
88001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91729 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.fillFromTo.key
95823 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99671 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/Arrays.fillFromTo.float.key
104058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107821 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/ArrayCopy.arraycopy.normal.0.key
118513 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123384 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/ArrayCopy.arraycopy.exceptional.0.key
127222 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131129 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././redux/arrays/ArrayCopy.arraycopy.exceptional.1.key
141868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
6190584 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test redux
6190626 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Total rule apps.sum.properties is written
6190628 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Total rule apps.avg.properties is written
6190628 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Nodes.sum.properties is written
6190628 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Nodes.avg.properties is written
6190628 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Branches.sum.properties is written
6190628 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Branches.avg.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Overall time (ms).sum.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Overall time (ms).avg.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Automode time (ms).sum.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Automode time (ms).avg.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Closed.sum.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Closed.avg.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Time per step (ms).sum.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Time per step (ms).avg.properties is written
6190629 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Total Runtime Memory (kB).sum.properties is written
6190630 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/Total Runtime Memory (kB).avg.properties is written
6190635 INFO Test worker d.u.i.k.p.r.p.StatisticsFile /home/runner/work/key/key/key.core/../key.ui/examples/index/../../../key.core/build/reports/runallproofs/NumberTestFiles.properties is written