492 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test newBook
387 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
397 WARN main d.u.i.k.s.ProofSettings 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)
423 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
24305 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28674 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
35314 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38757 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
42277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45132 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
48071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50856 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
54245 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57763 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test newBook
57770 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test oldBook
354 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
360 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
375 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/BookExamples/02FirstOrderLogic/Ex2.58.key
8237 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11371 INFO main 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
14411 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75064 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test oldBook
75068 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test comprehensions
382 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
385 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
411 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/general_sum.key
8211 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11136 INFO 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
14617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17535 INFO 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
20709 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23669 INFO 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
26639 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29343 INFO 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
32177 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34976 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/comprehensions/segsum.key
37890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40605 INFO 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
43016 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45480 INFO 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
47889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50317 INFO 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
52739 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55199 INFO 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
57576 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60064 INFO 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
62441 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
137831 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test comprehensions
137833 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performance
344 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
372 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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
19625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30849 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
42189 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52698 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
65185 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76061 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
92144 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103346 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
114356 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124830 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
140062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150852 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
165061 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
176065 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
188004 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
198674 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
211629 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
360385 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performance
360390 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test performancePOConstruction
379 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
385 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
398 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././performance-test/Test(Test__a0(int)).JML_normal_behavior_operation_contract.0.key
17329 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28353 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
39061 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49322 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
59512 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
430205 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test performancePOConstruction
430207 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test applicationRestrictions
330 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
337 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
350 INFO 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
7964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10938 INFO 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
13682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
13812 INFO 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
16476 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19197 INFO 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
21904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
22017 INFO 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
24644 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27267 INFO 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
29856 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
29973 INFO 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
32600 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35249 INFO 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
37852 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
37982 INFO 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
40567 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43171 INFO 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
45720 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
45862 INFO 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
48484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
479047 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test applicationRestrictions
479048 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test blockContracts
360 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.
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/.././heap/block_contracts/Simple__add.key
9192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12748 INFO 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
17154 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20590 INFO 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
23773 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26949 INFO 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
30078 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33244 INFO 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
38068 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41359 INFO 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
44355 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47437 INFO 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
50707 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53831 INFO 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
56803 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59861 INFO 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
62813 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
65856 INFO main d.u.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
68555 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71392 INFO main d.u.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
73987 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
76647 INFO 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
79519 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82390 INFO 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
85682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88818 INFO 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
92246 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95351 INFO 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
98147 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101064 INFO 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
104301 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
107506 INFO 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
110924 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114164 INFO 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
116624 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119197 INFO 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
121660 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124198 INFO 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
127083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
127328 INFO 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
130259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
609755 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test blockContracts
609756 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test jmlAsserts
346 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
357 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
384 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/jml-assert/assert.key
8601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11926 INFO 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
14824 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17527 INFO 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
20164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22856 INFO main d.u.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
25726 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28535 INFO main d.u.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
31394 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34181 INFO main d.u.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
36983 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39760 INFO main d.u.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
42474 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45212 INFO main d.u.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
47918 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50690 INFO main d.u.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
53391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
56151 INFO main d.u.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
58790 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61501 INFO main d.u.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
64260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67002 INFO main d.u.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
69682 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72366 INFO main d.u.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
74938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77582 INFO main d.u.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
80282 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82926 INFO main d.u.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
85569 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
698205 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test jmlAsserts
698209 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javaCard
365 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
391 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
404 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/javacard/updateBalance0.key
7961 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
9992 INFO 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
12192 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14060 INFO 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
16624 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18502 INFO 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
21083 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22960 INFO 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
28067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
728990 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javaCard
728992 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key
342 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
354 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
378 INFO 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
26936 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
760319 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key
760320 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#1
359 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/verifyThis11_1_Maximum/project.key
10550 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
774192 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#1
774193 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test lcp.key
348 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/fm12_01_LRS/lcp.key
11112 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
789207 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test lcp.key
789208 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test project.key#2
343 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
347 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
361 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/SemanticSlicing/project.key
14909 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
808555 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test project.key#2
808556 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_contains.key
324 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.
363 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/ArrayList_contains.key
9938 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
822075 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_contains.key
822078 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_get.key
353 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.
378 INFO 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
11207 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
837095 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_get.key
837096 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test ArrayList_size.key
358 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
361 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/ArrayList_size.key
9134 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
849890 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test ArrayList_size.key
849894 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_3_secure.key
377 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
404 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/.././heap/information_flow/UpdateAbstraction_ex7_3_secure.key
9218 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
862624 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_3_secure.key
862625 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_4_secure.key
311 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
320 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
334 INFO 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
9567 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
875887 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_4_secure.key
875889 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_5_secure.key
381 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
385 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
408 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/information_flow/UpdateAbstraction_ex7_5_secure.key
9127 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
888435 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_5_secure.key
888436 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex7_6_secure.key
336 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.
352 INFO 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
8847 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
900985 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex7_6_secure.key
900987 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test UpdateAbstraction_ex9_secure.key
354 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
372 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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/.././heap/information_flow/UpdateAbstraction_ex9_secure.key
10937 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
915705 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test UpdateAbstraction_ex9_secure.key
915705 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list
341 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
330 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
370 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list/ArrayList_add.key
14486 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19154 INFO 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
23699 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27148 INFO 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
53833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59314 INFO 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
65034 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68665 INFO 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
73844 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77388 INFO 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
80484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83549 INFO 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
86865 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90041 INFO 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
94142 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97497 INFO 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
100848 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104104 INFO 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
107352 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110493 INFO 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
113905 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
117068 INFO 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
120193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123293 INFO 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
126409 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129521 INFO 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
133015 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
136197 INFO 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
139393 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
142493 INFO 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
145786 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
148906 INFO 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
152683 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
155849 INFO 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
158823 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161861 INFO 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
165566 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
168843 INFO 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
172626 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
175947 INFO 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
178897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
182036 INFO 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
185199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
188336 INFO 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
191313 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
194428 INFO 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
199288 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
202669 INFO 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
210842 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
214450 INFO 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
217817 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
221021 INFO 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
224373 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
227513 INFO 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
230771 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
233915 INFO 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
237070 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
240210 INFO 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
245293 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1164667 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list
1164668 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_ghost
378 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.
405 INFO 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
12415 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16105 INFO 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
19849 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22709 INFO 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
27391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30415 INFO 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
33231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35933 INFO 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
39167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41908 INFO 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
44564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
47265 INFO 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
49793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52373 INFO 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
54883 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57533 INFO 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
60031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1227456 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_ghost
1227457 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_recursive
366 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
374 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
398 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_recursiveSpec/ListOperationsNonNull_getNextNN_normal_behavior.key
9176 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12552 INFO 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
15442 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
17930 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'macro simp-upd'
17936 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'rule observerDependencyEQ'
17955 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'tryclose'
17979 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1248582 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_recursive
1248583 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test list_seq
390 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
390 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
420 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/list_seq/SimplifiedLinkedList.remove.key
63067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69809 INFO 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
73698 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77037 INFO 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
83056 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
86582 INFO 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
91008 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94357 INFO 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
99167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
102530 INFO 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
105945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109068 INFO 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
112266 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115440 INFO 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
120153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
123677 INFO 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
137255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1390505 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test list_seq
1390506 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test observer
376 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
378 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
390 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/observer/ExampleObserver_ExampleObserver.key
9640 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12979 INFO 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
15981 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19083 INFO 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
22001 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24901 INFO 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
27974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30962 INFO 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
33835 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
36780 INFO 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
39614 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
42526 INFO 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
50358 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53943 INFO 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
57257 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60206 INFO 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
63944 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67003 INFO 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
69851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72722 INFO 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
76538 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79573 INFO 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
82393 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
85264 INFO 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
88029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
90946 INFO 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
93763 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1487311 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test observer
1487312 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test removeDups
381 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
400 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
415 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/removeDups/arrayPart.key
10664 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
14014 INFO 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
17362 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20248 INFO 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
34356 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1525950 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test removeDups
1525951 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test Saddleback_search.key
366 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
388 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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/saddleback_search/Saddleback_search.key
80946 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1613118 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test Saddleback_search.key
1613119 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test quicksort
377 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
391 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/quicksort/toplevel.key
9209 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12476 INFO 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
15387 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'script 'sort.script''
15391 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
15392 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
16369 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'select formula="{heapAtPre:=heap || exc:=null || heap:=heapAfter_sort_0}
seq ...'
16375 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
16383 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'let @seqPre="seqDef{int u;}(0, array.length, array[u])"
@seqSplit="seqDef ...'
16386 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule seqPermSym
formula="seqPerm(@seqSplit, @seqPre)"'
16403 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'rule seqPermSym
formula="seqPerm(@seqSort, @seqSplit)"'
16405 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'rule seqPermSym
formula="seqPerm(@seqSort0, @seqSort)"'
16406 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSplit)"'
16407 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermTrans
formula="seqPerm(@seqPre, @seqSort)"'
16407 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'rule seqPermSym
formula="seqPerm(@seqPre, @seqSort0)"'
16408 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose'
40057 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44757 INFO 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
47469 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot-prep'
48545 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'tryclose'
82130 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'macro simp-upd'
82259 INFO main d.u.i.k.m.s.ProofScriptEngine 4: 'rule seqPermFromSwap'
82274 INFO main d.u.i.k.m.s.ProofScriptEngine 5: 'rule andRight'
82276 INFO main d.u.i.k.m.s.ProofScriptEngine 6: 'auto'
82298 INFO main d.u.i.k.m.s.ProofScriptEngine 7: 'instantiate hide var=iv with=i_0'
82302 INFO main d.u.i.k.m.s.ProofScriptEngine 8: 'instantiate hide var=jv with=j_0'
82304 INFO main d.u.i.k.m.s.ProofScriptEngine 9: 'auto'
88268 INFO main d.u.i.k.m.s.ProofScriptEngine 10: 'macro simp-upd'
88341 INFO main d.u.i.k.m.s.ProofScriptEngine 11: 'rule seqPermFromSwap'
88346 INFO main d.u.i.k.m.s.ProofScriptEngine 12: 'rule andRight'
88348 INFO main d.u.i.k.m.s.ProofScriptEngine 13: 'auto'
88362 INFO main d.u.i.k.m.s.ProofScriptEngine 14: 'instantiate hide var=iv with=i_0'
88365 INFO main d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate hide var=jv with=to'
88366 INFO main d.u.i.k.m.s.ProofScriptEngine 16: 'auto'
92908 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
1712752 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test quicksort
1712753 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simpleTests
386 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
398 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/.././heap/simple/anonymise_datagroup.key
7986 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10775 INFO 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
13743 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16418 INFO 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
19007 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21462 INFO 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
23887 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26361 INFO 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
28720 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31128 INFO 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
34394 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37214 INFO 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
39560 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41946 INFO 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
45629 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
48474 INFO 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
51197 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
53849 INFO 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
56164 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58542 INFO 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
61147 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63813 INFO 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
66840 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
69666 INFO 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
71983 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74394 INFO 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
76670 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79074 INFO 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
81451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83880 INFO 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
87039 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89773 INFO 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
92096 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94481 INFO 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
100314 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103525 INFO 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
106140 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108585 INFO 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
111231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113887 INFO 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
116427 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
119132 INFO 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
121602 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124118 INFO 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
126620 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129171 INFO 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
131679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134286 INFO main 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
136584 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
138978 INFO 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
141368 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143855 INFO 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
146216 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
1859387 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simpleTests
1859388 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test SmansEtAl
362 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/SmansEtAl/ArrayList_add.key
15738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
19993 INFO 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
23922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26979 INFO 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
29764 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32574 INFO 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
35555 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38423 INFO 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
41238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44067 INFO 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
46774 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49591 INFO 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
52273 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55077 INFO 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
57821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60592 INFO 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
63391 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
66174 INFO 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
68878 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
71640 INFO 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
74327 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77094 INFO 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
79741 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82499 INFO 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
85193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87928 INFO 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
90617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
93388 INFO 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
96458 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99313 INFO 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
102011 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104779 INFO 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
107945 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110793 INFO 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
113873 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116758 INFO 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
119541 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
122333 INFO 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
126076 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129033 INFO 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
131687 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134456 INFO 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
137108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139865 INFO 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
144836 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
147870 INFO 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
150613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
153411 INFO 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
156044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
158854 INFO 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
162044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
164934 INFO 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
167679 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170486 INFO 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
174022 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177004 INFO 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
183770 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2046593 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test SmansEtAl
2046595 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VACID0
337 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.
365 INFO 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
9485 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12812 INFO 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
25045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28986 INFO 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
32574 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35412 INFO 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
38457 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41290 INFO 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
46637 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49661 INFO 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
54102 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57033 INFO 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
61281 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64058 INFO 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
69656 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2119540 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VACID0
2119540 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test VSTTE10
360 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
372 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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/vstte10_01_SumAndMax/SumAndMax_sumAndMax.key
13240 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17043 INFO 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
21262 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24424 INFO 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
27392 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30216 INFO 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
38116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41685 INFO 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
46259 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49488 INFO 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
64017 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67895 INFO 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
72029 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
75138 INFO 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
78212 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
81122 INFO 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
91684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
95322 INFO 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
100086 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
103238 INFO 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
106027 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
108886 INFO 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
111821 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
114709 INFO 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
117475 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120289 INFO 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
124650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
127714 INFO 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
132081 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135185 INFO 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
149814 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
153861 INFO 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
165149 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
168738 INFO 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
171912 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2294539 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test VSTTE10
2294540 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test WeideEtAl
387 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
397 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
411 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/WeideEtAl_01_AddAndMultiply/AddAndMultiply_add.key
9690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12907 INFO 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
16020 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18810 INFO 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
24268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2322093 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test WeideEtAl
2322094 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arithmetic
331 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
332 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
368 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arith/binomial1.key
8024 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10814 INFO main 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
13501 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16110 INFO main 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
23310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26450 INFO main 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
29067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31663 INFO main 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
37153 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39900 INFO main 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
42793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45393 INFO main 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
47948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50488 INFO main 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
52953 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55425 INFO main 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
59118 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
61836 INFO main 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
65370 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68310 INFO main 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
70968 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73580 INFO main 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
76561 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79123 INFO main 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
81581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84103 INFO main 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
89703 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92542 INFO main 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
134589 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
140979 INFO main 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
143581 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146200 INFO main 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
162732 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
166473 INFO main 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
168948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
171500 INFO main 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
173897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
176387 INFO main 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
178793 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
181288 INFO main 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
187971 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
190878 INFO main 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
193336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
195915 INFO main 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
198333 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
200849 INFO main 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
205075 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
207699 INFO main 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
210129 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
213156 INFO main 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
215564 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
218080 INFO main 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
220473 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
222988 INFO main 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
225383 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
227953 INFO main 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
230341 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232863 INFO main 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
235476 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
238059 INFO main 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
240574 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
243223 INFO main 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
245645 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
248203 INFO main 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
250801 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
253426 INFO main 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
255935 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
258528 INFO main 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
261031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
263650 INFO main 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
266161 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
268771 INFO main 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
271180 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
273773 INFO main 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
276175 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
278752 INFO main 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
281143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
283721 INFO main 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
286103 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
288676 INFO main 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
291061 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
293641 INFO main 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
296025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
298602 INFO main 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
300988 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
303586 INFO main 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
305977 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
308576 INFO main 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
310966 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
313567 INFO main 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
315957 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
318571 INFO main 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
320950 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
323557 INFO main 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
325949 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
328616 INFO main 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
331419 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
334113 INFO main 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
336511 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
339152 INFO main 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
341650 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
344298 INFO main 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
346897 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
349570 INFO main 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
352073 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
354795 INFO main 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
357328 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
360128 INFO main 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
362625 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
365280 INFO main 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
367673 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
370460 INFO main 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
373041 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
375806 INFO main 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
378290 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
381032 INFO main 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
383558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
386324 INFO main 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
388807 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
391609 INFO main 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
394451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
397272 INFO main 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
402712 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
405859 INFO main 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
408396 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
411054 INFO main 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
413922 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
416714 INFO main 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
419487 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
422294 INFO main 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
424663 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
427367 INFO main 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
429728 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432443 INFO main 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
434807 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
437518 INFO main 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
439876 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
442563 INFO main 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
444917 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
447615 INFO main 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
449970 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
452673 INFO main 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
455030 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
457744 INFO main 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
460101 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
462804 INFO main 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
465157 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
467883 INFO main 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
473505 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
476450 INFO main 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
478942 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
2804000 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arithmetic
2804000 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test arrays
354 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
365 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
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/arrays/arrayStoreException/array2DimPrim.key
12143 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15590 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/arrays/arrayStoreException/arrayStoreKnownDynType.key
18309 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20960 INFO main 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
24025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
26805 INFO main 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
29599 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
32256 INFO main 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
34693 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37195 INFO main 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
42843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
43066 INFO main 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
47609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
47936 INFO main 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
54526 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
2858997 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test arrays
2858998 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test javadl
369 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
378 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
392 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/instanceCreation/instanceCreation1.key
9114 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12151 INFO main 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
15508 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18382 INFO main 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
21072 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
23813 INFO main 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
26642 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29438 INFO main 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
32254 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
34986 INFO main d.u.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
37542 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40189 INFO main d.u.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
43890 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46726 INFO main d.u.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
46751 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
46751 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
46751 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
49452 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49669 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
49670 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
49670 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
52114 INFO main d.u.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
54781 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57429 INFO main d.u.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
57451 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
57451 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
57451 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
59948 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
60132 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
60133 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
60133 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
62619 INFO main d.u.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
65074 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67608 INFO main d.u.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
70141 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72732 INFO main d.u.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
75396 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
78110 INFO main d.u.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
80688 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
80896 INFO main d.u.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
80917 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
80918 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
80918 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
83376 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
83580 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
83581 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
83581 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
85992 INFO main d.u.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
86014 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
86015 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
86015 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
88698 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
88921 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
88922 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
88922 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
91371 INFO main d.u.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
93840 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96360 INFO main d.u.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
98819 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
101357 INFO main d.u.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
103813 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
106343 INFO main d.u.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
108999 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
111673 INFO main d.u.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
114211 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
116862 INFO main d.u.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
119407 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
119634 INFO main d.u.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
122837 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125592 INFO main d.u.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
125612 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
125613 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
125613 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
128217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
128479 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
128479 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
128479 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
130872 INFO main d.u.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
133434 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
136034 INFO main d.u.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
138511 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141209 INFO main d.u.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
141228 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
141229 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
141229 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
143708 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143975 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
143975 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
143975 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
146405 INFO main d.u.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
148851 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151465 INFO main d.u.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
153896 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
156465 INFO main d.u.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
158888 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161456 INFO main d.u.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
163893 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
164161 INFO main d.u.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
166775 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169422 INFO main d.u.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
171912 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
172201 INFO main d.u.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
174756 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
177437 INFO main d.u.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
179931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
180219 INFO main d.u.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
184116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
187382 INFO main d.u.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
190406 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
193420 INFO main d.u.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
196193 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
199110 INFO main d.u.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
201976 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
204872 INFO main d.u.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
207431 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
210241 INFO main d.u.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
212834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
215588 INFO main d.u.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
218069 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
220782 INFO main d.u.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
342097 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
349035 INFO main d.u.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
351789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
352122 INFO main d.u.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
354592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
354928 INFO main d.u.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
357412 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
360128 INFO main d.u.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
362592 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
365325 INFO main d.u.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
367796 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
370529 INFO main d.u.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
372993 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
375725 INFO main d.u.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
380168 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
383315 INFO main d.u.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
385752 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
388469 INFO main d.u.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
390892 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
393579 INFO main d.u.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
396067 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
398843 INFO main d.u.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
401404 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
404207 INFO main d.u.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
404230 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
404230 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
404231 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
410738 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
411212 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
411212 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
411212 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
414234 INFO main d.u.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
414253 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
414253 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
414253 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
418085 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
418587 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
418588 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
418588 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
421201 INFO main d.u.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
423648 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
426386 INFO main d.u.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
428784 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
431467 INFO main d.u.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
433926 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
436679 INFO main d.u.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
443964 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
447636 INFO main d.u.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
542139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
546073 INFO main d.u.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
546091 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
546091 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
546091 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
548811 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
549367 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
549368 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
549368 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
551725 INFO main 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
551744 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
551744 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
554798 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
555311 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
555311 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
557761 INFO main 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
557779 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
557779 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
560238 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
560763 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
560763 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
563145 INFO main 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
563163 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
563164 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
565654 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
566119 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
566119 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
568499 INFO main 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
568517 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
568517 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
571217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
571704 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
571705 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
574067 INFO main 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
574085 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
574085 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
576618 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
577107 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
577107 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
579467 INFO main 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
579486 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
579486 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
594100 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
594663 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
594663 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
598936 INFO main 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
598953 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
598954 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
601676 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
602254 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
602255 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
604641 INFO main 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
607026 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
609766 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
609788 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
612310 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
612830 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
615269 INFO 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
617752 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
618240 INFO 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
620720 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3480418 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test javadl
3480419 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test FOL
375 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
386 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
406 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/count.key
8300 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11018 INFO main 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
13580 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16152 INFO main 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
18639 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21082 INFO main 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
23499 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25973 INFO main 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
28407 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30841 INFO main 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
33256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35680 INFO main 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
38087 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40520 INFO main 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
42896 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
45308 INFO main 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
47667 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50056 INFO main 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
52418 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
54843 INFO main 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
57220 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
59623 INFO main 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
62301 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
64740 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/pred_log/tptp/PUZ/PUZ001p1.key
69889 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
72425 INFO main 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
74803 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77212 INFO main 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
87484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89935 INFO main 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
92313 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94707 INFO main 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
97072 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99504 INFO main 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
101834 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104233 INFO main 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
106576 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109000 INFO main 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
111317 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
113763 INFO main 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
116195 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
118692 INFO main 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
123649 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
126123 INFO main 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
128442 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
128665 INFO main 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
130946 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
131206 INFO main 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
133505 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135913 INFO main 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
138256 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
140699 INFO main 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
143133 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
145580 INFO main 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
147900 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
150308 INFO main 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
152617 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
155034 INFO main 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
157336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
159748 INFO main 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
162065 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
164483 INFO main 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
166791 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
169250 INFO main 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
171534 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
174058 INFO main 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
177566 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
180069 INFO main 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
186894 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
189409 INFO main 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
191804 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
194379 INFO main 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
196684 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
199153 INFO main 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
201492 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
203959 INFO main 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
206268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
208743 INFO main 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
211040 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
213528 INFO main 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
215805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
218261 INFO main 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
220568 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
223042 INFO main 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
225327 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
227816 INFO main 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
230108 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
232585 INFO main 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
234874 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
237360 INFO main 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
239648 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
242146 INFO main 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
244445 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
246951 INFO main 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
249240 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
251743 INFO main 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
254038 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
256534 INFO main 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
258813 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
261338 INFO main 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
263633 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3746746 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test FOL
3746748 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test strings
317 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
325 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
340 INFO main 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
7765 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
10530 INFO main 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
13217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
15896 INFO main 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
18388 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
20916 INFO main 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
23367 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
25837 INFO main 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
28307 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
30785 INFO main 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
33231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
35685 INFO main 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
39031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
41607 INFO main 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
44277 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
46886 INFO main 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
49866 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
52377 INFO main 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
55031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
57523 INFO main 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
60043 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62526 INFO main 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
65439 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68144 INFO main 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
70561 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73009 INFO main 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
75398 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77841 INFO main 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
80224 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
82670 INFO main 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
85062 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87502 INFO main 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
89990 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
92492 INFO main 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
94860 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
97328 INFO main 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
102236 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105186 INFO main 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
107554 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
110053 INFO main 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
112703 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115244 INFO main 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
117602 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120055 INFO main 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
122412 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
124908 INFO main 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
127255 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
129705 INFO main 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
132064 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
134507 INFO main 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
136857 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
139310 INFO main 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
141763 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
3891219 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test strings
3891220 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test simple_info_flow
366 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.
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/information_flow/UpdateAbstraction_ex7_1_insecure.key
8806 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
8912 INFO 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
12233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: open goal(s)
3903755 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test simple_info_flow
3903755 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test modelMethods
391 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
405 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
433 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Cell_footprint_acc.key
9031 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11953 INFO 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
14769 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17489 INFO 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
20221 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22995 INFO 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
25632 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28265 INFO 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
30848 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33468 INFO 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
41630 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
44838 INFO 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
47608 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
50273 INFO 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
53065 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55808 INFO 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
60571 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
63701 INFO 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
66247 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68833 INFO 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
71388 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
73983 INFO 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
76504 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
79092 INFO 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
81640 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
84253 INFO 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
86733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
89332 INFO 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
91857 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
94451 INFO 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
96956 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99529 INFO 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
102051 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
104650 INFO 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
107199 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
109882 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././heap/model_methods/Indirect_test.key
112484 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115184 INFO 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
117666 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
120300 INFO 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
122820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
125418 INFO 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
127910 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
130670 INFO 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
133257 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
135948 INFO 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
138425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
141023 INFO 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
143540 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
146146 INFO 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
148623 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
151224 INFO 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
159410 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
162485 INFO 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
165004 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4071624 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test modelMethods
4071624 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test permissionHeap
370 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.
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/permissions/permissions_method0.key
9025 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
12248 INFO main 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
15219 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
18011 INFO main 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
21820 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
24761 INFO main 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
28680 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
31587 INFO main 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
35165 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
37651 INFO main 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
44425 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49331 INFO main 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
54019 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
58665 INFO main 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
63237 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
67874 INFO main 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
72451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
77098 INFO main 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
82613 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87343 INFO main 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
91931 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
96527 INFO main 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
101123 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105711 INFO main 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
110451 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
115087 INFO main 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
128068 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
133461 INFO main 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
138352 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
143055 INFO main 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
147706 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
152306 INFO main 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
156787 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
161367 INFO main 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
165855 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
170462 INFO main 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
175761 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
180548 INFO main 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
185081 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
189659 INFO main 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
194159 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
198758 INFO main 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
203260 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
207872 INFO main 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
213156 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
217882 INFO main 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
222375 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
227133 INFO main 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
231616 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
236276 INFO main 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
240950 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
245640 INFO main 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
258883 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
264279 INFO main 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
269609 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
274333 INFO main 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
279021 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
283740 INFO main 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
288211 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
292840 INFO main 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
297300 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
301933 INFO main 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
306904 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
311660 INFO main 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
316160 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
320819 INFO main 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
325300 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
329957 INFO main 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
334416 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
339074 INFO main 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
343637 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
348326 INFO main 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
352805 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
357477 INFO main 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
361947 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
366633 INFO main 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
371084 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
375778 INFO main 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
380349 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
385092 INFO main 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
389565 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
394266 INFO main 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
398933 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
403686 INFO main 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
408483 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
413484 INFO main 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
418158 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
422875 INFO main 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
427333 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
432104 INFO main 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
436583 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
441586 INFO main 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
447843 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
452994 INFO main 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
457448 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
462194 INFO main 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
467497 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
472324 INFO main 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
483405 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
488785 INFO main 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
493789 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
498645 INFO main 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
503159 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
507999 INFO main 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
512488 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
517261 INFO main 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
521724 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
526497 INFO main 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
530957 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
535733 INFO main 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
543116 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
548493 INFO main 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
552974 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
557758 INFO main 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
562206 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
567011 INFO main 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
571465 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
576277 INFO main 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
580733 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
585580 INFO main 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
590445 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
595356 INFO main 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
603336 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
608736 INFO main 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
613211 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
618046 INFO main 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
622507 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
627393 INFO main 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
631862 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
636700 INFO main 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
641167 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
646030 INFO main 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
649932 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
653545 INFO main 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
658268 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
661897 INFO main 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
664589 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
667552 INFO main 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
670112 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
673614 INFO main 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
676459 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
679570 INFO main 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
682244 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
685267 INFO main 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
689351 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
693196 INFO main 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
697690 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
701670 INFO main 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
704831 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
708342 INFO main 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
711668 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
715204 INFO main 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
718376 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
721931 INFO main 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
725051 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
728607 INFO main 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
731737 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
735306 INFO main 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
738563 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
742133 INFO main 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
745254 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
748822 INFO main 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
751914 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
755484 INFO main 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
758935 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
762721 INFO main 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
765874 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
769460 INFO main 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
772873 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
776569 INFO main 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
780044 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
783739 INFO main 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
788441 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
788442 INFO main 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
793211 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
793215 INFO main 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
797851 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
797854 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Plotter
797855 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
797856 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
797857 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
797858 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
797859 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
797861 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_BFilter
797862 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_AFilter
797864 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
797864 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Plotter
797865 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
797866 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_workingPermissions_in_Plotter
797866 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
797867 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_stateInv_in_Sampler
797867 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
797868 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_BFilter
797869 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_AFilter
797870 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
797870 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
797871 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_staticPermissions_in_Sampler
797871 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for Definition_axiom_for_joinTransfer_in_Plotter
797945 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
4869745 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test permissionHeap
4869746 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test completionScopes
338 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
359 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/.././completionscopes/testCcatchReturnVal.key
8079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11045 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
14071 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
16870 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
19760 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22530 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
25231 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
27922 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
30558 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33203 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
35833 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
38459 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
41045 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
43675 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
46233 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
4918787 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test completionScopes
4918787 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test reload_examples
406 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
429 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
455 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././firstTouch/05-ReverseArray/reverseArray.key
17435 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
21660 INFO main 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
24251 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
24252 INFO 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
27952 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
27954 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
31659 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
31660 INFO 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
34600 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
34601 INFO 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
38094 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
38095 INFO 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
41275 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
4960235 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test reload_examples
4960236 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test proofLoadRepair
338 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
341 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
367 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
8055 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for andLeft
8056 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for replace_known_right
8060 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for close
8064 INFO main d.u.i.k.p.r.p.TestFile ... success: loaded
8069 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
10867 WARN main d.u.i.k.p.i.IntermediateProofReplayer Proof contains wrong number of \assumes instatiations for applyEq
10879 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
10880 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
13485 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
13487 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
16115 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
16116 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
18597 INFO main d.u.i.k.p.r.p.TestFile ... success: loading failed
4978989 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test proofLoadRepair
4978990 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test switch
368 INFO Timeout watchdog d.u.i.k.p.r.p.ForkedTestFileRunner Timeout watcher launched (2000 secs.)
390 WARN main d.u.i.k.s.ProofSettings The settings in /home/runner/.key/proof-settings.props are *not* read.
410 INFO main d.u.i.k.p.r.p.TestFile Now processing file /home/runner/work/key/key/key.core/../key.ui/examples/index/.././standard_key/java_dl/switch/labeled_case.key
8685 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
11887 INFO main d.u.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
14695 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17445 INFO main d.u.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
20217 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
22976 INFO main d.u.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
25661 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
28376 INFO main d.u.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
31139 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
33848 INFO main d.u.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
36601 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
39427 INFO main d.u.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
46049 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
49353 INFO main d.u.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
52605 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55514 INFO main d.u.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
59339 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5041620 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test switch
5041621 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Running test redux
370 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.
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/.././redux/arrays/Arrays.copyOf.key
13327 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
17269 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
20329 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
24365 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
24427 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 17 in 39ms, result is valid
24427 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
25991 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
29754 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
36760 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
40333 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
43277 INFO main d.u.i.k.m.s.ProofScriptEngine 1: 'macro autopilot'
48446 INFO main d.u.i.k.m.s.ProofScriptEngine 2: 'smt solver=Z3'
48487 INFO main d.u.i.k.m.s.SMTCommand Finished run on goal 27 in 32ms, result is valid
48487 INFO main d.u.i.k.m.s.ProofScriptEngine 3: 'tryclose'
51516 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
55498 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
58915 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
62063 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
65079 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
68076 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
71136 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
74167 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
77524 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
80666 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
84123 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
87285 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
95578 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
99445 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
102539 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
105643 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
113915 INFO main d.u.i.k.p.r.p.TestFile ... finished proof: closed.
5160234 INFO Test worker d.u.i.k.p.r.RunAllProofsTestUnit Returning from test redux
5160269 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
5160271 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
5160271 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
5160271 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
5160271 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
5160271 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
5160271 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
5160271 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
5160271 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
5160272 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
5160272 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
5160272 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
5160272 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
5160272 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
5160272 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
5160272 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
5160272 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