347 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test newBook
327 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
343 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)
371 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
26506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31279 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
38864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42588 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
46447 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49564 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
52815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55809 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
59512 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63258 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test newBook
63271 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test oldBook
335 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
358 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
382 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/BookExamples/02FirstOrderLogic/Ex2.58.key
8125 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11025 INFO main 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
13977 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80050 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test oldBook
80053 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test comprehensions
380 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
384 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
402 INFO 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
8488 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11632 INFO 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
15323 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18233 INFO 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
21403 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24292 INFO 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
27291 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30139 INFO 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
33111 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35931 INFO 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
38858 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41637 INFO 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
44115 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46615 INFO 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
49092 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51587 INFO 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
54044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56617 INFO 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
59039 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61519 INFO 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
63948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
144358 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test comprehensions
144362 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performance
338 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
338 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
370 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
20413 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32126 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
43688 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54354 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
67284 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78238 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
94742 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106166 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
117415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127952 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
143613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154511 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
169116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
180096 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
192331 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
203071 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
216220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
371616 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performance
371622 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performancePOConstruction
357 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
380 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
408 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
17851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29297 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
40496 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51489 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
62197 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
444725 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performancePOConstruction
444726 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test applicationRestrictions
399 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
417 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
433 INFO 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
8827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11866 INFO 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
14646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
14757 INFO 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
17595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20339 INFO 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
22950 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
23073 INFO 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
25710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28347 INFO 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
30955 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
31103 INFO 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
33740 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36422 INFO 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
39014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
39153 INFO 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
41753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44390 INFO 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
46954 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47106 INFO 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
49702 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
494748 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test applicationRestrictions
494754 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test blockContracts
380 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.
408 INFO 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
9945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13737 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__addAbsoluteValues.key
18208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21906 INFO 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
25246 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28488 INFO 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
31726 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34976 INFO 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
40198 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43650 INFO 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
46782 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49968 INFO 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
53406 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56745 INFO 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
59880 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63120 INFO 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
66180 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69386 INFO main 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
72262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75099 INFO main 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
77853 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80672 INFO 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
83675 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86698 INFO 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
90114 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93355 INFO 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
96971 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100225 INFO 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
103074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106090 INFO 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
109462 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112759 INFO 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
116235 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119517 INFO 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
122086 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124750 INFO 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
127321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129995 INFO 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
133116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
133398 INFO 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
136556 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
631755 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test blockContracts
631756 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test jmlAsserts
379 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
388 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
401 INFO main 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
9586 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12911 INFO 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
15980 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18964 INFO 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
21793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24612 INFO main 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
27636 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30681 INFO main 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
33693 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36713 INFO main 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
39841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42754 INFO main 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
45621 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48519 INFO main 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
51413 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54223 INFO main 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
56989 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59798 INFO main 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
62613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65479 INFO main 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
68257 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71093 INFO main 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
73864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76638 INFO main 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
79353 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82085 INFO main 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
84867 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87620 INFO main 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
90321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
725011 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test jmlAsserts
725013 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javaCard
334 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
347 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/javacard/updateBalance0.key
8199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10419 INFO 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
12791 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14682 INFO 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
17531 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19623 INFO 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
22393 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24429 INFO 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
29688 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
757512 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javaCard
757514 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key
355 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
377 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
392 INFO 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
27838 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
790121 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key
790123 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#1
351 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
371 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
400 INFO 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
10773 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
804560 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#1
804561 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test lcp.key
411 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
441 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/fm12_01_LRS/lcp.key
11684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
820433 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test lcp.key
820434 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#2
381 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
393 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
408 INFO 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
15552 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
840543 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#2
840545 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_contains.key
406 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.
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/information_flow/ArrayList_contains.key
10182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
854460 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_contains.key
854462 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.)
406 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
431 INFO 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
11140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
869591 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_get.key
869592 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_size.key
364 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
377 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
396 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/ArrayList_size.key
9847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
883031 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_size.key
883034 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_3_secure.key
398 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
425 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_3_secure.key
9964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
896778 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_3_secure.key
896781 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_4_secure.key
363 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.
403 INFO 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
9956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
910381 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_4_secure.key
910382 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_5_secure.key
383 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
396 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/information_flow/UpdateAbstraction_ex7_5_secure.key
9001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
923045 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_5_secure.key
923046 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_6_secure.key
334 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
362 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
389 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_6_secure.key
10691 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
937539 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_6_secure.key
937540 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex9_secure.key
377 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
395 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/.././heap/information_flow/UpdateAbstraction_ex9_secure.key
10833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
952303 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex9_secure.key
952304 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list
383 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
398 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
412 INFO 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
14801 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/list/ArrayList_ArrayList.key
24720 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28493 INFO 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
57564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63429 INFO 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
69714 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73638 INFO 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
79278 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83096 INFO 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
86449 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89783 INFO 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
93390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96828 INFO 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
101207 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104817 INFO 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
108391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111784 INFO 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
115366 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118793 INFO 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
122441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125820 INFO 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
129198 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
132566 INFO 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
135881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139261 INFO 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
143030 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146520 INFO 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
149942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
153379 INFO 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
156884 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
160263 INFO 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
164346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
167826 INFO 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
171043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
174362 INFO 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
178396 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
181879 INFO 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
185992 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
189526 INFO 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
192717 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196024 INFO 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
199401 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
202795 INFO 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
206010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
209457 INFO 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
214655 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
218341 INFO 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
227008 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
230932 INFO 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
234554 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238020 INFO 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
241596 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
244969 INFO 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
248456 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
251839 INFO 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
255213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
258596 INFO 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
264064 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1220312 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list
1220318 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_ghost
357 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
363 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_ghost/ArrayList_add.key
13974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17891 INFO 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
21829 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24881 INFO 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
29569 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32898 INFO 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
36025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38822 INFO 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
42153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45112 INFO 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
47896 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50718 INFO 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
53403 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56125 INFO 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
58791 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61540 INFO 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
64207 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1287452 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_ghost
1287455 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_recursive
335 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
351 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
379 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_recursiveSpec/ListOperationsNonNull_getNextNN_normal_behavior.key
9662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13121 INFO 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
16073 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
18496 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'macro simp-upd'
18504 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'rule observerDependencyEQ'
18525 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'tryclose'
18550 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1309256 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_recursive
1309259 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_seq
336 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
349 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
375 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/SimplifiedLinkedList.remove.key
70634 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77661 INFO 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
82202 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85925 INFO 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
92834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96894 INFO 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
101844 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105614 INFO 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
111079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114868 INFO 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
118719 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122261 INFO 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
125811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129237 INFO 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
134436 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138331 INFO 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
153835 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1468209 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_seq
1468210 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test observer
366 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.
387 INFO 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
10267 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13892 INFO 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
17018 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20119 INFO 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
23196 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26215 INFO 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
29260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32269 INFO 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
35182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38146 INFO 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
40974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43802 INFO 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
52015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55631 INFO 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
58794 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61758 INFO 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
65418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68513 INFO 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
71272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74116 INFO 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
77820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80785 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleSubject_notifyObservers.key
83554 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86361 INFO 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
89092 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91941 INFO 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
94646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1565822 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test observer
1565823 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test removeDups
345 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
351 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
366 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/removeDups/arrayPart.key
11261 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14802 INFO 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
18161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21051 INFO 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
34600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1604949 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test removeDups
1604950 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test Saddleback_search.key
344 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
369 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
399 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/saddleback_search/Saddleback_search.key
86759 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1698972 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test Saddleback_search.key
1698973 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test quicksort
367 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.
398 INFO 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
9722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13203 INFO 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
16105 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'script 'sort.script''
16108 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
16109 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
17213 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'select formula="{heapAtPre:=heap || exc:=null || heap:=heapAfter_sort_0}
seq ...'
17217 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
17227 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'let @seqPre="seqDef{int u;}(0, array.length, array[u])"
@seqSplit="seqDef ...'
17230 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule seqPermSym
formula="seqPerm(@seqSplit, @seqPre)"'
17246 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'rule seqPermSym
formula="seqPerm(@seqSort, @seqSplit)"'
17248 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'rule seqPermSym
formula="seqPerm(@seqSort0, @seqSort)"'
17250 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSplit)"'
17251 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSort)"'
17252 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'rule seqPermSym
formula="seqPerm(@seqPre, @seqSort0)"'
17252 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose'
43189 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48507 INFO 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
51505 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
52733 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'tryclose'
89950 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
90063 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'rule seqPermFromSwap'
90099 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule andRight'
90102 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'auto'
90134 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'instantiate hide var=iv with=i_0'
90140 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'instantiate hide var=jv with=j_0'
90142 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'auto'
96720 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'macro simp-upd'
96809 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'rule seqPermFromSwap'
96813 INFO main d.u.i.k.m.s.ProofScriptEngine 12: 'rule andRight'
96815 INFO main d.u.i.k.m.s.ProofScriptEngine 13: 'auto'
96835 INFO main d.u.i.k.m.s.ProofScriptEngine 14: 'instantiate hide var=iv with=i_0'
96838 INFO main d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate hide var=jv with=to'
96840 INFO main d.u.i.k.m.s.ProofScriptEngine 16: 'auto'
101832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1807764 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test quicksort
1807765 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simpleTests
363 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
378 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
404 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/simple/anonymise_datagroup.key
8568 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11652 INFO 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
15293 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18257 INFO 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
21090 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23885 INFO 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
26594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29380 INFO 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
32062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34840 INFO 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
38540 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41702 INFO 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
44336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47093 INFO 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
51425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54634 INFO 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
57665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60673 INFO 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
63272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65983 INFO 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
68909 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71896 INFO 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
75352 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78503 INFO 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
81126 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83834 INFO 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
86432 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89147 INFO 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
91812 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94538 INFO 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
98109 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101121 INFO 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
103678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106339 INFO 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
112746 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116350 INFO 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
119224 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121947 INFO 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
124844 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127804 INFO 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
130596 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133552 INFO 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
136285 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139116 INFO 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
141812 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144638 INFO 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
147505 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150416 INFO main 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
152940 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
155578 INFO 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
158185 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161000 INFO 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
163660 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1971884 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simpleTests
1971885 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SmansEtAl
359 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
377 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
401 INFO 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
16600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21321 INFO 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
25378 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28715 INFO 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
31733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34846 INFO 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
37989 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41150 INFO 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
44225 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47293 INFO 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
50278 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53324 INFO 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
56232 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59268 INFO 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
62193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65171 INFO 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
68171 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71147 INFO 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
74028 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76983 INFO 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
79864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82857 INFO 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
85708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88710 INFO 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
91560 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94571 INFO 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
97409 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100482 INFO 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
103784 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106882 INFO 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
109756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112761 INFO 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
116124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119292 INFO 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
122570 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125618 INFO 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
128588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131575 INFO 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
135611 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138772 INFO 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
141638 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144691 INFO 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
147479 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150431 INFO 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
155670 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
158976 INFO 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
161888 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
164899 INFO 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
167750 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170803 INFO 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
174195 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177320 INFO 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
180234 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183257 INFO 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
186971 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190153 INFO 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
197117 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2172675 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SmansEtAl
2172676 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VACID0
396 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
418 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
431 INFO 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
10349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13750 INFO 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
26424 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30632 INFO 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
34628 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37790 INFO 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
41152 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44239 INFO 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
50166 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53476 INFO 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
58475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61724 INFO 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
66257 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69324 INFO 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
75394 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2251717 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VACID0
2251717 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VSTTE10
377 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
391 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
416 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/vstte10_01_SumAndMax/SumAndMax_sumAndMax.key
13400 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17181 INFO 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
21542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24671 INFO 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
27608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30339 INFO 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
38750 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42284 INFO 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
47051 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50261 INFO 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
65138 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68913 INFO 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
73032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76072 INFO 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
79042 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81869 INFO 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
92888 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96528 INFO 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
101287 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104303 INFO 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
106964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109725 INFO 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
112552 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115309 INFO 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
117966 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120794 INFO 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
125240 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128337 INFO 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
132864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135978 INFO 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
152192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156246 INFO 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
167870 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
171424 INFO 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
174477 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2429261 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VSTTE10
2429261 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test WeideEtAl
402 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
406 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/WeideEtAl_01_AddAndMultiply/AddAndMultiply_add.key
10305 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13611 INFO 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
16843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19733 INFO 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
25536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2458334 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test WeideEtAl
2458335 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arithmetic
408 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.
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/.././standard_key/arith/binomial1.key
8176 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11167 INFO main 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
13993 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16859 INFO main 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
24404 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27572 INFO main 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
30184 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32958 INFO main 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
38625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41596 INFO main 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
44686 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47428 INFO main 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
50049 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52748 INFO main 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
55344 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58012 INFO main 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
61985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64794 INFO main 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
68502 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71621 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/divByZero.key
74381 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77142 INFO main 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
80406 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83224 INFO main 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
85810 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88466 INFO main 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
94218 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97237 INFO main 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
140027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146796 INFO main 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
149582 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152395 INFO main 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
169455 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173386 INFO main 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
175959 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178736 INFO main 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
181261 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183904 INFO main 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
186457 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
189173 INFO main 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
195968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
199048 INFO main 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
201653 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
204380 INFO main 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
206905 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
209574 INFO main 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
213942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
216714 INFO main 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
219302 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
222006 INFO main 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
224545 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
227206 INFO main 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
229721 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232376 INFO main 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
234858 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
237501 INFO main 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
240007 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
242650 INFO main 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
245343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
248031 INFO main 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
250694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
253427 INFO main 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
255919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
258594 INFO main 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
261326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
264035 INFO main 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
266613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
269311 INFO main 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
271886 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
274584 INFO main 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
277265 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
279986 INFO main 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
282475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
285166 INFO main 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
287645 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
290384 INFO main 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
292848 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
295533 INFO main 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
298010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
300769 INFO main 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
303244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
305937 INFO main 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
308409 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
311104 INFO main 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
313577 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
316297 INFO main 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
318777 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
321494 INFO main 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
323967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
326674 INFO main 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
329141 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
331872 INFO main 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
334371 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
337104 INFO main 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
339584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
342349 INFO main 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
345221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
348033 INFO main 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
350511 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
353277 INFO main 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
355846 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
358622 INFO main 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
361312 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
364128 INFO main 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
366737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
369578 INFO main 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
372185 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
375010 INFO main 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
377497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
380302 INFO main 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
382789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
385580 INFO main 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
388065 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
390850 INFO main 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
393327 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
396223 INFO main 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
398902 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
401672 INFO main 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
404152 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
407133 INFO main 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
410130 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
413286 INFO main 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
418418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
421522 INFO main 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
424010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
426880 INFO main 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
429839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432731 INFO main 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
435588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
438508 INFO main 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
440946 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
443781 INFO main 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
446225 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
449045 INFO main 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
451506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
454359 INFO main 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
456802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
459632 INFO main 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
462089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
464927 INFO main 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
467375 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
470198 INFO main 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
472653 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
475496 INFO main 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
477933 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
480774 INFO main 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
483217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
486048 INFO main 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
491900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
494974 INFO main 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
497550 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2959014 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arithmetic
2959015 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arrays
415 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.
454 INFO main 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
12462 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16208 INFO main 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
19028 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21870 INFO main 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
25221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28137 INFO main 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
31199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34091 INFO main 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
36762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39545 INFO main 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
45586 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45839 INFO main 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
50963 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
51330 INFO main 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
58614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3018124 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arrays
3018126 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javadl
409 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
418 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/.././standard_key/instanceCreation/instanceCreation1.key
10164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13657 INFO main 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
17346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20592 INFO main 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
23604 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26633 INFO main 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
29911 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33062 INFO main 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
36198 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39226 INFO main 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
42070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45027 INFO main 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
49176 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52438 INFO main 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
52467 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
52468 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
52468 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
55338 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55587 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
55588 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
55588 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
58253 INFO main 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
61146 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64060 INFO main 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
64087 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
64088 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
64088 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
66834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67061 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
67062 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
67062 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
69815 INFO main 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
72526 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75329 INFO main 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
78053 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80907 INFO main 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
83833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86776 INFO main 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
89699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
89942 INFO main 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
89966 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
89966 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
89967 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
92650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92881 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
92881 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
92881 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
95647 INFO main 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
95674 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
95674 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
95674 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
98608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98866 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
98866 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
98867 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
101511 INFO main 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
104230 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107036 INFO main 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
109758 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112581 INFO main 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
115302 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118081 INFO main 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
120956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123949 INFO main 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
126807 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129720 INFO main 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
132486 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
132747 INFO main 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
136292 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139416 INFO main 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
139440 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
139441 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
139441 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
142334 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142634 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
142635 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
142635 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
145253 INFO main 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
148063 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150898 INFO main 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
153686 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156582 INFO main 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
156605 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
156605 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
156606 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
159292 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
159605 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
159605 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
159606 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
162198 INFO main 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
164846 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
167662 INFO main 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
170302 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173182 INFO main 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
175820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178674 INFO main 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
181330 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
181649 INFO main 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
184486 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
187448 INFO main 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
190301 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
190698 INFO main 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
193495 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196457 INFO main 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
199178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
199506 INFO main 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
203762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
207334 INFO main 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
210604 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
213976 INFO main 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
216987 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
220169 INFO main 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
223259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
226468 INFO main 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
229233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232277 INFO main 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
235110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238089 INFO main 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
240801 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
243777 INFO main 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
373938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
381052 INFO main 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
384045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
384438 INFO main 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
387137 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
387558 INFO main 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
390423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
393485 INFO main 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
396217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
399353 INFO main 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
402081 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
405087 INFO main 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
407843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
410885 INFO main 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
415721 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
419180 INFO main 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
421800 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
424782 INFO main 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
427428 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
430360 INFO main 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
433012 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
436087 INFO main 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
438884 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
441971 INFO main 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
441995 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
441995 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
441995 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
449194 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
449732 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
449732 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
449733 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
453103 INFO main 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
453126 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
453126 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
453127 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
457325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
457947 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
457947 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
457948 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
460780 INFO main 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
463411 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
466429 INFO main 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
469121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
472094 INFO main 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
474790 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
477823 INFO main 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
485545 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
489700 INFO main 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
591480 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
595920 INFO main 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
595942 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
595942 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
595943 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
598807 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
599502 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
599503 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
599503 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
602194 INFO main 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
602217 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
602217 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
605564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
606199 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
606200 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
609060 INFO main 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
609081 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
609081 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
611767 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
612334 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
612334 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
614864 INFO main 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
614886 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
614887 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
617542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
618100 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
618101 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
620703 INFO main 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
620725 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
620725 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
623646 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
624227 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
624227 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
626807 INFO main 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
626828 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
626829 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
629673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
630238 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
630238 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
632811 INFO main 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
632834 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
632834 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
649056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
649710 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
649710 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
654470 INFO main 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
654493 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
654493 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
657432 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
658107 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
658108 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
660736 INFO main 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
663363 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
666478 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
666502 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
669259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
669874 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
672521 INFO 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
675259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
675837 INFO 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
678573 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3697512 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javadl
3697514 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test FOL
500 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
511 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
543 INFO main 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
9038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12266 INFO main 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
15168 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18237 INFO main 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
21175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24072 INFO main 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
26855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29666 INFO main 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
32361 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35154 INFO main 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
37831 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40640 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/functions.key
43349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46149 INFO main 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
48821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51578 INFO main 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
54208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56987 INFO main 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
59626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62395 INFO main 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
65030 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67722 INFO main 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
70591 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73371 INFO main 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
78853 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81767 INFO main 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
84359 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87127 INFO main 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
97795 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100570 INFO main 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
103263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106035 INFO main 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
108847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111639 INFO main 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
114273 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117078 INFO main 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
119711 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122403 INFO main 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
124979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127661 INFO main 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
130438 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133203 INFO main 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
138572 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141367 INFO main 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
143934 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
144210 INFO main 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
146777 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
147044 INFO main 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
149635 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152318 INFO main 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
154881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
157590 INFO main 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
160378 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163081 INFO main 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
165603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
168252 INFO main 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
170744 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173355 INFO main 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
175849 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178432 INFO main 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
180903 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183576 INFO main 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
186123 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
188850 INFO main 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
191374 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
194150 INFO main 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
197886 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
200664 INFO main 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
207761 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
210551 INFO main 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
213162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
215986 INFO main 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
218547 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
221278 INFO main 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
223847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
226619 INFO main 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
229161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
231931 INFO main 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
234499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
237280 INFO main 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
239821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
242591 INFO main 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
245083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
247766 INFO main 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
250236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
252923 INFO main 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
255406 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
258164 INFO main 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
260667 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
263459 INFO main 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
265978 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
268729 INFO main 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
271232 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
273995 INFO main 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
276504 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
279279 INFO main 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
281787 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
284583 INFO main 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
287054 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
289769 INFO main 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
292234 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3992699 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test FOL
3992699 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test strings
373 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
388 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
404 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/strings/charAt0.key
9011 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12098 INFO main 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
15125 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18005 INFO main 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
20780 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23567 INFO main 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
26289 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29036 INFO main 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
31656 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34426 INFO main 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
37104 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39782 INFO main 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
43541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46361 INFO main 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
49324 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52120 INFO main 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
55315 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58112 INFO main 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
60975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63735 INFO main 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
66441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69186 INFO main 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
72399 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75351 INFO main 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
77890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80627 INFO main 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
83215 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85898 INFO main 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
88599 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91327 INFO main 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
93908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96742 INFO main 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
99376 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102087 INFO main 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
104685 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107415 INFO main 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
113444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116693 INFO main 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
119312 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122011 INFO main 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
124839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127557 INFO main 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
130069 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
132663 INFO main 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
135116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
137682 INFO main 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
140153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142800 INFO main 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
145308 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
147900 INFO main 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
150354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152989 INFO main 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
155623 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4151152 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test strings
4151155 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simple_info_flow
359 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
366 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
380 INFO 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
9518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9645 INFO 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
13386 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
4164839 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simple_info_flow
4164840 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test modelMethods
367 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
372 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
392 INFO 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
8893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12195 INFO 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
15402 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18471 INFO 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
21461 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24460 INFO 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
27326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30244 INFO 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
33117 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36013 INFO 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
45003 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48615 INFO 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
51749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54701 INFO 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
57749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60722 INFO 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
66146 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69700 INFO 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
72535 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75406 INFO 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
78224 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81081 INFO 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
83877 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86843 INFO 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
89557 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92428 INFO 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
95221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98069 INFO 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
100785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103603 INFO 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
106373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109209 INFO 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
111966 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114779 INFO 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
117530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120379 INFO 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
123277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126169 INFO 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
128913 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131690 INFO 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
134390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
137211 INFO 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
139961 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142906 INFO 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
145590 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
148433 INFO 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
151177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154014 INFO 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
156754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
159586 INFO 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
162293 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
165113 INFO 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
174121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177503 INFO 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
180328 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4348254 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test modelMethods
4348255 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test permissionHeap
353 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
379 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/permissions/permissions_method0.key
9727 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13135 INFO 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
16327 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19302 INFO 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
23426 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26554 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/permissions_setAB.key
30658 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33709 INFO 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
37542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40177 INFO 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
47404 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52534 INFO 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
57373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62307 INFO 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
67125 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72080 INFO 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
76805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81640 INFO 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
87476 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92507 INFO 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
97201 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102106 INFO 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
106927 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111865 INFO 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
116773 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121700 INFO 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
136046 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141813 INFO 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
146886 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151839 INFO 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
156818 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161757 INFO 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
166417 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
171253 INFO 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
175951 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
180765 INFO 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
186229 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
191225 INFO 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
195945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
200820 INFO 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
205557 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
210413 INFO 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
215108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
220002 INFO 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
225559 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
230508 INFO 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
235241 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
240307 INFO 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
245021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
249984 INFO 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
254937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
259967 INFO 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
274551 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
280359 INFO 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
286046 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
291077 INFO 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
295964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
300923 INFO 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
305645 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
310577 INFO 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
315288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
320211 INFO 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
325419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
330497 INFO 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
335206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
340140 INFO 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
344843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
349762 INFO 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
354476 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
359444 INFO 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
364220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
369161 INFO 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
373840 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
378781 INFO 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
383484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
388458 INFO 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
393131 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
398028 INFO 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
402799 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
407797 INFO 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
412451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
417454 INFO 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
422109 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
427092 INFO 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
431808 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
436823 INFO 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
441534 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
446521 INFO 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
451214 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
456185 INFO 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
461165 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
466142 INFO 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
472530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
477976 INFO 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
482625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
487590 INFO 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
493129 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
498189 INFO 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
509808 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
515401 INFO 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
520663 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
525696 INFO 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
530440 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
535413 INFO 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
540017 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
544961 INFO 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
549553 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
554476 INFO 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
559049 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
563984 INFO 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
571672 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
577277 INFO 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
581881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
586854 INFO 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
591467 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
596480 INFO 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
601052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
606049 INFO 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
610651 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
615693 INFO 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
620687 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
625834 INFO 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
634176 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
639856 INFO 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
644512 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
649714 INFO 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
654343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
659422 INFO 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
664058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
669125 INFO 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
673770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
678805 INFO 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
682879 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
686689 INFO 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
691153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
695027 INFO 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
697973 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
701093 INFO 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
703754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
707010 INFO 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
709923 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
713114 INFO 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
715929 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
719087 INFO 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
723385 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
727327 INFO 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
732366 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
736509 INFO 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
739885 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
743763 INFO 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
747140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
750891 INFO 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
754161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
757853 INFO 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
761097 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
764813 INFO 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
768057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
771797 INFO 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
775097 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
778847 INFO 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
782100 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
785806 INFO 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
789080 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
792849 INFO 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
796392 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
800373 INFO 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
803590 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
807358 INFO 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
810866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
814704 INFO 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
818245 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
822070 INFO 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
826848 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
826849 INFO 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
831703 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
831704 INFO 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
836560 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
836563 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
836565 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
836566 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
836567 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
836569 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
836571 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
836573 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
836575 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
836580 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
836581 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
836582 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
836583 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
836586 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
836589 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
836590 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
836591 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
836592 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
836593 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
836594 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
836595 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
836595 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
836715 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
5186308 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test permissionHeap
5186309 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test completionScopes
409 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
409 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/.././completionscopes/testCcatchReturnVal.key
8739 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11663 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
14757 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17706 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
20557 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23347 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
25966 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28702 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
31344 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34032 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
36626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39294 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
41906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44526 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
47103 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5236222 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test completionScopes
5236223 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test reload_examples
407 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
423 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
440 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
18683 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23194 INFO main 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
25949 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
25949 INFO 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
29818 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
29820 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
33567 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
33568 INFO 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
36827 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
36828 INFO 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
40533 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
40534 INFO 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
43893 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
5280322 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test reload_examples
5280323 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test proofLoadRepair
344 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
356 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
371 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././proofLoadRepair/disjConj-manipulated.proof
8149 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft
8150 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right
8154 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close
8159 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
8165 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
10818 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for applyEq
10838 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
10839 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
13546 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
13547 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
15991 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
15992 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
18382 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
5298875 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test proofLoadRepair
5298876 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test switch
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.
431 INFO main 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
9647 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12974 INFO main 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
15849 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18757 INFO main 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
21606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24392 INFO main 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
27216 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30008 INFO main 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
32738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35551 INFO main 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
38335 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41074 INFO main 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
48002 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51425 INFO main 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
54917 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57905 INFO main 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
61817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5364017 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test switch
5364018 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test redux
340 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
342 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
356 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
13973 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18060 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
21426 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
25817 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
25910 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 17 in 65ms, result is valid
25913 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
27717 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31726 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
39223 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43196 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
46240 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
51971 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
52035 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 27 in 60ms, result is valid
52036 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
55408 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59576 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
63095 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66345 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
69535 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72657 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
75833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78995 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
82467 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85675 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
89331 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92540 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
101582 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105714 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
109131 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112371 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
121294 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5490212 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test redux
5490254 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
5490256 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
5490256 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
5490256 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
5490256 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
5490256 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
5490256 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
5490256 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
5490262 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
5490262 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
5490262 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
5490262 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
5490263 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
5490263 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
5490263 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
5490263 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
5490263 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