492 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test newBook
389 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
403 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)
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/.././newBook/09.list_modelfield/ArrayList.add.key
25392 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30068 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
37134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40733 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
44358 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47361 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
50451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53355 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
56918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60601 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test newBook
60605 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test oldBook
347 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.
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/.././standard_key/BookExamples/02FirstOrderLogic/Ex2.58.key
7530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10269 INFO main 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
13359 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76777 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test oldBook
76779 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test comprehensions
362 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.
385 INFO 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
8368 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11365 INFO 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
14823 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17837 INFO 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
20941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23773 INFO 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
26799 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29640 INFO 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
32647 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35453 INFO 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
38415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41178 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/bsum_negative.key
43666 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46239 INFO 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
48779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51302 INFO 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
53802 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56366 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/bprodSplit.key
58847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61371 INFO 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
63817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
140965 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test comprehensions
140968 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performance
369 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
375 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/.././performance-test/Disjoint(Disjoint__disjoint_08()).JML_operation_contract.0.key
18845 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29482 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
40023 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49822 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
61704 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71746 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
86970 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97436 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
107639 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117288 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
131710 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141780 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
155088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
165248 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
176420 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
186281 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
198395 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
349458 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performance
349459 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performancePOConstruction
346 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
355 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
368 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Test(Test__a0(int)).JML_normal_behavior_operation_contract.0.key
18088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29347 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
40445 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51317 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
62040 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
422313 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performancePOConstruction
422316 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test applicationRestrictions
366 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.
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/polarity_tests/wellformed1.key
7844 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10729 INFO 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
13524 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
13652 INFO 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
16379 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19096 INFO 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
21736 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
21880 INFO 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
24513 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27154 INFO 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
29768 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29883 INFO 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
32497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35166 INFO 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
37753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37882 INFO 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
40500 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43133 INFO 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
45708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45835 INFO 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
48384 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
470994 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test applicationRestrictions
470996 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test blockContracts
364 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.
414 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__add.key
9484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12863 INFO 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
16932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20299 INFO 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
23389 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26483 INFO 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
29660 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32732 INFO 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
37600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40879 INFO 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
43836 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46893 INFO 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
50036 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53110 INFO 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
56009 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59027 INFO 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
61916 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64873 INFO main 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
67497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70131 INFO main 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
72733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75323 INFO 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
78148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81013 INFO 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
84419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87508 INFO 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
91027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94137 INFO 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
96940 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99829 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_loop_contracts/SimpleVariants/sum_onLoop_internal.key
103107 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106238 INFO 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
109631 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112801 INFO 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
115230 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117789 INFO 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
120253 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122818 INFO 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
125668 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
125922 INFO 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
128832 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
600241 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test blockContracts
600243 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test jmlAsserts
366 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/.././standard_key/java_dl/jml-assert/assert.key
8947 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12040 INFO 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
14743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17363 INFO 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
19956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22521 INFO main 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
25300 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28082 INFO main 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
30871 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33562 INFO main 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
36277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38939 INFO main 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
41554 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44291 INFO main 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
46858 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49529 INFO main 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
52127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54739 INFO main 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
57306 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59914 INFO main 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
62503 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65142 INFO main 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
67639 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70199 INFO main 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
72711 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75253 INFO main 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
77874 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80446 INFO main 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
82979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
685961 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test jmlAsserts
685965 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javaCard
337 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.
354 INFO 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
8081 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10076 INFO 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
12275 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14088 INFO 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
16722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18565 INFO 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
21180 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22969 INFO 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
27907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
716494 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javaCard
716495 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key
348 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
370 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
393 INFO 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
27322 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
748193 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key
748195 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#1
334 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
354 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/.././heap/verifyThis11_1_Maximum/project.key
9656 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
761320 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#1
761321 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test lcp.key
317 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
319 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
332 INFO 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
10655 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
775881 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test lcp.key
775882 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#2
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/.././heap/SemanticSlicing/project.key
14564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
794662 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#2
794664 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_contains.key
347 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
367 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/.././heap/information_flow/ArrayList_contains.key
9716 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
808019 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_contains.key
808020 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_get.key
368 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.
415 INFO 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
10343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
822072 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_get.key
822073 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_size.key
358 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.
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/information_flow/ArrayList_size.key
8879 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
834434 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_size.key
834436 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_3_secure.key
353 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
357 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
396 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_3_secure.key
9320 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
847399 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_3_secure.key
847400 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_4_secure.key
351 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.
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/information_flow/UpdateAbstraction_ex7_4_secure.key
9219 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
860143 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_4_secure.key
860144 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_5_secure.key
339 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
348 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
364 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_5_secure.key
9060 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
872549 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_5_secure.key
872551 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_6_secure.key
308 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
326 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
354 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_6_secure.key
9602 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
885709 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_6_secure.key
885710 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex9_secure.key
384 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
411 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
427 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex9_secure.key
10590 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
899763 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex9_secure.key
899764 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list
352 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.
384 INFO 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
14135 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18711 INFO 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
23326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26857 INFO 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
53705 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59135 INFO 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
64953 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68643 INFO 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
73901 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77502 INFO 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
80712 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83893 INFO 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
87255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90476 INFO 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
94587 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97943 INFO 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
101321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104581 INFO 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
107822 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110981 INFO 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
114441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117657 INFO 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
120805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123973 INFO 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
127119 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130326 INFO 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
133863 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
137123 INFO 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
140388 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143583 INFO 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
146931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150121 INFO 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
153987 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
157246 INFO 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
160259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163360 INFO 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
167110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170425 INFO 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
174209 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177540 INFO 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
180591 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183720 INFO 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
186923 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190116 INFO 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
193153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196380 INFO 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
201249 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
204785 INFO 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
212950 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
216641 INFO 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
220145 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
223438 INFO 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
226841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
230032 INFO 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
233354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
236553 INFO 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
239665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
242863 INFO 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
247959 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1151431 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list
1151432 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_ghost
356 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
360 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
373 INFO 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
12345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16090 INFO 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
19884 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22887 INFO 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
27565 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30740 INFO 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
33665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36452 INFO 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
39771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42673 INFO 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
45453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48220 INFO 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
50839 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53545 INFO 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
56151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58880 INFO 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
61491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1215778 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_ghost
1215779 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_recursive
327 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
334 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/.././heap/list_recursiveSpec/ListOperationsNonNull_getNextNN_normal_behavior.key
9099 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12456 INFO 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
15369 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
17734 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'macro simp-upd'
17741 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'rule observerDependencyEQ'
17762 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'tryclose'
17785 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1236767 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_recursive
1236768 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_seq
370 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.
420 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/SimplifiedLinkedList.remove.key
64879 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72071 INFO 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
76052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79504 INFO 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
85576 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89253 INFO 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
93659 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97097 INFO 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
102011 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105580 INFO 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
109160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112465 INFO 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
115682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118951 INFO 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
123759 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127435 INFO 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
141039 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1382599 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_seq
1382600 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test observer
342 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.
374 INFO 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
9415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12780 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_inv.key
15955 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18986 INFO 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
21970 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24902 INFO 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
28043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31167 INFO 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
34121 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37110 INFO 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
40054 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43050 INFO 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
50915 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54699 INFO 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
58037 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61147 INFO 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
64894 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68062 INFO 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
70982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73992 INFO 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
77815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80945 INFO 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
83836 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86805 INFO 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
89730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92732 INFO 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
95698 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1481429 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test observer
1481430 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test removeDups
320 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
331 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
355 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/removeDups/arrayPart.key
10871 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14248 INFO 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
17694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20703 INFO 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
34367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1520209 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test removeDups
1520211 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test Saddleback_search.key
352 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
360 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
373 INFO 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
81088 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1608209 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test Saddleback_search.key
1608210 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test quicksort
306 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
312 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
324 INFO 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
9270 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12493 INFO 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
15426 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'script 'sort.script''
15432 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
15432 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
16473 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'select formula="{heapAtPre:=heap || exc:=null || heap:=heapAfter_sort_0}
seq ...'
16489 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
16509 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'let @seqPre="seqDef{int u;}(0, array.length, array[u])"
@seqSplit="seqDef ...'
16511 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule seqPermSym
formula="seqPerm(@seqSplit, @seqPre)"'
16536 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'rule seqPermSym
formula="seqPerm(@seqSort, @seqSplit)"'
16545 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'rule seqPermSym
formula="seqPerm(@seqSort0, @seqSort)"'
16546 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSplit)"'
16547 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSort)"'
16550 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'rule seqPermSym
formula="seqPerm(@seqPre, @seqSort0)"'
16551 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose'
39341 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44214 INFO 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
47092 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
48224 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'tryclose'
80301 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
80420 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'rule seqPermFromSwap'
80437 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule andRight'
80439 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'auto'
80469 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'instantiate hide var=iv with=i_0'
80474 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'instantiate hide var=jv with=j_0'
80476 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'auto'
86181 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'macro simp-upd'
86249 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'rule seqPermFromSwap'
86252 INFO main d.u.i.k.m.s.ProofScriptEngine 12: 'rule andRight'
86257 INFO main d.u.i.k.m.s.ProofScriptEngine 13: 'auto'
86272 INFO main d.u.i.k.m.s.ProofScriptEngine 14: 'instantiate hide var=iv with=i_0'
86279 INFO main d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate hide var=jv with=to'
86281 INFO main d.u.i.k.m.s.ProofScriptEngine 16: 'auto'
90803 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1705515 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test quicksort
1705516 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simpleTests
365 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
365 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
390 INFO 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
7754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10538 INFO 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
13747 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16612 INFO 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
19288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21857 INFO 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
24353 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26958 INFO 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
29452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31978 INFO 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
35464 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38445 INFO 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
40973 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43512 INFO 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
47453 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50453 INFO 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
53329 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56160 INFO 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
58640 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61150 INFO 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
63924 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66718 INFO 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
70035 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72926 INFO 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
75398 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77921 INFO 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
80366 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82913 INFO 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
85473 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88029 INFO 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
91432 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94387 INFO 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
96867 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99383 INFO 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
105386 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108808 INFO 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
111580 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114187 INFO 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
116982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119824 INFO 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
122519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125363 INFO 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
127995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130655 INFO 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
133317 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135991 INFO 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
138663 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141459 INFO main 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
143898 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146426 INFO 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
148936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151565 INFO 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
154048 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1860007 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simpleTests
1860008 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SmansEtAl
381 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.
429 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SmansEtAl/ArrayList_add.key
15688 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19966 INFO 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
23711 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26770 INFO 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
29574 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32369 INFO 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
35437 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38309 INFO 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
41126 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43930 INFO 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
46626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49380 INFO 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
52058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54813 INFO 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
57514 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60247 INFO 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
63062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65839 INFO 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
68547 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71320 INFO 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
74006 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76798 INFO 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
79469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82194 INFO 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
84864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87656 INFO 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
90306 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93054 INFO 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
96138 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
98952 INFO 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
101614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104379 INFO 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
107498 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110361 INFO 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
113418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116223 INFO 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
118989 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121744 INFO 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
125475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128378 INFO 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
131028 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133765 INFO 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
136401 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139154 INFO 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
144013 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
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/.././heap/SmansEtAl/Stack_footprint.key
149811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152587 INFO 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
155201 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
157955 INFO 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
161087 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163972 INFO 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
166726 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169549 INFO 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
172994 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
175930 INFO 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
182474 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2045887 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SmansEtAl
2045888 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VACID0
366 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
373 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
391 INFO 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
9941 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13176 INFO 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
25517 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29539 INFO 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
33269 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36299 INFO 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
39548 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42447 INFO 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
48152 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51254 INFO 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
55879 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58929 INFO 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
63366 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66214 INFO 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
72182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2121471 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VACID0
2121472 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VSTTE10
342 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
350 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
363 INFO 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
12589 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16478 INFO 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
20882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24011 INFO 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
27075 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29908 INFO 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
37827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41250 INFO 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
45816 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49080 INFO 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
63172 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67099 INFO 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
71225 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74313 INFO 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
77419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80301 INFO 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
90495 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94159 INFO 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
98934 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102048 INFO 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
104829 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107708 INFO 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
110657 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113521 INFO 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
116257 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119090 INFO 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
123356 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126432 INFO 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
130732 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133816 INFO 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
147454 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151506 INFO 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
162154 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
165838 INFO 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
168994 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2293573 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VSTTE10
2293574 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test WeideEtAl
354 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.
385 INFO 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
9120 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12290 INFO 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
15334 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18028 INFO 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
23333 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2320095 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test WeideEtAl
2320096 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arithmetic
396 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
400 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
413 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/binomial1.key
7880 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10906 INFO main 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
13771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16564 INFO main 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
24142 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27333 INFO main 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
30032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32736 INFO main 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
38490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41435 INFO main 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
44465 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47243 INFO main 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
49873 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52580 INFO main 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
55236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57886 INFO main 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
61906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64740 INFO main 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
68354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71346 INFO main 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
74077 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76810 INFO main 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
80001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82689 INFO main 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
85289 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87966 INFO main 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
93731 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96700 INFO main 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
138321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144932 INFO main 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
147681 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150463 INFO main 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
166795 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170661 INFO main 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
173265 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
175982 INFO main 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
178535 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
181159 INFO main 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
183724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
186372 INFO main 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
193094 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196204 INFO main 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
198783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
201493 INFO main 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
204044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
206703 INFO main 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
211068 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
213817 INFO main 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
216397 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
219080 INFO main 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
221617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
224280 INFO main 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
226854 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
229532 INFO main 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
232089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
234751 INFO main 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
237315 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
239983 INFO main 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
242633 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
245345 INFO main 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
247990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
250696 INFO main 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
253236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
255929 INFO main 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
258673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
261412 INFO main 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
264050 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
266783 INFO main 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
269438 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
272169 INFO main 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
274827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
277581 INFO main 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
280124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
282836 INFO main 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
285387 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
288096 INFO main 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
290647 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
293367 INFO main 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
295907 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
298641 INFO main 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
301185 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
303919 INFO main 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
306459 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
309190 INFO main 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
311737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
314489 INFO main 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
317071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
319852 INFO main 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
322392 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
325147 INFO main 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
327699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
330475 INFO main 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
333026 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
335786 INFO main 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
338346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
341142 INFO main 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
344104 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
347141 INFO main 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
349815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
352584 INFO main 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
355238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
358142 INFO main 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
361013 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
363935 INFO main 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
366836 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
369836 INFO main 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
372483 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
375303 INFO main 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
377824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
380637 INFO main 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
383213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
386004 INFO main 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
388532 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
391318 INFO main 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
393827 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
396615 INFO main 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
399139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
401926 INFO main 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
404448 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
407256 INFO main 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
409875 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
412701 INFO main 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
417736 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
420843 INFO main 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
423380 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
426241 INFO main 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
429257 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432180 INFO main 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
435129 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
438073 INFO main 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
440599 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
443457 INFO main 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
445984 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
448882 INFO main 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
451398 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
454236 INFO main 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
456758 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
459602 INFO main 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
462114 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
464970 INFO main 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
467502 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
470368 INFO main 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
472887 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
475766 INFO main 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
478283 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
481150 INFO main 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
483674 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
486540 INFO main 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
492502 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
495714 INFO main 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
498443 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2821640 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arithmetic
2821642 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arrays
348 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
353 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
369 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/array2DimPrim.key
11309 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14857 INFO main 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
17674 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20395 INFO main 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
23438 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/.././standard_key/arrays/arrayStoreException/throwArrayStoreException.key
29118 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31805 INFO main 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
34353 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36910 INFO main 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
42452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
42672 INFO main 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
47167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47485 INFO main 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
54009 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2876104 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arrays
2876105 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javadl
394 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
400 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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/.././standard_key/instanceCreation/instanceCreation1.key
8508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11555 INFO main 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
14724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17665 INFO main 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
20384 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23034 INFO main 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
25908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28577 INFO main 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
31286 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33977 INFO main 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
36521 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39107 INFO main 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
43113 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45979 INFO main 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
46004 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
46005 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
46005 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
48536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48745 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
48745 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
48745 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
51155 INFO main 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
53767 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56358 INFO main 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
56378 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
56379 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
56379 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
58862 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59063 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
59063 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
59064 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
61437 INFO main 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
63872 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66348 INFO main 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
68908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71458 INFO main 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
74136 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76885 INFO main 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
79448 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
79668 INFO main 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
79690 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
79690 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
79691 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
82120 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82327 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
82328 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
82328 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
84694 INFO main 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
84714 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
84715 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
84715 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
87260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87481 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
87481 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
87481 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
89957 INFO main 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
92380 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94898 INFO main 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
97335 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99848 INFO main 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
102268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104794 INFO main 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
107391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110011 INFO main 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
112620 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115238 INFO main 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
117731 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
117948 INFO main 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
121116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123947 INFO main 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
123967 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
123967 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
123968 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
126513 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126773 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
126773 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
126774 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
129122 INFO main 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
131528 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134067 INFO main 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
136481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139321 INFO main 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
139341 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
139341 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
139341 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
141780 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142057 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
142057 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
142057 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
144387 INFO main 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
146779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
149332 INFO main 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
151716 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154269 INFO main 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
156648 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
159162 INFO main 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
161544 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
161833 INFO main 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
164394 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166996 INFO main 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
169447 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
169729 INFO main 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
172255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
174920 INFO main 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
177367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
177680 INFO main 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
181367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
184515 INFO main 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
187536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190502 INFO main 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
193238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196099 INFO main 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
198805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
201668 INFO main 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
204219 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
206912 INFO main 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
209473 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
212139 INFO main 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
214584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
217250 INFO main 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
338519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
344758 INFO main 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
347295 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
347776 INFO main 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
350207 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
350542 INFO main 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
352964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
355747 INFO main 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
358160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
360822 INFO main 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
363238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
365908 INFO main 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
368324 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
371007 INFO main 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
375273 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
378337 INFO main 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
380718 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
383433 INFO main 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
385841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
388460 INFO main 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
390898 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
393613 INFO main 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
396151 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
398924 INFO main 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
398944 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
398945 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
398945 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
405432 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
405901 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
405902 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
405902 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
408984 INFO main 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
409004 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
409005 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
409005 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
412714 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
413207 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
413207 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
413207 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
415775 INFO main 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
418160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
420842 INFO main 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
423206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
425848 INFO main 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
428275 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
431029 INFO main 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
438147 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
441852 INFO main 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
534860 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
538797 INFO main 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
538815 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
538815 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
538815 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
541527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
542084 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
542085 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
542085 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
544497 INFO main 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
544516 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
544516 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
547444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
547958 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
547959 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
550378 INFO main 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
550396 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
550396 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
552821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
553317 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
553317 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
555599 INFO main 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
555617 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
555617 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
558089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
558548 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
558548 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
560833 INFO main 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
560850 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
560850 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
563356 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
563833 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
563834 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
566167 INFO main 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
566185 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
566186 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
568762 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
569262 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
569262 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
571590 INFO main 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
571608 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
571608 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
585937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
586488 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
586489 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
590855 INFO main 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
590874 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
590874 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
593615 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
594169 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
594169 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
596611 INFO main 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
598963 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
601665 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
601686 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
604172 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
604672 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
607032 INFO 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
609485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
609989 INFO 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
612413 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3489210 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javadl
3489211 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test FOL
353 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.
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/.././standard_key/pred_log/count.key
8056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10871 INFO main 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
13508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16111 INFO main 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
18684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21254 INFO main 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
23776 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26279 INFO main 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
28764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31255 INFO main 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
33746 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36238 INFO main 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
38693 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41181 INFO main 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
43616 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46146 INFO main 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
48565 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51111 INFO main 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
53536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55989 INFO main 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
58416 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60867 INFO main 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
63508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66043 INFO main 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
71267 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73879 INFO main 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
76288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78817 INFO main 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
89113 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91661 INFO main 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
94059 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/.././standard_key/pred_log/tptp/SET/SET043p1.key
98932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101410 INFO main 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
103780 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106255 INFO main 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
108660 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111155 INFO main 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
113564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116039 INFO main 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
118544 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121106 INFO main 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
126101 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128673 INFO main 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
131062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
131284 INFO main 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
133635 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
133884 INFO main 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
136246 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138775 INFO main 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
141231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143781 INFO main 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
146288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
148861 INFO main 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
151244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
153809 INFO main 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
156177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
158671 INFO main 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
161044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163541 INFO main 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
165906 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
168398 INFO main 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
170771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173339 INFO main 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
175699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178306 INFO main 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
181889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
184466 INFO main 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
191255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
193864 INFO main 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
196349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
198949 INFO main 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
201318 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
203847 INFO main 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
206220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
208780 INFO main 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
211146 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
213690 INFO main 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
216061 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
218606 INFO main 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
220981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
223523 INFO main 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
225896 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
228452 INFO main 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
230828 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
233382 INFO main 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
235747 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238334 INFO main 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
240706 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
243278 INFO main 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
245648 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
248225 INFO main 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
250588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
253166 INFO main 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
255539 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
258130 INFO main 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
260513 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
263101 INFO main 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
265471 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
268059 INFO main 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
270431 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3762411 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test FOL
3762412 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test strings
327 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
331 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
345 INFO main 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
7749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10601 INFO main 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
13378 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16086 INFO main 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
18749 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21362 INFO main 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
23908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26508 INFO main 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
29061 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31639 INFO main 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
34177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36722 INFO main 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
39995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42738 INFO main 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
45477 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48102 INFO main 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
51011 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53652 INFO main 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
56313 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58936 INFO main 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
61549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64169 INFO main 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
67169 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69987 INFO main 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
72501 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75054 INFO main 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
77553 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80144 INFO main 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
82630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85260 INFO main 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
87761 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90332 INFO main 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
92929 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95511 INFO main 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
98001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100580 INFO main 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
105541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108619 INFO main 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
111130 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113705 INFO main 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
116377 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118992 INFO main 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
121463 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124051 INFO main 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
126513 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129067 INFO main 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
131525 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134087 INFO main 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
136573 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139153 INFO main 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
141600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144164 INFO main 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
146833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3912066 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test strings
3912067 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simple_info_flow
358 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
360 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/information_flow/UpdateAbstraction_ex7_1_insecure.key
9059 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9164 INFO 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
12481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3924883 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simple_info_flow
3924884 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test modelMethods
352 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.
390 INFO 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
8820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11861 INFO 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
14743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17522 INFO 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
20303 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23016 INFO 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
25630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28297 INFO 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
30908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33536 INFO 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
41556 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44791 INFO 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
47530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50185 INFO 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
52974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55682 INFO 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
60636 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63758 INFO 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
66338 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68938 INFO 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
71572 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74194 INFO 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
76718 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79350 INFO 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
81870 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84542 INFO 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
87050 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89657 INFO 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
92204 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94801 INFO 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
97332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99962 INFO 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
102494 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105083 INFO 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
107614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110261 INFO 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
112882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115584 INFO 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
118123 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120734 INFO 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
123233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125836 INFO 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
128354 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131064 INFO 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
133627 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
136384 INFO 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
138860 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141468 INFO 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
143985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146597 INFO 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
149102 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151739 INFO 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
160089 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163222 INFO 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
165739 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4093482 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test modelMethods
4093484 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test permissionHeap
350 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.
368 INFO 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
8595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11620 INFO 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
14742 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17612 INFO 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
21486 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24432 INFO 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
28290 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31162 INFO 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
34564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37032 INFO 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
43563 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48369 INFO 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
52969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57569 INFO 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
62132 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66733 INFO 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
71245 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75810 INFO 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
81234 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85977 INFO 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
90441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94983 INFO 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
99530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104082 INFO 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
108829 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113517 INFO 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
126426 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
131737 INFO 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
136616 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141252 INFO 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
145938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150536 INFO 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
155029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
159634 INFO 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
164137 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
168706 INFO 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
174014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178749 INFO 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
183225 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
187821 INFO 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
192270 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196848 INFO 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
201284 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
205860 INFO 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
211206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
215916 INFO 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
220406 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
225030 INFO 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
229509 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
234101 INFO 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
238745 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
243399 INFO 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
256585 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
261895 INFO 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
267242 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
271935 INFO 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
276581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
281234 INFO 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
285694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
290305 INFO 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
294758 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
299382 INFO 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
304320 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
309069 INFO 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
313530 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
318164 INFO 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
322658 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
327272 INFO 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
331707 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
336341 INFO 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
340866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
345533 INFO 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
349975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
354625 INFO 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
359054 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
363721 INFO 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
368179 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
372860 INFO 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
377410 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
382118 INFO 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
386569 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
391245 INFO 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
395684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
400359 INFO 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
404900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
409597 INFO 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
414201 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
419089 INFO 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
423858 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
428642 INFO 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
433054 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
437735 INFO 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
443636 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
448556 INFO 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
452977 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
457668 INFO 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
462881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
467663 INFO 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
478696 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
483974 INFO 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
488939 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
493716 INFO 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
498164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
502878 INFO 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
507293 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
512020 INFO 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
516432 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
521170 INFO 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
525574 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
530294 INFO 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
537500 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
542750 INFO 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
547170 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
551927 INFO 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
556342 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
561082 INFO 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
565491 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
570240 INFO 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
574647 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
579435 INFO 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
584244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
589097 INFO 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
596991 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
602315 INFO 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
606795 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
611563 INFO 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
615980 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
620767 INFO 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
625175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
629968 INFO 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
634443 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
639247 INFO 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
643116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
646646 INFO 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
651447 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
654985 INFO 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
657681 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
660688 INFO 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
663315 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
666387 INFO 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
669134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
672142 INFO 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
674779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
677798 INFO 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
681864 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
685651 INFO 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
690469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
694363 INFO 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
697451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
700975 INFO 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
704057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
707633 INFO 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
710728 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
714193 INFO 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
717467 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
721094 INFO 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
724208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
727807 INFO 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
731037 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
734625 INFO 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
737712 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
741267 INFO 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
744371 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
747876 INFO 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
751286 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
754982 INFO 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
758107 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
761668 INFO 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
764974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
768587 INFO 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
771877 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
775504 INFO 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
780066 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
780067 INFO 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
784723 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
784724 INFO 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
789348 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
789350 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
789352 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
789353 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
789353 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
789355 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
789356 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
789357 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
789359 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
789360 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
789361 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
789361 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
789362 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
789362 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
789363 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
789364 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
789364 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
789365 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
789366 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
789366 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
789367 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
789367 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
789440 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
4883102 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test permissionHeap
4883102 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test completionScopes
332 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
337 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
362 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
8349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11192 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
14214 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16923 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
19614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22112 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
24549 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27015 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
29470 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31921 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
34362 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36835 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
39237 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41658 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
44041 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4929713 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test completionScopes
4929714 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test reload_examples
394 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
408 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
436 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
17551 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21825 INFO main 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
24284 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
24285 INFO 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
27980 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
27981 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
31620 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
31622 INFO 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
34565 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
34566 INFO 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
38084 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
38085 INFO 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
41238 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
4971111 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test reload_examples
4971112 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test proofLoadRepair
332 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
332 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
346 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
7302 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft
7303 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right
7306 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close
7310 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
7314 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
10009 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for applyEq
10020 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
10021 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
12501 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
12503 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
14886 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
14887 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
17185 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
4988469 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test proofLoadRepair
4988470 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test switch
375 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
389 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
406 INFO main 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
8512 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11644 INFO main 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
14345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17033 INFO main 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
19788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22449 INFO main 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
25036 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27759 INFO main 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
30449 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33186 INFO main 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
35882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38582 INFO main 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
45020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48284 INFO main 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
51543 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54369 INFO main 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
58085 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5049861 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test switch
5049862 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test redux
324 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
332 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
357 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
13999 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18016 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
21456 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
25164 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
25227 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 17 in 39ms, result is valid
25228 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
26755 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30748 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
38135 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41995 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
45284 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
50594 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
50642 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 27 in 34ms, result is valid
50642 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
53798 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58044 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
61743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65153 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
68473 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71745 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
75038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78307 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
81910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85258 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
88929 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92281 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
100975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105036 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
108374 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111698 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
120258 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5175014 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test redux
5175055 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
5175056 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
5175056 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
5175056 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
5175056 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
5175056 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
5175056 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
5175057 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
5175057 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
5175057 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
5175057 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
5175057 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
5175057 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
5175057 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
5175057 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
5175057 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
5175058 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