527 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test newBook
372 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 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)
439 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././newBook/09.list_modelfield/ArrayList.add.key
26003 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30750 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
38113 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41906 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
45688 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48793 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
51981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54883 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
58493 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62254 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test newBook
62269 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test oldBook
363 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.
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/.././standard_key/BookExamples/02FirstOrderLogic/Ex2.58.key
8653 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11746 INFO main 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
14942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80357 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test oldBook
80360 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test comprehensions
376 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
387 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
407 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/general_sum.key
8761 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11773 INFO 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
15420 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18388 INFO 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
21594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24475 INFO 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
27440 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30258 INFO 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
33202 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36029 INFO 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
38969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41773 INFO 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
44249 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46747 INFO 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
49180 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51673 INFO 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
54077 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56585 INFO 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
59027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61531 INFO 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
63968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
144679 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test comprehensions
144681 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performance
370 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
374 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
399 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Disjoint(Disjoint__disjoint_08()).JML_operation_contract.0.key
19791 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30910 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
42236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52644 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
65358 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75944 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
92282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103486 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
114455 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124689 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
140032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150738 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
165123 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
175825 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
187704 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
198180 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
211092 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
366496 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performance
366501 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performancePOConstruction
341 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.
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/.././performance-test/Test(Test__a0(int)).JML_normal_behavior_operation_contract.0.key
18032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29473 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
40705 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51721 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
62609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
440185 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performancePOConstruction
440187 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test applicationRestrictions
363 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
362 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
388 INFO 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
8103 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11048 INFO 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
13754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
13872 INFO 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
16581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19284 INFO 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
21881 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
22016 INFO 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
24661 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27282 INFO 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
29922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
30090 INFO 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
32675 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35299 INFO 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
37863 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
38016 INFO 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
40606 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43247 INFO 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
45789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45950 INFO 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
48481 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
488986 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test applicationRestrictions
488987 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test blockContracts
403 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
420 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/.././heap/block_contracts/Simple__add.key
9622 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13399 INFO 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
17996 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21689 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/block_contracts/Simple__addWithJump.key
25246 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28709 INFO 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
32084 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35494 INFO 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
40716 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44454 INFO 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
47714 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51085 INFO 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
54518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57941 INFO 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
61122 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64461 INFO 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
67674 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71010 INFO main 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
73980 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76962 INFO main 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
79845 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82777 INFO 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
85942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89087 INFO 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
92658 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96042 INFO 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
99805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103239 INFO 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
106254 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109460 INFO 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
112967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116333 INFO 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
119979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123380 INFO 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
126058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128889 INFO 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
131576 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134392 INFO 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
137506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
137800 INFO 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
140926 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
630475 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test blockContracts
630477 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test jmlAsserts
367 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
376 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
389 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert.key
9425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12720 INFO 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
15824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18675 INFO 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
21461 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24322 INFO main 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
27292 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30238 INFO main 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
33225 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36119 INFO main 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
38933 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41779 INFO main 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
44592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47411 INFO main 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
50286 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53158 INFO main 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
55944 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58845 INFO main 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
61629 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64461 INFO main 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
67233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70074 INFO main 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
72845 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75603 INFO main 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
78297 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81095 INFO main 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
83753 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86540 INFO main 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
89213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
722641 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test jmlAsserts
722642 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javaCard
358 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
368 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/javacard/updateBalance0.key
8390 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10559 INFO 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
12936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14945 INFO 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
17648 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19610 INFO 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
22345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24290 INFO 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
29838 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
755349 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javaCard
755355 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key
381 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
394 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
407 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/coincidence_count/project.key
28141 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
788069 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key
788072 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#1
373 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.
399 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/verifyThis11_1_Maximum/project.key
10459 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
802163 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#1
802164 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test lcp.key
346 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.
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/fm12_01_LRS/lcp.key
11621 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
817934 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test lcp.key
817935 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#2
323 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.
348 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SemanticSlicing/project.key
14576 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
837076 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#2
837078 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_contains.key
335 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
339 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/ArrayList_contains.key
9652 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
850424 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_contains.key
850425 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_get.key
371 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.
396 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/ArrayList_get.key
11383 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
865653 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_get.key
865654 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_size.key
356 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.
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/information_flow/ArrayList_size.key
9581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
878746 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_size.key
878747 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_3_secure.key
333 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
351 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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/information_flow/UpdateAbstraction_ex7_3_secure.key
9424 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
891708 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_3_secure.key
891709 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_4_secure.key
357 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.
392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_4_secure.key
9887 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
905187 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_4_secure.key
905188 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_5_secure.key
341 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.
361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_5_secure.key
9205 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
918048 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_5_secure.key
918049 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_6_secure.key
363 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.
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/UpdateAbstraction_ex7_6_secure.key
9739 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
931568 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_6_secure.key
931570 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex9_secure.key
364 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
368 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
395 INFO 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
10758 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
946272 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex9_secure.key
946274 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list
350 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
364 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
377 INFO 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
14623 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19511 INFO 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
24282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27876 INFO 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
55725 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61528 INFO 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
67653 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71513 INFO 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
76948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80730 INFO 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
83942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87186 INFO 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
90690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94066 INFO 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
98363 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101933 INFO 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
105370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108750 INFO 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
112227 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115566 INFO 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
119128 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122495 INFO 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
125752 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129063 INFO 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
132286 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135575 INFO 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
139259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142642 INFO 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
146014 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
149333 INFO 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
152778 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156116 INFO 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
160045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163432 INFO 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
166585 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169835 INFO 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
173651 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177070 INFO 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
181029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
184497 INFO 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
187626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190913 INFO 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
194227 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
197563 INFO 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
200698 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
204127 INFO 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
209218 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
212827 INFO 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
221266 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
225107 INFO 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
228622 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232050 INFO 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
235542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238908 INFO 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
242316 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
245663 INFO 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
248958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
252304 INFO 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
257595 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1207766 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list
1207768 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_ghost
352 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
361 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
380 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_ghost/ArrayList_add.key
12857 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16913 INFO 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
20824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24051 INFO 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
28958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32395 INFO 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
35550 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38585 INFO 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
42039 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45107 INFO 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
48052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51030 INFO 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
53857 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56732 INFO 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
59542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62431 INFO 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
65244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1276032 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_ghost
1276034 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_recursive
374 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
381 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
402 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_recursiveSpec/ListOperationsNonNull_getNextNN_normal_behavior.key
10256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13771 INFO 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
16870 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
19341 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'macro simp-upd'
19348 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'rule observerDependencyEQ'
19366 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'tryclose'
19409 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1298810 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_recursive
1298811 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.)
401 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
419 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/SimplifiedLinkedList.remove.key
67176 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74261 INFO 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
78598 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82070 INFO 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
88418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92118 INFO 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
96611 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100102 INFO 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
105135 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/.././heap/list_seq/ArrayList.get.key
112076 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115288 INFO 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
118508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121662 INFO 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
126541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130207 INFO 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
144496 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1448213 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_seq
1448215 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test observer
357 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
363 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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/observer/ExampleObserver_ExampleObserver.key
9868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13273 INFO 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
16294 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19326 INFO 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
22203 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25159 INFO 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
28299 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31276 INFO 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
34119 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37013 INFO 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
39834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42734 INFO 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
51041 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54637 INFO 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
57899 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60840 INFO 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
64520 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67543 INFO 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
70332 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73261 INFO 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
76968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79956 INFO 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
82711 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85526 INFO 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
88241 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91096 INFO 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
93788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1545178 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test observer
1545181 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test removeDups
354 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
368 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/removeDups/arrayPart.key
10676 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14141 INFO 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
17308 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20228 INFO 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
34723 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1584460 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test removeDups
1584461 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test Saddleback_search.key
357 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
366 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
379 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/saddleback_search/Saddleback_search.key
86744 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1677779 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test Saddleback_search.key
1677780 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test quicksort
349 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
364 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
379 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/toplevel.key
9502 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12919 INFO 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
15919 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'script 'sort.script''
15926 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
15927 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
17074 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'select formula="{heapAtPre:=heap || exc:=null || heap:=heapAfter_sort_0}
seq ...'
17079 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
17088 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'let @seqPre="seqDef{int u;}(0, array.length, array[u])"
@seqSplit="seqDef ...'
17091 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule seqPermSym
formula="seqPerm(@seqSplit, @seqPre)"'
17110 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'rule seqPermSym
formula="seqPerm(@seqSort, @seqSplit)"'
17112 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'rule seqPermSym
formula="seqPerm(@seqSort0, @seqSort)"'
17113 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSplit)"'
17114 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSort)"'
17115 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'rule seqPermSym
formula="seqPerm(@seqPre, @seqSort0)"'
17117 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose'
42718 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47821 INFO 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
50648 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
51905 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'tryclose'
88805 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
88948 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'rule seqPermFromSwap'
88964 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule andRight'
88967 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'auto'
88996 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'instantiate hide var=iv with=i_0'
89002 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'instantiate hide var=jv with=j_0'
89004 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'auto'
95505 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'macro simp-upd'
95582 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'rule seqPermFromSwap'
95586 INFO main d.u.i.k.m.s.ProofScriptEngine 12: 'rule andRight'
95589 INFO main d.u.i.k.m.s.ProofScriptEngine 13: 'auto'
95607 INFO main d.u.i.k.m.s.ProofScriptEngine 14: 'instantiate hide var=iv with=i_0'
95610 INFO main d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate hide var=jv with=to'
95615 INFO main d.u.i.k.m.s.ProofScriptEngine 16: 'auto'
100562 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1785427 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test quicksort
1785428 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simpleTests
390 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.
421 INFO 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
8348 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11381 INFO 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
14917 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17831 INFO 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
20557 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23197 INFO 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
25781 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28432 INFO 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
30985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33601 INFO 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
37083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40061 INFO 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
42597 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45207 INFO 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
49117 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52215 INFO 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
55138 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57998 INFO 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
60494 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63057 INFO 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
65897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68770 INFO 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
71897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74813 INFO 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
77305 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79882 INFO 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
82365 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84922 INFO 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
87525 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90123 INFO 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
93450 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96405 INFO 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
98914 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101490 INFO 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
107665 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111140 INFO 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
113913 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116600 INFO 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
119377 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122260 INFO 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
124953 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127850 INFO 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
130505 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133219 INFO 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
135859 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138634 INFO 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
141393 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
144180 INFO main 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
146625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
149249 INFO 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
151741 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154434 INFO 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
156922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1942827 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simpleTests
1942828 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SmansEtAl
349 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
349 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
376 INFO 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
15910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20516 INFO 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
24482 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27694 INFO 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
30717 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33724 INFO 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
36848 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39869 INFO 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
42882 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45796 INFO 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
48650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
51552 INFO 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
54386 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57313 INFO 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
60149 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63072 INFO 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
66005 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68955 INFO 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
71730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74648 INFO 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
77490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80427 INFO 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
83234 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86150 INFO 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
88915 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91801 INFO 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
94617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97547 INFO 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
100722 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103756 INFO 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
106518 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109398 INFO 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
112691 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115700 INFO 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
118904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121891 INFO 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
124780 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127713 INFO 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
131704 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134798 INFO 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
137594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
140514 INFO 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
143265 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146176 INFO 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
151253 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154462 INFO 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
157310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
160230 INFO 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
162967 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
165865 INFO 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
169205 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
172251 INFO 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
175110 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178082 INFO 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
181735 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
184889 INFO 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
191860 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2138285 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SmansEtAl
2138286 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.)
369 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/vacid0_01_SparseArray/Harness_sparseArrayTestHarness1.key
9908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13366 INFO 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
26263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30355 INFO 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
34082 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37237 INFO 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
40546 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43537 INFO 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
49144 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52424 INFO 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
57156 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60312 INFO 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
64690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67619 INFO 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
73546 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2215325 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VACID0
2215327 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VSTTE10
401 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
421 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
434 INFO 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
12975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16899 INFO 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
21242 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24475 INFO 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
27594 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30491 INFO 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
38553 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42135 INFO 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
46783 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50051 INFO 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
64588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68537 INFO 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
72676 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75807 INFO 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
79047 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82021 INFO 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
92631 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96349 INFO 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
101216 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104454 INFO 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
107254 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110220 INFO 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
113162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116060 INFO 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
118819 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
121747 INFO 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
126104 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129244 INFO 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
133685 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
136792 INFO 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
151216 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
155344 INFO 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
166391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170071 INFO 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
173258 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2391741 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VSTTE10
2391742 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test WeideEtAl
345 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.
372 INFO 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
9946 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13240 INFO 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
16547 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19489 INFO 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
25106 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2420440 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test WeideEtAl
2420440 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arithmetic
402 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 The settings in /home/runner/.key/proof-settings.props are *not* read.
428 INFO main 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
7879 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10684 INFO main 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
13350 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15953 INFO main 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
23091 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26163 INFO main 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
28697 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31254 INFO main 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
36754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39503 INFO main 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
42334 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44938 INFO main 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
47500 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50052 INFO main 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
52471 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54976 INFO main 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
58694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61522 INFO main 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
65117 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67946 INFO main 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
70536 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73066 INFO main 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
76030 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78644 INFO main 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
81010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83557 INFO main 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
89070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91924 INFO main 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
134167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
140663 INFO main 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
143268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
145922 INFO main 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
162663 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166439 INFO main 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
168915 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
171496 INFO main 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
173841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
176311 INFO main 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
178679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
181185 INFO main 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
187759 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190678 INFO main 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
193040 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
195602 INFO main 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
197945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
200445 INFO main 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
204604 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
207216 INFO main 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
209630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
212151 INFO main 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
214492 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
216988 INFO main 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
219317 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
221833 INFO main 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
224178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
226699 INFO main 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
229046 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
231567 INFO main 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
234130 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
236747 INFO main 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
239187 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
241739 INFO main 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
244075 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
246612 INFO main 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
249153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
251734 INFO main 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
254181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
256750 INFO main 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
259186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
261768 INFO main 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
264321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
266912 INFO main 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
269272 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
271846 INFO main 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
274189 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
276757 INFO main 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
279099 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
281677 INFO main 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
284005 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
286588 INFO main 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
288919 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
291501 INFO main 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
293845 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
296437 INFO main 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
298781 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
301386 INFO main 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
303724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
306334 INFO main 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
308662 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
311268 INFO main 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
313597 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
316217 INFO main 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
318547 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
321168 INFO main 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
323507 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
326143 INFO main 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
328887 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
331595 INFO main 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
333938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
336590 INFO main 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
339032 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
341715 INFO main 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
344255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
346954 INFO main 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
349410 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
352255 INFO main 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
354914 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
357610 INFO main 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
359995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
362681 INFO main 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
365000 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
367670 INFO main 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
369982 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
372638 INFO main 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
374958 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
377632 INFO main 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
379954 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
382645 INFO main 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
384963 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
387664 INFO main 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
390084 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
392804 INFO main 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
397826 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
400813 INFO main 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
403170 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
405926 INFO main 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
408764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
411625 INFO main 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
414384 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
417247 INFO main 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
419587 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
422344 INFO main 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
424687 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
427431 INFO main 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
429769 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432499 INFO main 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
434828 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
437581 INFO main 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
439916 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
442660 INFO main 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
444985 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
447729 INFO main 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
450056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
452814 INFO main 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
455149 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
457918 INFO main 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
460263 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
463032 INFO main 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
468600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
471614 INFO main 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
474115 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2897601 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arithmetic
2897602 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arrays
324 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
333 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
358 INFO main 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
12326 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16081 INFO main 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
19010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21783 INFO main 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
24890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27783 INFO main 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
30696 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33433 INFO main 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
36070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38722 INFO main 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
44356 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
44632 INFO main 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
49098 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
49495 INFO main 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
56003 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2954122 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arrays
2954123 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javadl
354 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.
377 INFO main 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
9496 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12795 INFO main 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
16257 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19339 INFO main 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
22148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25002 INFO main 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
28072 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30978 INFO main 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
33940 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36826 INFO main 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
39544 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42339 INFO main 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
46401 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49536 INFO main 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
49563 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
49564 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
49564 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
52321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52580 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
52581 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
52581 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
55143 INFO main 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
57944 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60737 INFO main 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
60760 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
60761 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
60761 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
63456 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63693 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
63694 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
63694 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
66347 INFO main 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
68952 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71670 INFO main 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
74289 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76992 INFO main 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
79814 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82687 INFO main 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
85346 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
85568 INFO main 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
85591 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
85591 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
85591 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
88148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88386 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
88386 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
88386 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
90978 INFO main 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
91001 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
91001 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
91002 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
93756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94109 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
94109 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
94109 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
96644 INFO main 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
99212 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101924 INFO main 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
104484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107168 INFO main 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
109723 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
112380 INFO main 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
115145 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117976 INFO main 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
120754 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123593 INFO main 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
126213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
126520 INFO main 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
129912 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
132944 INFO main 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
132967 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
132967 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
132967 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
135707 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
136077 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
136078 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
136078 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
138546 INFO main 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
141087 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143824 INFO main 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
146392 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
149110 INFO main 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
149132 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
149133 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
149133 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
151682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151998 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
151999 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
151999 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
154428 INFO main 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
156936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
159637 INFO main 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
162182 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
164866 INFO main 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
167397 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170095 INFO main 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
172620 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
172963 INFO main 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
175657 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
178443 INFO main 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
181124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
181467 INFO main 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
184132 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
186960 INFO main 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
189560 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
189897 INFO main 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
193772 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
197294 INFO main 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
200316 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
203465 INFO main 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
206345 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
209376 INFO main 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
212367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
215417 INFO main 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
218038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
220923 INFO main 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
223593 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
226466 INFO main 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
229043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
231876 INFO main 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
353622 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
360244 INFO main 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
363243 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
363647 INFO main 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
366225 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
366630 INFO main 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
369144 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
371979 INFO main 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
374517 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
377359 INFO main 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
379892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
382741 INFO main 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
385274 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
388117 INFO main 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
392607 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
395870 INFO main 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
398386 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
401231 INFO main 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
403743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
406563 INFO main 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
409114 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
411992 INFO main 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
414650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
417575 INFO main 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
417597 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
417597 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
417597 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
424327 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
424876 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
424876 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
424876 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
428093 INFO main 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
428116 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
428116 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
428116 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
432045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432656 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
432656 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
432657 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
435333 INFO main 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
437822 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
440717 INFO main 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
443200 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
446034 INFO main 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
448563 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
451479 INFO main 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
458608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
462509 INFO main 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
556763 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
560903 INFO main 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
560924 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
560925 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
560925 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
563711 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
564375 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
564376 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
564376 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
566893 INFO main 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
566914 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
566914 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
569942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
570544 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
570544 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
573147 INFO main 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
573168 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
573169 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
575696 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
576283 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
576283 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
578680 INFO main 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
578700 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
578700 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
581203 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
581759 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
581759 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
584153 INFO main 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
584176 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
584177 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
586884 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
587456 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
587456 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
589897 INFO main 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
589918 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
589919 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
592532 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
593119 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
593120 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
595560 INFO main 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
595580 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
595580 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
610320 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
611016 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
611017 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
615412 INFO main 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
615432 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
615432 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
618208 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
618887 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
618887 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
621354 INFO main 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
623831 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
626758 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
626784 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
629419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
630027 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
632505 INFO 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
635091 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
635671 INFO 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
638239 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3593145 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javadl
3593152 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test FOL
345 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
352 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
366 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/count.key
8181 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11195 INFO main 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
14067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16898 INFO main 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
19597 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22362 INFO main 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
25052 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27780 INFO main 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
30448 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33194 INFO main 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
35820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38515 INFO main 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
41148 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43843 INFO main 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
46496 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49191 INFO main 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
51771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54454 INFO main 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
57029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59711 INFO main 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
62333 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64979 INFO main 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
67784 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
70497 INFO main 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
76013 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78956 INFO main 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
81497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84194 INFO main 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
94730 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97452 INFO main 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
100056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102712 INFO main 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
105292 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107967 INFO main 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
110560 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113211 INFO main 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
115779 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118444 INFO main 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
120992 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123709 INFO main 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
126432 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129192 INFO main 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
134353 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
137100 INFO main 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
139684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
139960 INFO main 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
142464 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
142716 INFO main 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
145284 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
147955 INFO main 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
150523 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
153289 INFO main 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
155909 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
158644 INFO main 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
161180 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
163850 INFO main 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
166395 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169116 INFO main 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
171633 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
174317 INFO main 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
176849 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
179544 INFO main 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
182059 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
184763 INFO main 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
187292 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190056 INFO main 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
193812 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
196602 INFO main 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
203588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
206379 INFO main 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
208996 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
211816 INFO main 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
214325 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
217053 INFO main 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
219569 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
222305 INFO main 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
224823 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
227583 INFO main 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
230096 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232831 INFO main 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
235336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238082 INFO main 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
240588 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
243342 INFO main 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
245851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
248612 INFO main 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
251124 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
253917 INFO main 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
256423 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
259201 INFO main 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
261728 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
264497 INFO main 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
267019 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
269804 INFO main 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
272336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
275227 INFO main 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
277751 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
280538 INFO main 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
283055 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
285834 INFO main 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
288349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3884486 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test FOL
3884487 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test strings
350 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.
377 INFO main 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
8310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11319 INFO main 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
14098 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16985 INFO main 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
19668 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22417 INFO main 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
25043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27819 INFO main 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
30467 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33198 INFO main 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
35865 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38573 INFO main 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
41995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44806 INFO main 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
47756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50501 INFO main 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
53723 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56499 INFO main 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
59270 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62009 INFO main 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
64655 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67353 INFO main 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
70541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73556 INFO main 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
76142 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78802 INFO main 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
81370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84001 INFO main 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
86603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89250 INFO main 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
91818 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94466 INFO main 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
97161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99992 INFO main 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
102564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105242 INFO main 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
110343 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113510 INFO main 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
116090 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118775 INFO main 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
121614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124327 INFO main 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
126868 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129542 INFO main 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
132058 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134734 INFO main 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
137260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
140024 INFO main 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
142561 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
145271 INFO main 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
147782 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150441 INFO main 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
153162 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4040595 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test strings
4040595 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simple_info_flow
355 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.
388 INFO 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
9206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
9329 INFO 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
12815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
4053706 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simple_info_flow
4053707 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test modelMethods
328 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
338 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
359 INFO 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
8692 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11957 INFO 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
14961 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17937 INFO 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
20900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23844 INFO 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
26683 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29571 INFO 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
32348 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35195 INFO 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
43723 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47207 INFO 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
50103 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53000 INFO 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
55987 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58883 INFO 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
63937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67349 INFO 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
70101 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72932 INFO 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
75678 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78462 INFO 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
81184 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83997 INFO 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
86724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89590 INFO 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
92288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95127 INFO 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
97811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
100594 INFO 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
103310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106111 INFO 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
108816 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111627 INFO 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
114339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117150 INFO 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
119969 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122866 INFO 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
125558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128404 INFO 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
131059 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133854 INFO 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
136552 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139514 INFO 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
142165 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
145090 INFO 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
147788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150617 INFO 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
153280 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156121 INFO 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
158817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161636 INFO 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
170277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173610 INFO 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
176290 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4233072 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test modelMethods
4233073 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test permissionHeap
384 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
398 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
425 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/permissions/permissions_method0.key
9922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
13311 INFO main 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
16490 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19503 INFO main 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
23618 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26815 INFO main 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
31186 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34417 INFO main 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
38250 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40909 INFO main 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
48198 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53437 INFO main 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
58429 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63533 INFO main 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
68444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73417 INFO main 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
78242 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83259 INFO main 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
89119 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94273 INFO main 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
99216 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104218 INFO main 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
109056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114033 INFO main 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
119127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124114 INFO main 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
137932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143796 INFO main 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
149015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
154118 INFO main 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
159178 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
164182 INFO main 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
169022 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
173969 INFO main 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
178808 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
183753 INFO main 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
189461 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
194607 INFO main 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
199441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
204422 INFO main 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
209214 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
214177 INFO main 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
218990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
223983 INFO main 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
229733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
234975 INFO main 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
239850 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
244852 INFO main 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
249681 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
254670 INFO main 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
259674 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
264738 INFO main 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
278766 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
284590 INFO main 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
290321 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
295404 INFO main 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
300398 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
305472 INFO main 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
310258 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
315253 INFO main 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
320021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
325026 INFO main 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
330287 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
335429 INFO main 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
340204 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
345228 INFO main 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
350010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
355051 INFO main 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
359825 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
364901 INFO main 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
369825 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
374923 INFO main 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
379682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
384739 INFO main 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
389506 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
394554 INFO main 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
399313 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
404372 INFO main 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
409262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
414374 INFO main 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
419138 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
424221 INFO main 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
428979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
434055 INFO main 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
438815 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
443907 INFO main 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
448676 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
453757 INFO main 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
458525 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
463625 INFO main 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
468585 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
473689 INFO main 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
480480 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
486066 INFO main 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
490818 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
495905 INFO main 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
501527 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
506704 INFO main 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
518387 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
524086 INFO main 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
529452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
534606 INFO main 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
539337 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
544448 INFO main 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
549175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
554266 INFO main 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
558986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
564081 INFO main 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
568806 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
573912 INFO main 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
581736 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
587522 INFO main 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
592265 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
597419 INFO main 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
602161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
607317 INFO main 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
612057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
617268 INFO main 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
622100 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
627309 INFO main 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
632444 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
637702 INFO main 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
646153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
651950 INFO main 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
656704 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
661900 INFO main 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
666644 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
671841 INFO main 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
676584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
681779 INFO main 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
686516 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
691725 INFO main 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
695885 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
699762 INFO main 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
704313 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
708188 INFO main 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
711168 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
714362 INFO main 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
717068 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
720736 INFO main 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
723673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
726935 INFO main 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
729788 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
733074 INFO main 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
737603 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
741684 INFO main 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
746841 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
751144 INFO main 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
754535 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
758348 INFO main 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
761756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
765657 INFO main 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
769066 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
772921 INFO main 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
776474 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
780274 INFO main 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
783669 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
787527 INFO main 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
790900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
794772 INFO main 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
798158 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
802089 INFO main 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
805380 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
809289 INFO main 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
812972 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
817037 INFO main 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
820469 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
824362 INFO main 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
827995 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
831995 INFO main 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
835597 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
839647 INFO main 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
844611 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
844612 INFO main 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
849691 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
849692 INFO main 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
854565 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
854567 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
854569 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
854570 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
854571 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
854572 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
854574 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
854575 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
854577 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
854579 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
854580 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
854581 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
854582 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
854582 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
854583 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
854584 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
854585 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
854586 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
854587 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
854587 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
854588 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
854588 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
854666 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
5087923 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test permissionHeap
5087925 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test completionScopes
355 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.
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/.././completionscopes/testCcatchReturnVal.key
8462 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11591 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
14718 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17886 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
20861 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23760 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
26472 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29271 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
32009 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34778 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
37475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40251 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
42885 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45566 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././completionscopes/testCcatchBreakLabelNonmatchingNested.key
48213 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5139029 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test completionScopes
5139030 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test reload_examples
377 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
384 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
397 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
18831 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23271 INFO main 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
25747 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
25749 INFO 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
29570 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
29572 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
33379 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
33380 INFO 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
36542 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
36544 INFO 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
40193 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
40195 INFO 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
43506 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
5182723 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test reload_examples
5182724 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test proofLoadRepair
337 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
347 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././proofLoadRepair/disjConj-manipulated.proof
7838 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft
7840 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right
7847 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close
7852 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
7858 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
10644 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for applyEq
10657 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
10659 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
13188 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
13190 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
15744 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
15745 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
18090 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
5200990 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test proofLoadRepair
5200991 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test switch
393 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.
424 INFO main 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
9215 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12488 INFO main 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
15331 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18201 INFO main 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
21070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23885 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/empty_switch_null_catch.key
26601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29374 INFO main 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
32166 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35051 INFO main 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
37812 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40573 INFO main 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
47304 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50730 INFO main 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
54122 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57114 INFO main 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
61006 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5265432 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test switch
5265433 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test redux
344 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
361 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/.././redux/arrays/Arrays.copyOf.key
13718 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17822 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
21109 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
25322 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
25398 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 17 in 48ms, result is valid
25398 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
27049 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31187 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
38623 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42359 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
45474 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
51034 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
51077 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 27 in 36ms, result is valid
51077 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
54370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58539 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
62071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65513 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
68694 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71855 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
75010 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78192 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
81666 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84900 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
88580 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
91868 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
100666 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104672 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
107946 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111162 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
119975 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5390306 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test redux
5390344 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
5390351 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
5390351 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
5390351 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
5390352 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
5390352 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
5390352 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
5390352 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
5390352 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
5390352 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
5390352 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
5390353 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
5390353 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
5390354 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
5390354 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
5390354 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
5390354 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